Map GADT type specification to function arguments

gadt

#1

Hi,

You probably know how many of the commandline parsers in OCaml work: you construct a “specification” which then leads to a function which has the same signature as the specification implied. For example Cmdliner.

I have created such a specification type in this gist with some help, and I seems to be able to compose String and Int to get the proper String -> Int etc. signatures. But I am struggling on how to write the function which handles the decoding. The decode_elem function does not type for obvious reasons and I am unsure how to tackle that to begin with.

Needless to say, I’m a GADT newbie. I was told that Farfadet does something similar, but it also does a lot more than that and it is tricky for me to condense it to a smaller example.

Any help is appreciated!


#2

I haven’t had a chance to look at the rest, but for decode_elem you need some annotation:

let decode_elem : type a. a elem -> (string -> a) = function
  | String -> fun x -> x
  | Int -> int_of_string

#3

Oh wow, that works indeed! I wasn’t aware that the type system even allows that.


#4

It is explained in the OCaml documentation.