Expressing subrecord constraints

From Impredicative Wiki
Jump to: navigation, search

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>
Personal tools