Expressing subrecord constraints
From Impredicative Wiki
It is possible to use the disjointness constraints [a ~ b] and symmetric concatenation a ++ b of the Ur/Web record calculus to express record subtype constraints.
(* Here the Ur/Web compiler infers the evidence ( the "extension" below ) which shows the value x has a record subtype of super *) fun subrecordWitness [super :: {Type}] [extension ::: {Type}] [super ~ extension] (fl : folder super) (x : $(super ++ extension)) = @@fold [fn (r :: {Type}) => [r ~ extension] => $(r ++ extension) -> $r] (fn [nm :: Name] [t :: Type] [r :: {Type}] [[nm] ~ r] (acc : [r ~ extension] => $(r ++ extension) -> $r) [[nm = t] ++ r ~ extension] => fn (rn : $([nm = t] ++ r ++ extension)) => {nm = rn.nm} ++ acc(rn -- nm)) (fn [[] ~ extension] (x : $extension) => {}) [super] fl ! x con supertype :: {Type} = [One = string, Two = int] val v : $supertype = subrecordWitness [supertype] {One = "foo", Two = 2, Three = "bar"} fun main () = return <xml> <head> <title>Subrecord Constraint Witness</title> </head> <body> <h1>Illustracion of subrecord constraint witness</h1> <p> It is possible using the disjointness constraint and symmetric concatenation of Ur/Web to express subrecord constraints. </p> </body> </xml>