[Caml-list] Polymorphic recursion and GADTs

[Caml-list] Polymorphic recursion and GADTs

[Lukasz Stafiniak]

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

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: 4350 bytes --]

Re: [Caml-list] Polymorphic recursion and GADTs

[Lukasz Stafiniak]

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

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.)
> [...]
> Now to a more complex example.
>

In the complex example, the problem is not the difference between ['a.]
syntax and [type a.] syntax, but polymorphic recursion and GADTs in OCaml
generally. What type annotations do I need to provide?

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

Re: [Caml-list] Polymorphic recursion and GADTs

[Gabriel Scherer]

[-- 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 --]

Re: [Caml-list] Polymorphic recursion and GADTs

[Lukasz Stafiniak]

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

The annotation needs to be directly at the "function" node:

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))
    : ((a, b) meet -> (a, b) nearby))
      (compare x goal))

Regarding the first part, thanks to Gabriel, that explained it to me.

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

> 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.)
>> [...]
>> Now to a more complex example.
>>
>
> In the complex example, the problem is not the difference between ['a.]
> syntax and [type a.] syntax, but polymorphic recursion and GADTs in OCaml
> generally. What type annotations do I need to provide?
>

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

Re: [Caml-list] Polymorphic recursion and GADTs

[Lukasz Stafiniak]

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

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

> The annotation needs to be directly at the "function" node:
>
>
Even better: no (additional) annotation is needed if I export the
beta-redex as a match clause.

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

Re: [Caml-list] Polymorphic recursion and GADTs

[Lukasz Stafiniak]

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

On Tue, Dec 10, 2013 at 2:20 PM, Lukasz Stafiniak <lukstafi@gmail.com>wrote:

> On Mon, Dec 9, 2013 at 10:34 PM, Lukasz Stafiniak <lukstafi@gmail.com>wrote:
>
>> The annotation needs to be directly at the "function" node:
>>
>>
> Even better: no (additional) annotation is needed if I export the
> beta-redex as a match clause.
>
*as a match expression

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

Re: [Caml-list] Polymorphic recursion and GADTs

[Lukasz Stafiniak]

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

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

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

Re: [Caml-list] Polymorphic recursion and GADTs

[Gabriel Scherer]

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

You must not use a type annotation here ('t47), because its (implicit)
scope is above. Removing the annotation or using _ in lieu of the free type
variable solves your problem. See this recent bugreport where the same
question was raised:
  http://caml.inria.fr/mantis/view.php?id=6264


On Tue, Dec 10, 2013 at 3:24 PM, Lukasz Stafiniak <lukstafi@gmail.com>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
>
>

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

Re: [Caml-list] Polymorphic recursion and GADTs

[Jacques Garrigue]

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

Re: [Caml-list] Polymorphic recursion and GADTs

[Lukasz Stafiniak]

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

On Tue, Dec 10, 2013 at 11:43 PM, Jacques Garrigue <
garrigue@math.nagoya-u.ac.jp> wrote:

>
> 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:
>
> I realized that after posting :-)


>
> 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.
>
> I do not need it, I am just exploring ways of outputting that information
in case someone would find it useful (under the big conditional that
someone would find InvarGenT useful in the first place, rather than just
cool...)

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

Re: [Caml-list] Polymorphic recursion and GADTs

[Lukasz Stafiniak]

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

On Tue, Dec 10, 2013 at 11:51 PM, Lukasz Stafiniak <lukstafi@gmail.com>wrote:

>
>> I do not need it, I am just exploring ways of outputting that information
> in case someone would find it useful (under the big conditional that
> someone would find InvarGenT useful in the first place, rather than just
> cool...)
>
*under the big counterfactual
*rather than merely cool

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