Re: [Caml-list] Confusing behaviour of type inference for polymorphic classes.

[Dmitri Boulytchev <dboulytchev@gmail.com>]

> I think this is caused by the recursion. The type inference assumes
> that the recursive call will have the same type as the parent. Since
> you switch 'a and 'b in the recursive call the compiler inferes that
> 'a == 'b.
>
     I don't think we have a recursive call here since we call
a method from *another* object.

     BR,
     DB

> On Mon, Dec 02, 2013 at 01:33:55AM +0400, Dmitri Boulytchev wrote:
>>      Hello everyone,
>>
>>      I stumbled on the following confusing behaviour of the type
>> checker: given the definitions
>>
>>      type ('a, 'b) t =
>>         A of 'a * ('b, 'a) t
>>       | B of 'a
>>
>>     class ['a, 'b, 'ta, 'tb] m =
>>       object
>>         method t : ('a -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t -> ('ta,
>> 'tb) t =
>>           fun fa fb s ->
>>             match s with
>>             | A (a, bat) -> A (fa a, (new m)#t fb fa bat)
>>             | B  a       -> B (fa a)
>>       end
>>
>>      the following type is inferred for the class m:
>>
>>      class ['a, 'b, 'ta, 'c] m :
>>        object
>>          constraint 'b = 'a  <--- why?
>>          constraint 'c = 'ta <--- why?
>>          method t : ('a -> 'ta) -> ('a -> 'ta) -> ('a, 'a) t -> ('ta, 'ta) t
>>        end
> I think this is caused by the recursion. The type inference assumes
> that the recursive call will have the same type as the parent. Since
> you switch 'a and 'b in the recursive call the compiler inferes that
> 'a == 'b.
>
>>     Perhaps some explicit annotation is needed here (like that for
>> the polymorphic recursion
>> for functions).
>>     I found the following workaround: first we abstract the instance
>> creation ("new m") away:
>>
>>     class ['a, 'b, 'ta, 'tb] m' f =
>>       object
>>         method t : ('a -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t -> ('ta,
>> 'tb) t =
>>           fun fa fb s ->
>>             match s with
>>             | A (a, bat) -> A (fa a, (f ())#t fb fa bat)
>>             | B  a       -> B (fa a)
>>       end
>>
>>    which gives us the unconstrained type
>>
>>     class ['a, 'b, 'ta, 'tb] m' :
>>          (unit ->
>>           < t : ('b -> 'tb) -> ('a -> 'ta) -> ('b, 'a) t -> ('tb,
>> 'ta) t; .. >) ->
>>           object
>>             method t : ('a -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t ->
>> ('ta, 'tb) t
>>           end
>>
>>    Then we construct the instance creation explicitly polymorphic function:
>>
>>     let rec f : 'a 'b 'ta 'tb . unit -> <t : ('a -> 'ta) -> ('b ->
>> 'tb) -> ('a, 'b) t -> ('ta, 'tb) t> =
>>       fun () -> new m' f
>>
>>   and finally the class we're looking for:
>>
>>     class ['a, 'b, 'ta, 'tb] m = ['a, 'b, 'ta, 'tb] m' f
>>
>>     The complete annotated source file is attached.
>>     This workaround however does not solve everything: we cannot
>> actually inherit
>> from the m since it calls hardcoded "new m"; we should inherit from
>> m' (with additional parameter)
>> instead and "tie the knot" on the toplevel.
>>      Are there better solutions? Please help :)
> Try using a self type or #m but this might not be solvable.
>   
>>      Best regards,
>>      Dmitry Boulytchev,
>>      St.Petersburg State University,
>>      Russia.
> MfG
> 	Goswin
>