Jason (jcreed) wrote,

Yesterday in HOT we were talking about the ML type exn, which Karl Crary taught us to pronounce not as "EXceptioN" --- the type of which, historically, is what it really is --- but as "EXteNsible", for extensible sum types are a perfectly valid thing even apart from the exception control flow mechanism. I had known this for some time, but daydreaming in the back of class I wondered if one could dually make sense out of extensible product types --- some sort of dynamically extensible record type thingy.

It turns out you can! I'm not sure if it's really the canonical answer, but it certainly makes some sense, and you can even hack them up in ML, basing them off the existing exn type. The idea is that you can generate new tags at runtime and build records with fields labelled by these tags.

As an extra bonus, over lunch today tom7 showed me how phantom types can be cleverly used to simulate row polymorphism. I made one small (I think) improvement, using the built-in product type instead of an abstract type of phantom conjunctions. This means writing the necessary static coercions requires no brainpower to generate the appropriate tangle of combinators. You just write the old shape as a tuple pattern, and the new shape as a tuple, and it works.

Here, then, is the code for "Phantom Extensible Products": (One small caveat; I suspect strongly in the absence of full understanding that putting a functor inside a structure means I am doing "higher-order modules" even though taking a tuple of a function doesn't really increase the order. NJ seems to love this shit, but Idunno what other compilers do. Anyone know if there's a way around having to do things this way?)

signature PXPROD =
    type 'c xrec
    type ('a,'b) tag

    val empty : unit xrec

    (* "safe set" --- tracks the added field in the type *)
    val sset : 'c xrec -> ('a,'b) tag -> 'a -> ('b * 'c) xrec
    (* "unsafe set" --- forgets that it was added. Not really
     unsafe per se, but I can't think of a better name. Its
     forgetting of the addition does not contribute to safety,
     anyhow. *)
    val uset : 'c xrec -> ('a,'b) tag -> 'a ->       'c  xrec

    val spi : ('b * 'c) xrec -> ('a,'b) tag -> 'a
    (* "safe projection" --- if we provide evidence that the
    record contains a certain field, we get its data
    unqualified *)
    val upi :       'c  xrec -> ('a,'b) tag -> 'a option
    (* "unsafe projection" --- if we have no such evidence,
    we can at least get out maybe SOME of its data, or NONE *)
    val coerce : ('c -> 'd) -> 'c xrec -> 'd xrec

signature TAG =
    type content
    type ('a,'b) tag
    type stag
    val dtag : (content, stag) tag

signature PXP =

type ('a,'b) tag

structure Pxprod : PXPROD
  where type ('a,'b) tag = ('a,'b) tag

functor NewTag(type content) : TAG
  where type content = content 
  where type ('a,'b) tag = ('a,'b) tag 


structure Pxp :> PXP = 
type ('a,'b) tag = ('a -> exn) * (exn -> 'a option)

structure Pxprod =
type 'c xrec = exn list
type ('a,'b) tag = ('a,'b) tag

val empty = []
fun sset d (ti,tt) x = (ti x) :: d
val uset = sset

fun upi (h::tl) (ti,tt) = (case (tt h) of SOME x => SOME x
					  | NONE => upi tl (ti,tt))
  | upi [] t = NONE
fun spi xrec t = Option.valOf (upi xrec t)

fun coerce f x = x


functor NewTag(type content) =
type content = content
type ('a,'b) tag = ('a,'b) tag
type stag = unit
val dtag : (content, stag) tag =  
	exception E of content
	(E, (fn y => ((raise y) handle E x => SOME x) handle _ => NONE))


structure Test =
open Pxp
open Pxprod

structure I = NewTag(type content = int)    
structure S = NewTag(type content = string) 
structure R = NewTag(type content = real)
structure B = NewTag(type content = bool)

val R = R.dtag
val I = I.dtag
val S = S.dtag
val B = B.dtag

val r = empty

val r = sset r I 601
val r = sset r S "foo"
val r = sset r B false
val r = sset r R 3.14
val r = uset r R 2.17
val r = uset r S "bar"

fun drop r = coerce (fn (x,y) => y) r
fun arrange r = coerce (fn (r,(b,(s,(i,x)))) => (b,(i,(s,x)))) r

(* val assemble : (B.stag * (I.stag * (S.stag * 'a))) xrec
		  -> (bool * int * string * real option) *)
fun assemble x = (spi x B,
		  spi (drop x) I,
		  spi (drop (drop x)) S,
		  upi x R)

val result = assemble (coerce arrange r)


Tags: crazy, extensible, programming, records, sml

  • (no subject)

    K's off at an atypically Saturdayish Type-Thursday event, so I stuck around the apartment hiding from 100-degree heat, and noodled around with…

  • (no subject)

    Playing around with the agda javascript backend, now. Like, my ears are popping from the sudden change of type-theory-pressure.

  • (no subject)

    https://deadlockempire.github.io is a very cute edutainment game, meant to teach people about deadlocks and race conditions and concurrency…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded