Jason (jcreed) wrote,

Did a good chunk of the homework for HOT compilation, and then got sucked back into thinking about stupid (but cute) ML tricks with phantom types and exn. Here is the result: http://www.cs.cmu.edu/~jcreed/transfer/px.tar.gz
Much credit again goes to tom7 for suggestions and prodding me into believing this could be done at all.

Here is a recap of what it is about: there is a type α xrec, pronounced "the type of extensible records satisfying refinement α". You can, up to suitable amounts of sympathetic squinting, embed into this type

  • row-polymorphic run-time-extensible variants
  • row-polymorphic run-time-extensible records
  • ordinary ML datatypes with inductive refinements

It's not quite as slick as you might hope; you have to provide static coercions all over the place, i.e. proofs that refinements are satisfied as you sling data around, but the point is the coercions are purely static, and could theoretically be eliminated by a smart optimizing compiler.

Here is a taste of an example; I can write a signature
 type even
 type odd
 val zero : even xrec
 val succ_even_odd : even xrec -> odd xrec
 val succ_odd_even : odd xrec -> even xrec
 val pred : odd xrec -> even xrec
and implement it with
structure S = NewXTag()
type 'a S = 'a S.stag
structure Z = NewTag(type content = unit)
type Z = Z.stag

datatype even = Zero of Z
              | OddSucc of odd S
withtype odd = even S

val zero = coe Zero (set1 Z.dtag ())
fun succ x = set1 S.dtag x
fun succ_even_odd (x) = succ x
fun succ_odd_even (x) = coe OddSucc (succ x)
fun pred x = test1 S.dtag x
Some explanation: NewXTag and NewTag are functors that generate new 'tags'. NewXTag always creates a tag that carries data of type &alpha xrec, and NewTag creates a tag that carries data of a type passed to the functor as a parameter. Lt, Rt are the injection to the type sum, the function coe is the coercion primitive of type (α → β) → α xrec → β xrec, and set1 and test1 are constructors and deconstructors of the extensible record type.

The neat thing, I think, is that you can write the refinement as a datatype, just about the exact style you'd want to; I was afraid I would have to resort to writing S and K combinators to hack up a representation of type functions to hit with some internalization of mu, or something scary like that.
Tags: ml, phantom types, wanking

  • (no subject)

    Some further progress cleaning up the https://xkcd.com/1360/ -esque augean stables that is my hard drive. Tomato chicken I made a couple days ago…

  • (no subject)

    Did some personal archaeology. Helped a little with laundry. Threw some chicken, onions, tomato, stock, peppers in the slow cooker and hopefully…

  • (no subject)

    Dinner with akiva and dannel at nuevo portal in carroll gardens. Ate a pile of chicken stew and rice and beans and maduros, good times. I do miss…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded