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: