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

[Jeremy Yallop <yallop@gmail.com>]

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.