Re: [Caml-list] Polymorphic recursion and GADTs

[Gabriel Scherer <gabriel.scherer@gmail.com>]

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

TL;DR: you should use those "rigid variables" to annotate type variable
that will be refined in a GADT pattern matching.

The way GADT type variables can be refined with different types in each
branches is different and orthogonal to the type unification mechanism.
Variables ('a) use type unification on each branch, which fails with the
error you observe. Local type constructors (a), and only them, can be
refined in GADT clauses, so that type refinement works. The syntax
  let rec f : type a . a -> ... = fun x -> ...
as opposed to
  let rec f (type a) (x : a) ... = ...
combines the GADT-readiness of those weird variables with polymorphic
recursion -- which is orthogonal, but in practice they often come together.

For more technical details, see "Ambivalent types for type inference with
GADTs", by Jacques Garrigue and Didier Rémy, 2013:
http://gallium.inria.fr/~remy/gadts/Garrigue-Remy:gadts@short2013.pdf


On Mon, Dec 9, 2013 at 6:16 PM, Lukasz Stafiniak <lukstafi@gmail.com> wrote:

> Hello,
>
> I am at a loss as to the difference between ['a.] syntax and [type a.]
> syntax of introducing polymorphic recursion. I will provide some examples.
> (Bear with me, they are automatically generated.)
> >>>
> 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
> 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 : '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))
> <<<
> The above produces:
> Error: This pattern matches values of type boolean term
>        but a pattern was expected which matches values of type integer term
>        Type boolean is not compatible with type integer
> but if we replace the corresponding line with:
> >>>
> ...
> let rec eval : type a . (a term -> a) =
> ...
> <<<
> then it compiles fine.
>
> Now to a more complex example. According to my understanding (and
> InvarGenT), the following code should type-check:
> >>>
> type _ place =
>   | LocA : a place
>   | LocB : b place
> and a
> and b
>
> type (_, _) nearby =
>   | Here : (*∀'b.*)'b place * 'b place -> ('b, 'b) nearby
>   | Transitive : (*∀'a, 'b, 'c.*)('a, 'b) nearby * ('b, 'c) nearby ->
>     ('a, 'c) nearby
> type boolean
>
> external is_nearby : (('a, 'b) nearby -> boolean) = "is_nearby"
> type _ ex1 =
>   | Ex1 : (*∀'a, 'b.*)('b place * ('a, 'b) nearby) -> 'a ex1
> external wander : ('a place -> 'a ex1) = "wander"
> type (_, _) meet =
>   | Same : (*∀'b.*) ('b, 'b) meet
>   | NotSame : (*∀'a, 'b.*) ('a, 'b) meet
> external compare : ('a place -> 'b place -> ('a, 'b) meet) = "compare"
> let rec walk : type a b . (a place -> b place -> (a, b) nearby) =
>   (fun x goal ->
>     ((function Same -> Here (x, goal)
>        | NotSame ->
>            let Ex1 ((y, to_y)) = wander x in Transitive (to_y, walk y
> goal)))
>       (compare x goal))
> <<<
> Here we get
> Error: This expression has type b place
>        but an expression was expected of type a place
>        Type b is not compatible with type a
> And when we switch to the ['a.] syntax, we get
> Error: This definition has type 'a. 'a place -> 'a place -> ('a, 'a) nearby
>        which is less general than
>          'a 'b. 'a place -> 'b place -> ('a, 'b) nearby
>
> Thanks in advance for any thoughts.
> If you are curious, the source code is:
> https://github.com/lukstafi/invargent/blob/master/examples/simple_eval.gadt
>
> https://github.com/lukstafi/invargent/blob/master/examples/equational_reas.gadt
>
>

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