[Caml-list] Type inference curiosity

[Caml-list] Type inference curiosity

[Grumpy]

Hello,

I think there is an incoherency or a bug somewhere in the type inference
engine with the following code with version 4.02.3 (I have not tested in
previous versions). Both functions eval and eval2 are identical but the
inferred types are different, and the type inferred for eval2 is
actually wrong.

The function eval is typed correcly ('a exp -> 'a) while the type
inferred for funcion function eval2 is (int exp -> int), which is wrong
because of the Inc case returning ('a exp -> 'a).

It seems the syntax (type a) leads to this incorrect behaviour...


type _ exp =
  | Stop : int exp
  | Inc : (int exp -> int) exp

let rec eval : type a. a exp -> a = function
  | Stop -> 0
  | Inc -> (fun (p : int exp) -> 1 + eval p)

let rec eval2 (type a) (p : a exp) : a =
  match p with
  | Stop -> 0
  | Inc -> (fun (p : int exp) -> 1 + eval2 p)

Re: [Caml-list] Type inference curiosity

[Nicolás Ojeda Bär]

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

Hello,

Recursive definitions need to be explicitly annotated to be polymorphic.
The (type a) annotation
introduces an abstract type a in the body of the function but does not make
it polymorphic.
The annotation type a. on the other hand, does both.

See http://caml.inria.fr/pub/docs/manual-ocaml/extn.html#sec227 for the
details.

Cheers,
Nicolas


On Fri, Mar 24, 2017 at 10:20 AM, Grumpy <grumpy@drno.eu> wrote:

> Hello,
>
> I think there is an incoherency or a bug somewhere in the type inference
> engine with the following code with version 4.02.3 (I have not tested in
> previous versions). Both functions eval and eval2 are identical but the
> inferred types are different, and the type inferred for eval2 is
> actually wrong.
>
> The function eval is typed correcly ('a exp -> 'a) while the type
> inferred for funcion function eval2 is (int exp -> int), which is wrong
> because of the Inc case returning ('a exp -> 'a).
>
> It seems the syntax (type a) leads to this incorrect behaviour...
>
>
> type _ exp =
>   | Stop : int exp
>   | Inc : (int exp -> int) exp
>
> let rec eval : type a. a exp -> a = function
>   | Stop -> 0
>   | Inc -> (fun (p : int exp) -> 1 + eval p)
>
> let rec eval2 (type a) (p : a exp) : a =
>   match p with
>   | Stop -> 0
>   | Inc -> (fun (p : int exp) -> 1 + eval2 p)
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

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

Re: [Caml-list] Type inference curiosity

[Grumpy]

This does not explain why the compiler accepts as well typed the
function eval2, after inferring a = int from the first branch.
Do I miss something ?

Le 24/03/2017 à 10:55, Nicolás Ojeda Bär a écrit :
> Hello,
> 
> Recursive definitions need to be explicitly annotated to be
> polymorphic.  The (type a) annotation
> introduces an abstract type a in the body of the function but does not
> make it polymorphic.
> The annotation type a. on the other hand, does both.
> 
> See http://caml.inria.fr/pub/docs/manual-ocaml/extn.html#sec227
> <http://caml.inria.fr/pub/docs/manual-ocaml/extn.html#sec227> for the
> details.
> 
> Cheers,
> Nicolas
> 
> 
> On Fri, Mar 24, 2017 at 10:20 AM, Grumpy <grumpy@drno.eu
> <mailto:grumpy@drno.eu>> wrote:
> 
>     Hello,
> 
>     I think there is an incoherency or a bug somewhere in the type inference
>     engine with the following code with version 4.02.3 (I have not tested in
>     previous versions). Both functions eval and eval2 are identical but the
>     inferred types are different, and the type inferred for eval2 is
>     actually wrong.
> 
>     The function eval is typed correcly ('a exp -> 'a) while the type
>     inferred for funcion function eval2 is (int exp -> int), which is wrong
>     because of the Inc case returning ('a exp -> 'a).
> 
>     It seems the syntax (type a) leads to this incorrect behaviour...
> 
> 
>     type _ exp =
>       | Stop : int exp
>       | Inc : (int exp -> int) exp
> 
>     let rec eval : type a. a exp -> a = function
>       | Stop -> 0
>       | Inc -> (fun (p : int exp) -> 1 + eval p)
> 
>     let rec eval2 (type a) (p : a exp) : a =
>       match p with
>       | Stop -> 0
>       | Inc -> (fun (p : int exp) -> 1 + eval2 p)
> 
>     --
>     Caml-list mailing list.  Subscription management and archives:
>     https://sympa.inria.fr/sympa/arc/caml-list
>     <https://sympa.inria.fr/sympa/arc/caml-list>
>     Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>     <http://groups.yahoo.com/group/ocaml_beginners>
>     Bug reports: http://caml.inria.fr/bin/caml-bugs
>     <http://caml.inria.fr/bin/caml-bugs>
> 
> 

Re: [Caml-list] Type inference curiosity

[Jacques Garrigue]

On 2017/03/24 19:13, Grumpy wrote:
> 
> This does not explain why the compiler accepts as well typed the
> function eval2, after inferring a = int from the first branch.
> Do I miss something ?

What is happening here is that the typing for (type a) is different internally
and externally. Inside the function, a is a locally abstract type, which
can be refined both in int and (int exp -> int).
Outside, it is a (not yet generalized) type variable.
The recursive call forces this type variable to be unified with int, with no
impact on the internal view. It works because there is only one recursive
call. All this is perfectly sound.
I admit this is confusing, so writing recursive function types as in eval is the right way.

Jacques

> Le 24/03/2017 à 10:55, Nicolás Ojeda Bär a écrit :
>> Hello,
>> 
>> Recursive definitions need to be explicitly annotated to be
>> polymorphic.  The (type a) annotation
>> introduces an abstract type a in the body of the function but does not
>> make it polymorphic.
>> The annotation type a. on the other hand, does both.
>> 
>> See http://caml.inria.fr/pub/docs/manual-ocaml/extn.html#sec227
>> <http://caml.inria.fr/pub/docs/manual-ocaml/extn.html#sec227> for the
>> details.
>> 
>> Cheers,
>> Nicolas
>> 
>> 
>> On Fri, Mar 24, 2017 at 10:20 AM, Grumpy <grumpy@drno.eu
>> <mailto:grumpy@drno.eu>> wrote:
>> 
>>   Hello,
>> 
>>   I think there is an incoherency or a bug somewhere in the type inference
>>   engine with the following code with version 4.02.3 (I have not tested in
>>   previous versions). Both functions eval and eval2 are identical but the
>>   inferred types are different, and the type inferred for eval2 is
>>   actually wrong.
>> 
>>   The function eval is typed correcly ('a exp -> 'a) while the type
>>   inferred for funcion function eval2 is (int exp -> int), which is wrong
>>   because of the Inc case returning ('a exp -> 'a).
>> 
>>   It seems the syntax (type a) leads to this incorrect behaviour...
>> 
>> 
>>   type _ exp =
>>     | Stop : int exp
>>     | Inc : (int exp -> int) exp
>> 
>>   let rec eval : type a. a exp -> a = function
>>     | Stop -> 0
>>     | Inc -> (fun (p : int exp) -> 1 + eval p)
>> 
>>   let rec eval2 (type a) (p : a exp) : a =
>>     match p with
>>     | Stop -> 0
>>     | Inc -> (fun (p : int exp) -> 1 + eval2 p)
>> 
>>   --
>>   Caml-list mailing list.  Subscription management and archives:
>>   https://sympa.inria.fr/sympa/arc/caml-list
>>   <https://sympa.inria.fr/sympa/arc/caml-list>
>>   Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>>   <http://groups.yahoo.com/group/ocaml_beginners>
>>   Bug reports: http://caml.inria.fr/bin/caml-bugs
>>   <http://caml.inria.fr/bin/caml-bugs>