Jason (jcreed) wrote,

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":

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

  • (no subject)

    Walked around UW-madison campus yesterday. It was almost entirely deserted, peaceful, cold. The passageways between buildings were as often as…

  • (no subject)

    Today I saw a really aesthetically great scene: there was a guy shuffling along the sidewalk, and the wind picked up and the rainwater falling from…

  • (no subject)

    About ten years ago, in the beginning of the calendar year 2000, 19-year-old me took some classes including "15-312" * and "Category Theory", and…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded