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

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

[Dmitri Boulytchev]

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

     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

    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 :)

     Best regards,
     Dmitry Boulytchev,
     St.Petersburg State University,
     Russia.



[-- Attachment #2: sample.ml --]
[-- Type: text/x-ocaml, Size: 1471 bytes --]

type ('a, 'b) t = 
    A of 'a * ('b, 'a) t 
  | B of 'a

(*
   The initial definition

   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

   gives us the following type:

   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
*)

(* The modified version with the "new" abstracted 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

(* Inferred type with no artificial constraints:

   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
*)

(* Instance creation function: *)

let rec f : 'a 'b 'ta 'tb . unit -> <t : ('a -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t -> ('ta, 'tb) t> = 
  fun () -> new m' f

class ['a, 'b, 'ta, 'tb] m = ['a, 'b, 'ta, 'tb] m' f

(* Ok now:
   class ['a, 'b, 'ta, 'tb] m' : ['a, 'b, 'ta, 'tb] m
*)

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

[Goswin von Brederlow]

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

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

[Dmitri Boulytchev]

> 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
>

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

[Goswin von Brederlow]

On Mon, Dec 02, 2013 at 07:05:45PM +0400, Dmitri Boulytchev wrote:
> >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

Different instance but same class and method. The type system is a bit
odd with objects sometimes.
 
MfG
	Goswin

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

[Jeremy Yallop]

Hi Dmitri,

On 1 December 2013 21:33, Dmitri Boulytchev <dboulytchev@gmail.com> wrote:
>     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

There's good news and bad news.  The good news is that the problem can
be solved for your particular example.  The bad news is that the
approach doesn't work in the general case.  On to the details...

First, let's get some definitions out of the way.  A parameterised
type definition "('a1, 'a2, ... 'an) t" is *regular* if all
occurrences of "t" within its definition are instantiated with the
parameters from the lhs of the '=' (i.e. it occurs exactly as "('a1,
'a2, ... 'an) t").  Here are some regular data types definitions:

   type 'a list = Nil | Cons of 'a * 'a listapproach

   type ('a, 'b) altlist = Nil | Cons of 'a * 'b * ('a, 'b) altlist

In each of these the type constructor being defined is only
instantiated with the exact parameter list from the lhs of the '='.

In contrast, here are some non-regular data type definitions:

   type 'a nested = Empty | Branch of 'a * ('a * 'a) nested

   type ('a, 'len) vec =
     Nil : ('a, zero) vec
   | Cons : 'a * ('a, 'n) vec -> ('a, 'n succ) vec

In each of these the type constructor being defined is instantiated
with parameter lists that are different from the lhs of the
definition: "('a * 'a) nested" is different from "'a nested" in the
first case, and "('a, zero) vec" and "('a, 'n succ)" vec are different
from "('a, 'len) vec" in the second case.

The analogue of non-regular types for functions is polymorphic
recursion.  A function is *polymorphic-recursive* if some calls to the
function in its own definition instantiate the type variables
differently from the definition itself.  Here's a polymorphic
recursive function

   let rec depth : 'a. 'a nested -> int = function
     | Empty -> 0
     | Branch (_, n) -> 1 + depth n

The call to "depth" on the last line uses it at type "('a * 'a) nested
-> int", which is different from the defined type "'a nested -> int".
If you call "depth" on a value of type "int nested" of depth 3 then
the recursive calls will have the following types:

   int nested -> int
   (int * int) nested -> int
   ((int * int) * (int * int)) nested -> int
   (((int * int) * (int * int)) * ((int * int) * (int * int))) nested -> int

It's also worth noting that the type annotation can't be omitted,
since polymorphic-recursive types can't be inferred, although they can
be checked.

In contrast, here's a function that's polymorphic and recursive but
not polymorphic-recursive:

  let rec length : 'a. 'a list -> int = function
    | Nil -> 0
    | Cons (_, l) -> 1 + length l

In this case the call to "length" uses it at type "'a list -> int" --
just the same type as the definition.  If you call "length" on a value
of type "int list" of length 3 then the recursive calls will have the
following types:

  int list -> int
  int list -> int
  int list -> int
  int list -> int

In this case the type annotation is unnecessary, and if you omit it
then OCaml will infer the same type, "'a list -> int".

It'll probably come as no surprise that non-regular types and
polymorphic recursion are closely related: traversals over non-regular
types generally involve polymorphic recursion.

In your example the type 't' is non-regular: it's defined to take
parameters "('a, 'b)", but used in its definition as "('b, 'a) t":

>   type ('a, 'b) t =
>      A of 'a * ('b, 'a) t
>    | B of 'a

Traversals over values of type "t" therefore need to be
polymorphic-recursive.  Since you've exposed the type parameters as
class parameters you need the class type to be non-regular as well:
you've defining "m" with parameters "['a, 'b, 'ta, 'tb]", but trying
to instantiate it with parameters "['b, 'a, 'tb, 'ta]".  This isn't
possible in OCaml: class and object types (like other structural types
such as polymorphic variants) can only be regular.  The approach
you're trying therefore won't work in general for defining traversals
over non-regular types.  As you've noted, you can work around the
problem using open recursion and typing the knot yourself, but you
lose the ability to subtype in the process.

On to the good news.  Unlike "nested" and "vec", your type "t" is only
a little bit non-regular.  The non-regularity is a simple flip of the
type parameters, so a recursive traversal of a value of "t" involves
calling the traversal function at the following types

   ('a, 'b) t -> 'result
   ('b, 'a) t -> 'result
   ('a, 'b) t -> 'result
   ('b, 'a) t -> 'result
   ...

This gives us a clue as to how we might attack the typing problem.
Unfolding the traversal methods one level gives us a pair of
mutually-recursive methods, neither of which is polymorphic-recursive,
and neither of which instantiates the class with different parameters:

   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)
       method t' :  ('b -> 'tb) -> ('a -> 'ta) -> ('b, 'a) t -> ('tb, 'ta) 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

In fact, instead of repeatedly creating new instances you can now use
a "self" binding, which will give you more scope for overriding
behaviour with subtyping:

   class ['a, 'b, 'ta, 'tb] m =
     object (self)
       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, self#t' fb fa bat)
           | B  a       -> B (fa a)
       method t' :  ('b -> 'tb) -> ('a -> 'ta) -> ('b, 'a) t -> ('tb, 'ta) t =
         fun fa fb s ->
           match s with
           | A (a, bat) ->
             A (fa a, self#t fb fa bat)
           | B  a       -> B (fa a)
     end

Of course, unfolding in this way doesn't work for general non-regular
types, since unfolding "nested" or "vec" would go on forever.

You might also consider unfolding the type "t" itself, at which point
traversals become more straightforward.  If you can expand the
definition of "t" to a pair of mutually recursive (and regular!)
types:

    type ('a, 'b) t =
       A of 'a * ('a, 'b) s
     | B of 'a
    and ('a, 'b) s =
       C of 'b * ('a, 'b) t
     | D of 'b

then you can use your current approach without any changes.

Hope this helps,

Jeremy.

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

[Alain Frisch]

On 12/02/2013 04:24 PM, Jeremy Yallop wrote:
> There's good news and bad news.  The good news is that the problem can
> be solved for your particular example.  The bad news is that the
> approach doesn't work in the general case.

A more general solution is based on recursive modules:

=======================================================================
type ('a, 'b) t =
     A of 'a * ('b, 'a) t
   | B of 'a

module rec X : sig
   class ['a, 'b, 'ta, 'tb] m : object
     method t : ('a -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t -> ('ta, 'tb) t
   end
end = struct
   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 X.m)#t fb fa bat)
           | B  a       -> B (fa a)
     end
end
=======================================================================


This technique also works e.g. for defining mutually recursive classes 
and nominal types.


Alain

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

[Jeremy Yallop]

On 3 December 2013 08:35, Alain Frisch <alain@frisch.fr> wrote:
> On 12/02/2013 04:24 PM, Jeremy Yallop wrote:
>> There's good news and bad news.  The good news is that the problem can
>> be solved for your particular example.  The bad news is that the
>> approach doesn't work in the general case.
>
> A more general solution is based on recursive modules:

Using recursive modules certainly makes it possible to write a class
with the correct type, but unless I'm mistaken you lose the ability to
override the behaviour on recursive calls -- i.e. the call to (new
X.m)#t can no longer be replaced with a call through a self variable.

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

[Alain Frisch]

On 12/03/2013 11:17 AM, Jeremy Yallop wrote:
> Using recursive modules certainly makes it possible to write a class
> with the correct type, but unless I'm mistaken you lose the ability to
> override the behaviour on recursive calls -- i.e. the call to (new
> X.m)#t can no longer be replaced with a call through a self variable.

The instance on which the method is called cannot be "self", since it 
corresponds to different type parameters for the class.  I don't know 
what Dmitri is exactly looking for, but maybe a polymorphic method 
(instead of a parametrized class) would do the job as well.

-- Alain

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

[Jeremy Yallop]

On 3 December 2013 12:33, Alain Frisch <alain@frisch.fr> wrote:
> On 12/03/2013 11:17 AM, Jeremy Yallop wrote:
>> Using recursive modules certainly makes it possible to write a class
>> with the correct type, but unless I'm mistaken you lose the ability to
>> override the behaviour on recursive calls -- i.e. the call to (new
>> X.m)#t can no longer be replaced with a call through a self variable.
>
> The instance on which the method is called cannot be "self", since it
> corresponds to different type parameters for the class.

That's true for the approach based on recursive modules, but not for
the unfolding approach outlined in my earlier message, which does
support recursive calls through self.

> I don't know what Dmitri is exactly looking for, but maybe a polymorphic method (instead of a parametrized class) would do the job as well.

Agreed.  For straightforward polymorphic recursion either your
recursive module approach or a simple recursive method or function is
sufficient.  Classes are better for open recursion, but only work
either for regular types or for types with finite irregularity (i.e.
where a finite number of unfoldings bring you back to the original
parameter list).

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

[Dmitri Boulytchev]

     Jeremy, Alain,

    the code snippet I presented was actually boiled down from the more 
complex example.
I don't have any particular interest to the concrete type t; I'm ok to 
give up
on "finitely regularizable" types but I definitely don't want to give up 
on GADTs
which might be essentially irregular.

 > As you've noted, you can work around the
 > problem using open recursion and typing the knot yourself, but you
 > lose the ability to subtype in the process.

   Well, having the solution with the polymorphic recursive function

     class ['a, 'b, 'ta, 'tb] proto_m f =
       object ... end

     let rec f : 'a 'b 'ta 'tb . unit -> ('a, 'b, 'ta, 'tb) #proto_m = 
fun () -> new proto_m f

     class ['a, 'b, 'ta, 'tb] m = ['a, 'b, 'ta, 'tb] proto_m f

   it is possible to inherit from proto_m:

     class ['a, 'b, 'ta, 'tb] m' f  =
       object
         inherit ['a, 'b, 'ta, 'tb] proto_m f as super
         method t fa fb s =
           match s with
           | A (a, bat) -> <some extra work>; super#t fa fb s
           | B  a       -> <some extra work>; super#t fa fb s
       end

     let rec g : 'a 'b 'ta 'tb . unit -> ('a, 'b, 'ta, 'tb) #proto_m = 
fun () -> new m' g

     class ['a, 'b, 'ta, 'tb] subm = ['a, 'b, 'ta, 'tb] m' g

   Here subm is a legitimate subclass of m with the desired behaviour 
(this property can not be
achieved with the recursive module though it is really much more elegant 
way to provide the proper
instantiation for class type parameters). So I don't see why I'm loosing 
the ability to subtype.
It seems to me that this workaround can be used to overcome the "regular 
class" restriction
completely in a syntax-conversion manner. I appreciate any comments.

   Dmitry.

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

[Jeremy Yallop]

On 3 December 2013 17:49, Dmitri Boulytchev <dboulytchev@gmail.com> wrote:
>   Here subm is a legitimate subclass of m with the desired behaviour [...]. So I don't see why I'm loosing the ability to subtype.

You're quite right, of course: you still have subtyping.  What you're
giving up are some of the benefits of inheritance, since the
"recursive" calls go through the instance you pass in rather than
through a self variable.  If you don't have other reasons for using
objects and classes it might be worth considering using records
instead, since they're semantically much simpler.  The example should
translate directly:

  type ('a, 'b, 'ta, 'tb) m' =  {
    t : ('a -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t -> ('ta, 'tb) t
  }

  let proto_m f = {
    t = fun fa fb s ->
    ...

  let m' f =
    let super = proto_m f in {
      super with t = fun fa fb s ->
    ...

> It seems to me that this workaround can be used to overcome the "regular class" restriction completely in a syntax-conversion manner. I appreciate any comments.

Yes, it's a neat approach!  One small suggestion: in order to handle
the case where the type you're traversing has multiple recursive
instantations with different parameters you might consider passing the
instance creation function in a way that allows it to be called
polymorphically (e.g. by wrapping it in a record with a polymorphic
field):

  type new_proto_m = {
     new_proto_m : 'a 'b 'ta 'tb .
         unit -> <t : ('a -> 'ta) -> ('b -> 'tb) ->
                      ('a, 'b) t -> ('ta, 'tb) t>
  }

There is one last thing I'm curious about.  The difficulties that
you're avoiding with open recursion seem to arise from the
representation of the traversal as a parameterised class with a
monomorphic method.  Have you considered switching things round and
using an unparameterised class with polymorphic methods instead?  I
think everything turns out much simpler if you do: you can use
straightforward inheritance, calls through self, etc.

  class m =
  object (self)
    method t : 'a 'b 'ta 'tb. ('a -> 'ta) -> ('b -> 'tb) ->
                              ('a, 'b) t -> ('ta, 'tb) t =
      fun fa fb s ->
        match s with
        | A (a, bat) -> A (fa a, self#t fb fa bat)
        | B  a       -> B (fa a)
  end

The map and fold generators supplied with Camlp4 use a variant of this
approach, and it seems to work well in practice.

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

[Dmitri Boulytchev]

> Yes, it's a neat approach!  One small suggestion: in order to handle
> the case where the type you're traversing has multiple recursive
> instantations with different parameters you might consider passing the
> instance creation function in a way that allows it to be called
> polymorphically (e.g. by wrapping it in a record with a polymorphic
> field):
     Of course; this is yet another workaround to make it possible to use
that workaround :)

> There is one last thing I'm curious about.  The difficulties that
> you're avoiding with open recursion seem to arise from the
> representation of the traversal as a parameterised class with a
> monomorphic method.
     The reason is quite simple --- class parameters are used to represent
the *result* type of the transformation, not the parameters of the 
transforming
type. I simplified the example just to clarify the polymorphic class issues.
     In reality what I'm interested in is somewhat like this: for a type

     ('a, 'b, ...) t = A ... | B ... | C ...

     we generate a virtual class

     class virtual ['ta, 'tb, ..., 'inh, 'syn] t_t = object
         method virtual c_A : <explicitly polymorphic type on 'a, 'b etc.>
         method virtual c_B : <explicitly polymorphic type on 'a, 'b etc.>
         etc.
     end

     which represents some attribute transformation with inherited 
attribute type 'inh; the
type of synthesized attribute for type 'a is 'ta, for 'b is 'tb etc., 
for type ('a, 'b, ...) t
is 'syn. The methods of the class handle the individual constructors; 
the arguments for
these methods capture the transformation function as well.
     For example, for regular map we have the following bindings:

     class ['ta, 'tb, ...] map_t = object
         inherit ['ta, 'tb, ..., unit, ('ta, 'tb, ...) t] t_t
         ...
     end

     for show we have

     class show_t = object
         inherit [string, string, ..., unit, string] t_t
         ...
     end

     for, say, eval

     class eval_t = object
         inherit [int, int, ..., string -> int, int] t_t
         ...
     end

     etc.

     Under this representation we might need the single 
shallow-traversal generic function
to implement all these transformations.
     Per-constructor object encoding allows modification with less 
boilerplate code (via
inhertance); in addition if we have a polymorphic-variant type t = [ a | 
b | c ... ] then
the certain transformation for t can be constructed by regular class 
inheritance from the
implementations of the same transformation for it's counterparts.


     Best regards,
     Dmitry.

     P.S. I was'nt offended by your long message (but surprised a little 
bit ).