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

[Goswin von Brederlow <goswin-v-b@web.de>]

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