Re: [Caml-list] Type inference curiosity

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

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>