|
[Oct. 23rd, 2006|07:32 pm]
Jason
|
I found this half by accident looking for something to show  arh006; it's got a pretty nice long bass solo over "Have you met Miss Jones":
http://youtube.com/watch?v=Cqm9FWXaOU8
Today I think I finally fixed my stupid logic programming HW 5, and did some silly but fun phantom types stuff with tom7. The takeaway idea is that you can get your index language to support first-order rewriting, if you don't mind putting in all the coercions yourself. The indexed type is exposed as a phantom type like type 'a foo = bar as usual, (where bar is the actual representation) and the things you use as indices are themselves elements of a type type 'a exp = unit, which has constructors exposed through a signature that express the allowable rewrites.
What we hacked up was a, ahem, proof of concept that you can, ahem, "do" higher-order rewriting too, by hacking up the first-order rewriting theory of S and K. It got sick very fast. |
|
