[Ur] type system expressivity

[Adam Chlipala]

Here's a quick example.  I was a bit surprised at the need to invoke 
[sourcify_list] directly in the example at the end, but it seems like a 
clear step up compared to your manual implementation.


structure Sourcify : sig
     class sourcify :: Type -> Type -> Type

     val mkSourcify : t1 ::: Type -> t2 ::: Type -> (t1 -> transaction 
t2) -> sourcify t1 t2
     val sourcify : t1 ::: Type -> t2 ::: Type -> sourcify t1 t2 -> t1 
-> transaction t2
end = struct
     class sourcify = fn t1 t2 => t1 -> transaction t2

     fun mkSourcify [t1] [t2] (x : t1 -> transaction t2) = x
     fun sourcify [t1] [t2] (f : t1 -> transaction t2) x = f x
end

open Sourcify

val sourcify_int : sourcify int _ = mkSourcify source
val sourcify_float : sourcify float _ = mkSourcify source
val sourcify_string : sourcify string _ = mkSourcify source

fun sourcify_list [t1] [t2] (_ : sourcify t1 t2) : sourcify (list t1) 
(list t2) =
     mkSourcify (List.mapM sourcify)

fun sourcify_record [r ::: {(Type * Type)}] (fl : folder r) (s : $(map 
(fn (t1, t2) => sourcify t1 t2) r))
     : sourcify $(map fst r) $(map snd r) =
     mkSourcify (@Monad.mapR2 _ [fn (t1, t2) => sourcify t1 t2] [fst] [snd]
                  (fn [nm ::_] [t ::_] f x => @sourcify f x) fl s)


(* Test case *)

type test = {A : int, B : float, C : list string}

val sourcify_list_string : sourcify (list string) _ = sourcify_list
val sourcify_test : sourcify test _ = sourcify_record
val sourcify_list_test : sourcify (list test) _ = sourcify_list

val f : list test -> _ = sourcify