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 endand 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 endSome 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.