Jason (jcreed) wrote,
Jason
jcreed

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.
Tags: music, work
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 2 comments