[Caml-list] GADTs and JSON

[Caml-list] GADTs and JSON

[Trevor Smith]

[-- Attachment #1: Type: text/plain, Size: 507 bytes --]

Hello,

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

[-- Attachment #2: Type: text/html, Size: 659 bytes --]

Re: [Caml-list] GADTs and JSON

[Milan Stanojević]

You must have 'a in the input if you want to return 'a json (at least
a non-empty one). Same way you can't have function unit -> 'a list
that returns a non-empty list.

But it is probably not hard for you to create a witness type and have
that in input.
For example
eg get:(map : map json) -> key:string -> 'a witness -> 'a json option

You get None if key is not there or if it is not of the expected type.



On Thu, May 21, 2015 at 5:42 PM, Trevor Smith
<trevorsummerssmith@gmail.com> wrote:
> Hello,
>
> 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

Re: [Caml-list] GADTs and JSON

[Rodolphe Lepigre]

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/