Re: [Caml-list] Polymorphic recursion and GADTs

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2013/12/11 01:24, Lukasz Stafiniak wrote:

> I have another challenge for you. Without the redundant annotations (i.e. with only an annotation on let-rec) it type-checks nicely. I am providing more annotations as an option.
> >>>
> type _ term =
>   | Lit : integer -> integer term
>   | Plus : integer term * integer term -> integer term
>   | IsZero : integer term -> boolean term
>   | If : (*∀'a.*)boolean term * 'a term * 'a term -> 'a term
>   | Pair : (*∀'a, 'b.*)'a term * 'b term -> (('a * 'b)) term
>   | Fst : (*∀'a, 'b.*)(('a * 'b)) term -> 'a term
>   | Snd : (*∀'a, 'b.*)(('a * 'b)) term -> 'b term
> and integer
> and boolean
>   
> external plus : (integer -> integer -> integer) = "plus"
> external is_zero : (integer -> boolean) = "is_zero"
> external if_then : (boolean -> 'a -> 'a -> 'a) = "if_then"
> let rec eval : type a . (a term -> a) =
>   ((function Lit i -> i | IsZero x -> is_zero (eval x)
>     | Plus (x, y) -> plus (eval x) (eval y)
>     | If (b, t, e) -> if_then (eval b) (eval t) (eval e)
>     | Pair (x, y) -> (eval x, eval y)
>     | Fst p -> let ((x, y): (a * 't47)) = eval p in x
>     | Snd p -> let ((x, y): ('t59 * a)) = eval p in y): a term -> a)
> <<<
> We get at "eval p" to the right of "let ((x, y): (a * 't47))":
> Error: This expression has type a * b#0
>        but an expression was expected of type a * b#0
>        The type constructor b#0 would escape its scope

As always, Gabriel's answer is correct, but I have two remarks.
First, concerning your first example where you needed annotations on the local function,
you can actually avoid that by using pattern matching rather than function application:

let rec walk : type a b . (a place -> b place -> (a, b) nearby) =
  fun x goal ->
  match compare x goal with
  | Same -> Here (x, goal)
  | NotSame ->
      let Ex1 ((y, to_y)) = wander x in Transitive (to_y, walk y goal)

Now, for the above example, of course you don't need to annotate the "function" construct,
but if you want to name the rigid variables 't47 and 't59, you can do that through eta-expansion:

let rec eval : type a . (a term -> a) =
  function Lit i -> i | IsZero x -> is_zero (eval x)
    | Plus (x, y) -> plus (eval x) (eval y)
    | If (b, t, e) -> if_then (eval b) (eval t) (eval e)
    | Pair (x, y) -> (eval x, eval y)
    | Fst p -> (fun (type b) p -> let ((x, y): (a * b)) = eval p in x) p
    | Snd p -> (fun (type b) p -> let ((x, y): (b * a)) = eval p in y) p

Not very clean, so we need to do something about it.

	Jacques