I was working with GADT (where all is so strongly typed… which is first painful then gives satisfaction).
Going back to a case with ADT type, I felt surprised not to be able to answer to the following question (when pattern matching): how to recognize the primitive type of an OCaml value?
Let’s take a simple (non GADT) example:
type t = A of string * string
| B of string * int
val f : string -> 'a -> t
let f (x:string) (y:'a) : t =
match a with
| (* int pattern *) -> A (x, b)
| (* string pattern *) -> B (x, b)
How can we recognize the primitive type of the arguments?
Is there a function such as the #show_val
directive called in the Toplevel:
let a = "foo";;
#show_val a
(* val a : string *)
As a pattern matching can’t take an int on a branch and a string on another (two different types), my question is weird and reveals that I should obviously be missing something.
let f x = match x with 1 -> true | "a" -> false
^^^
Error: This pattern matches values of type string
but a pattern was expected which matches values of type int
A simplified GADT example (with no problem as arguments are easily pattern matched) would be:
type t = A of string * string
| B of string * int
type _ expr =
| String : string -> string expr
| Int : int -> int expr
| T : t -> t expr
| Foo : string * 'a expr -> t expr
let rec eval : type a. a expr -> a = function
| String x -> x
| Int x -> x
| T x -> x
| Foo (x, String y) -> A (x, y)
| Foo (x, Int y) -> B (x, y)
| _ -> failwith "not a valid expression"
I’m surprised to be in trouble with simple ADT case as I begin to be comfortable with GADT!
It looks like I’m trying to use GADT pattern on ADT…
EDIT: the question can also be: “How to do with ADT the above GADT example ?”