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
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
