Using GADT to model records that share some of their fields

Learning
4

@raphael-proust : once you have lifted the option to the type level with

type nothing = private Nothing_tag
type just = private Just_tag
type ('a,'b) opt =
  | Nothing: ('a, nothing) opt
  | Just: 'a -> ('a, just) opt

it is possible to keep the direct definition of the record with a constraint, rather than adding another layer of GADTs

type x type y type z type w
type 'p r = {
  x:x;
  y:y;
  z:(z, 'z_status) opt;
  w:(w, 'w_status) opt
}
constraint 'p =  <z:'z_status; w:'w_status>

then the get on opt is a total function that we can define once

let get (Just x) = x

while still being able to write functions that work with either Just or Nothing:

let f (type a) (x: <z:a; ..> r) =
  get x.w,
  match x.z with
  | Just z -> Some z
  | Nothing -> None

In particular, it also means that we can validate once the presence of a field:

type (_,_) eq = Refl:('a,'a) eq

let present (type a elt) (x: (elt,a) opt) : (a,just) eq option =
match x with
  | Just _ -> Some Refl
  | Nothing -> None

let test (type a b) (r: <z:a; w:b > present) = 
  match present r.w, present r.z with
  | Some Refl, Some Refl −>
    (* in this branch and only in this branch,
       we know that `w` and `z` are present *) 
    Some (get r.w, get r.z)
  | _ -> None

An important point is that here we are using an object type to (ab)use the fact that “method” names are commutative and we don’t have to remember the position of the z or w “method” in the object type.

8 Likes