Re: [Caml-list] GADTs and JSON

[Rodolphe Lepigre <rodolphe.lepigre@univ-savoie.fr>]

Hi,

> Is it possible to encode a recursive, heterogenous map and list datastructure
> with GADTs?
> 
> I want to encode JSON (there are already a couple of great libraries out there
> so this is kind of an academic question). I would like to have functions that
> can only take a JSON map type, for example to take a json map and return a
> value. The key here is that the map can hold values of type int,string and also
> maps. Is this possible?
> 
> eg get : (map : map json) -> key:string -> 'a json
> 
> Thank you.
> 
> Trevor

You should probably have a look at the examples given for GADTs on the page
about language extensions (advanced examples section):

http://caml.inria.fr/pub/docs/manual-ocaml-400/manual021.html#toc85

Not so long ago I used equality types to encode collections of object of
different types. Here is an example with lists and a function for obtaining
the n-th element.

##########
type (_,_) eq = Eq : ('a,'a) eq

type 'a typ =
  | Int   : int typ
  | Float : float typ
  | Pair  : 'a typ * 'b typ -> ('a * 'b) typ

let rec equal : type a b. a typ -> b typ -> (a,b) eq option = fun t1 t2 ->
  match (t1,t2) with
  | (Int       , Int      ) -> Some Eq
  | (Float     , Float    ) -> Some Eq
  | (Pair(a,b) , Pair(c,d)) ->
      begin
        match (equal a c, equal b d) with
        | (Some Eq, Some Eq)  -> Some Eq 
        | _                   -> None
      end
  | _                       -> None

type _ tlist' =
  | Nil  : unit tlist'
  | Cons : ('a typ * 'a * unit tlist') -> unit tlist'

type tlist = unit tlist'

let rec nth : type a. tlist -> int -> a typ -> a = fun l n ty ->
  match (l, n) with
  | (Nil          , _) -> raise Not_found
  | (Cons(ty',t,_), 0) ->
      begin
        match equal ty ty' with
        | Some Eq -> t
        | None    -> invalid_arg "Ill type in nth"
      end
  | (Cons(_,_,l)  , _) -> nth l (n-1) ty

let l = Cons(Int, 3, Cons(Float, 4.2, Nil))

let n : int   = nth l 0 Int
let f : float = nth l 1 Float
##########

Regards,

Rodolphe

-- 
Rodolphe Lepigre
LAMA, Université de Savoie, FRANCE
http://lama.univ-savoie.fr/~lepigre/