(no title)

Notes from a Medium-Sized Island

Jason

[	website	\|	My Website	]
[	userinfo	\|	livejournal userinfo	]
[	archive	\|	journal archive	]

[Nov. 7th, 2005|05:40 pm]

Jason

[

Tags

ml, phantom types, wanking

]

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

sig
 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
end

and implement it with

struct
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
end

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.

Link

Comments:

From:

ex_trurl
2005-11-07 11:42 pm (UTC)

Not to be a pain or anything, but I'm not sure that your example really illustrates the utility of xrec well. I mean if I just wanted the above I could have just used

datatype even = Zero
              | Even of odd
and       odd = Odd of even

and define the operations as one would expect. I guess it would be useful to see how your example could be leveraged in an extensible fashion.

(Reply) (Thread)

From:

jcreed
2005-11-08 04:39 am (UTC)

Well, the point is that you can name however many different refinements you want over the same data structure and the coercions have no dynamic content.

so I could write
datatype nat = NatZero of Z | NatSucc of Nat S
and then write (assuming I put in a map function for the NewXTag functor as I neglected to do; say smap : ('a -> 'b) -> 'a S.stag -> 'b S.stag)

fun staticEvenToNat (Succ (x : odd S)) = NatSucc(smap staticOddToNat odd)
 |  staticEvenToNat Zero = NatZero
and staticOddToNat (x : even S) = NatSucc(smap staticEvenToNat x)

which is a proof that the even and odd refinements are subrefinements of the trivial refinement on nats (although this is still a nontrivial refinement on the larger type xrec!) and then I can do something like

(* val evenToNat : even xrec -> nat xrec *)
fun evenToNat e = coe EvenToNat e

which is operationally equivalent to the identity function.

(Reply) (Parent) (Thread)

From:

jcreed
2005-11-08 04:40 am (UTC)

The identity function, I should say, on the type that 'a xrec is defined to be for all values of the phantom type 'a, which happens to be in my implementation exn list

(Reply) (Parent) (Thread)

From:

jcreed
2005-11-08 04:41 am (UTC)

Er, so, the reason I used that as an example was just to show I could do a nontrivial refinement at all.

(Reply) (Parent) (Thread)