[Caml-list] recursive module, object types, tying knot

[Caml-list] recursive module, object types, tying knot

[Dmitry Grebeniuk]

Hello.

  I have an usual question.  I want to make some object
types (container-like) that can map the stored contents
with its method.  For example, let the container will be
the simple list:
class ['a] (lst : list 'a) = object ...
  method map : ('a -> 'b) -> 'b lst

  The compiler yields an error:
# class ['a] lst x = object
   method map : 'b . ('a -> 'b) -> 'b lst
   = fun f -> List.map f x end;;
Error: This type scheme cannot quantify 'b :
it escapes this scope.

  I know the solution with separate function for map,
but I don't like it: the whole mess with objects is
to use less information to make api call: compare
"MapIntToString.get my_map 123" with
"my_map#get 123".  Having to remember where
(in which module) the correct map function resides
will ruin the purpose of the code I'm writing now.

  (maybe "implicit values" could help here, but they are
not the part of official compiler for now.)

  I need to write the code that performs that map, maybe
with help of some additional types and values.  And I
began experimenting.


  Now I have two pieces of code (for even simpler
container, that contains just one value), the second one
is derived from the first one by replacing the type "ta"
from the record to the object type.  The first piece
of code works, but the second does not.  Why there is
such a difference, and, more importantly, how should
I tweak the second piece of code to make it work?
(if you remember, referencing the record's fields will
require the path to the module where the record
is declared (see the "q#tbm.L.tam" subexpression),
so the first "solution" is not a solution for my current
problem.)

$ ocaml
        Objective Caml version 3.12.1+rc1

# module rec L
 :
  sig
    type 'a ta = { tam : 'b. ('a -> 'b) -> 'b L.tb }
    class ['a] tb : 'a -> object method tbm : 'a L.ta end
    val make_ta : 'a -> 'a L.ta
  end
 =
  struct
    type 'a ta = { tam : 'b. ('a -> 'b) -> 'b L.tb }
    let make_ta : 'a -> 'a L.ta = fun a -> { tam = fun f -> new L.tb (f a)}
    class ['a] tb x = object method tbm : 'a L.ta = L.make_ta x end
  end;;
module rec L :
  sig
    type 'a ta = { tam : 'b. ('a -> 'b) -> 'b L.tb; }
    class ['a] tb : 'a -> object method tbm : 'a L.ta end
    val make_ta : 'a -> 'a L.ta
  end

# let q = new L.tb 123;;
val q : int L.tb = <obj>

# let w = q#tbm.L.tam string_of_int;;
val w : string L.tb = <obj>

#

  (it really works -- the map is applied, the
object is created.  I've checked it with more
extended types that allowed me to examine
the contents of such a great container.)

$ ocaml
        Objective Caml version 3.12.1+rc1

# module rec L
   :
    sig
      type 'a ta = < tam : 'b. ('a -> 'b) -> 'b L.tb >
      class ['a] tb : 'a -> object method tbm : 'a L.ta end
      val make_ta : 'a -> 'a L.ta
    end
   =
    struct
      type 'a ta = < tam : 'b. ('a -> 'b) -> 'b L.tb >
      let make_ta : 'a -> 'a L.ta = fun a ->
        object method tam : 'b. ('a -> 'b) -> 'b L.tb =
          fun f -> new L.tb (f a)
        end
      class ['a] tb x = object method tbm : 'a L.ta = L.make_ta x end
    end;;
Error: In the definition of L.tb, type 'a L.ta should be 'b L.ta
#

  Maybe there is a problem with type "ta" in the second piece,
because record is "concrete" type, but the object type is just
a list of their methods.  But I can't check it successfully: trying
to wrap occurences of "tb" with "type 'a id = Id of 'a" (and removing
"ta" at all) does not help, just yields different types in error
"In the definition of .., type .. should be ..".

  Please help me.  Any ideas are highly appreciated.

Re: [Caml-list] recursive module, object types, tying knot

[Jacques Garrigue]

On 2011/09/08, at 6:29, Dmitry Grebeniuk wrote:

> Hello.
> 
>  I have an usual question.  I want to make some object
> types (container-like) that can map the stored contents
> with its method.  For example, let the container will be
> the simple list:
> class ['a] (lst : list 'a) = object ...
>  method map : ('a -> 'b) -> 'b lst
> 
>  The compiler yields an error:
> # class ['a] lst x = object
>   method map : 'b . ('a -> 'b) -> 'b lst
>   = fun f -> List.map f x end;;
> Error: This type scheme cannot quantify 'b :
> it escapes this scope.

The answer is unfortunately short: there is no solution.
Namely recursive types in ocaml must be regular.
I.e., they must expand to a finite graph.
In particular this means that, inside the class lst, all occurences
of lst must have exactly the parameter 'a.
As you have already found, you can avoid this problem by
defining a record which "hides" the use of lst.
Namely, you must break the cycle with a datatype,
either record or sum type.
Unfortunately this also means that this type has to belong
to some module, and you also lose subtyping.

Jacques Garrigue

Re: [Caml-list] recursive module, object types, tying knot

[Dmitry Grebeniuk]

Hello.

>> Error: This type scheme cannot quantify 'b :
>> it escapes this scope.

> The answer is unfortunately short: there is no solution.

  Thank you for the definitive and quick answer!

> Namely recursive types in ocaml must be regular.
> I.e., they must expand to a finite graph.
> In particular this means that, inside the class lst, all occurences
> of lst must have exactly the parameter 'a.

  Just interesting: where this graph and its finiteness property
are used?

> As you have already found, you can avoid this problem by
> defining a record which "hides" the use of lst.
> Namely, you must break the cycle with a datatype,
> either record or sum type.
> Unfortunately this also means that this type has to belong
> to some module, and you also lose subtyping.

  I've tried to make the type (lst 'b) belong to some first-class
module returned by some method call (to object with type
lst 'a), but without any success.
  And while playing with first-class modules I've noted that
I can't constrain the parametric type of module:
let module M = (lst#mapmodule : Mappable with type t 'a = list a)
 -- one more way is blocked (but don't know was it the way
really).


  But I can reformulate (and maybe make easier) my task:
I can move the code that work with different type parameters
(lst 'a -> lst 'b) to simple functions.  For example, "map" for
containers -- to the function like "container_map", which
will work with containers (objects that have some methods),
to make the code work:
container_map func (new lst [1;2;3]);
container_map func (new arr [|1;2;3|]).
  I understand that the imaginable "container_map" function
should require some method with some type, that can
give me the value of type lst 'b for lst 'a in case of lists,
and the value of type arr 'b for arr 'a in case of arrays,
but I can't write such type (even with first-class modules).
  Is it impossible too?

Re: [Caml-list] recursive module, object types, tying knot

[Jacques Garrigue]

On 2011/09/09, at 20:14, Dmitry Grebeniuk wrote:

>> Namely recursive types in ocaml must be regular.
>> I.e., they must expand to a finite graph.
>> In particular this means that, inside the class lst, all occurences
>> of lst must have exactly the parameter 'a.
> 
>  Just interesting: where this graph and its finiteness property
> are used?

Well, there are many algorithms that must do exhaustive traversal
of types to verify some property, and it implies that the type must
be finite.
Also, while unification on regular types is easy, I don't know of
any algorithms for non-regular types.

>> As you have already found, you can avoid this problem by
>> defining a record which "hides" the use of lst.
>> Namely, you must break the cycle with a datatype,
>> either record or sum type.
>> Unfortunately this also means that this type has to belong
>> to some module, and you also lose subtyping.
> 
>  I've tried to make the type (lst 'b) belong to some first-class
> module returned by some method call (to object with type
> lst 'a), but without any success.
>  And while playing with first-class modules I've noted that
> I can't constrain the parametric type of module:
> let module M = (lst#mapmodule : Mappable with type t 'a = list a)
> -- one more way is blocked (but don't know was it the way
> really).

This is indeed a restriction of locally abstract types that one
cannot use them as row variables. This might be done if there
are applications.

>  But I can reformulate (and maybe make easier) my task:
> I can move the code that work with different type parameters
> (lst 'a -> lst 'b) to simple functions.  For example, "map" for
> containers -- to the function like "container_map", which
> will work with containers (objects that have some methods),
> to make the code work:
> container_map func (new lst [1;2;3]);
> container_map func (new arr [|1;2;3|]).
>  I understand that the imaginable "container_map" function
> should require some method with some type, that can
> give me the value of type lst 'b for lst 'a in case of lists,
> and the value of type arr 'b for arr 'a in case of arrays,
> but I can't write such type (even with first-class modules).
>  Is it impossible too?

The main problem is that you cannot define a constructor
method which return an object with a different parameter.
On the other hand, fold can be defined as a polymorphic
method, allowing you to define functions building various kinds
of containers, starting from an arbitrary one.

Jacques Garrigue

Re: [Caml-list] recursive module, object types, tying knot

[Dmitry Grebeniuk]

Hello.

>> I can't constrain the parametric type of module:
>> let module M = (lst#mapmodule : Mappable with type t 'a = list a)
>> -- one more way is blocked (but don't know was it the way
>> really).
>
> This is indeed a restriction of locally abstract types that one
> cannot use them as row variables. This might be done if there
> are applications.

  I don't know whether it can help.  In general, there seems to be
no way to write a type of function that is polymorphic on some
parametric type:
"forall _ t, forall 'a, 'b, map: ('a -> 'b) -> 'a t -> 'b t".
  Maybe something like this could work:
module type MAP = sig
  type 'a t
  val map : ('a -> 'b) -> 'a t -> 'b t
end
let gen_map1 =
  fun (type 'a tt) ->
  fun mapmodule ->
  let module M = (val mapmodule : MAP with type 'a t = 'a tt) in
  fun f -> fun (x : 'a tt) -> M.map f x
(* or *)
let gen_map2 mapmodule =
  let module M = (val mapmodule : MAP) in
  fun f (x : 'a M.t) -> M.map f x

  But the changes in typechecker should be too massive
to make it work.  So, it's better to forget my perfectionistic
attempts.

  Anyway, I've learned many things about OCaml type
system, so this was not completely useless work for me.

  And if some code should use "any mappable data
structure", there is no other way than wrapping this code
into functor.

> On the other hand, fold can be defined as a polymorphic
> method, allowing you to define functions building various kinds
> of containers, starting from an arbitrary one.

  I've tried to write some code where the initial container is
stored in the object itself, but couldn't make it work.  And
this approach (map = fold_right + cons) is somewhat limited,
it will work good for single-linked lists, but I can't imagine
it can work with more complex data structures like trees
(and I can imagine the overhead of folding + consing
over arrays).  So I prefer to avoid such style of mapping.

Re: [Caml-list] recursive module, object types, tying knot

[Gabriel Scherer]

On Tue, Sep 13, 2011 at 6:56 AM, Dmitry Grebeniuk <gdsfh1@gmail.com> wrote:
>  I've tried to write some code where the initial container is
> stored in the object itself, but couldn't make it work.  And
> this approach (map = fold_right + cons) is somewhat limited,
> it will work good for single-linked lists, but I can't imagine
> it can work with more complex data structures like trees

You may define more general folds. The idea is that from any algebraic
datatype you can derive a fold operator.

See for example:

  type 'a list = Nil | Cons of 'a * 'a list
  val list_fold : 'r -> ('a -> 'r -> 'r) -> 'r

  type 'a tree = Nil | Leaf of 'a list * 'a * 'a list
  val tree_fold : 'r -> ('r -> 'a -> 'r) -> 'r

  type ('a, 'b, 'c) strange_list =
    | End of 'c
    | ACons of 'a * ('a, 'b, 'c) strange_list
    | BCons of 'b * ('a, 'b, 'c) strange_list
  val strange_list_fold : ('c -> 'r) -> ('a -> 'r -> 'r) -> ('b -> r -> r) -> r

The idea is that for each constructor of the datatype, you add an
argument to the fold, that has the same signature as its type as a
function (Nil : 'a list) (Cons :  'a -> 'a list -> 'a list), with
recursive occurences of the type replaced by the elimination type
parameter 'r.

There is a more abstract construction : if you express recursive
datatypes as fixpoint of a type with one more parameter (~ polynomial
functor), you can define fold recursively from a `map` operation on
this type. For example, ('a list) is the fixpoint on 'b of (type ('a,
'b) cons = Nil' | Cons' of 'a * 'b), which is witnessed by the
existence of reciprocal (val wrap : ('a, 'a list) cons -> 'a list) and
(val unwrap : 'a list -> ('a, 'a list cons)), and (some form of)
list_fold can be defined as
  let rec list_fold li = f (map_cons (list_fold f) (unwrap li))

For a more abstract and hardly readable presentation of this topic,
see the article "Functional programming with Bananas, Lenses,
Envelopes and Barbed Wire" by Meijer, Fokkinga and Paterson, 1991.

> (and I can imagine the overhead of folding + consing
> over arrays).  So I prefer to avoid such style of mapping.

An `iter` function is sufficient for arrays:

class type ['a] array = object
  ...
  method length : int
  method iter : (int -> 'a -> unit) -> unit
end

You can then express the map operation:
  let map f t =
    let result = make_array t#length in
    t#iter (fun i x -> result#set i (f x));
    result

An internal map would have to allocate a new array anyway (in the
general case where (f : 'a -> 'b), you can't mutate the array
in-place), so this is as efficient memory-wise. Similarly, a map
defined by the user from a fold on a recursive datatype has the same
allocation profile as an internally-defined fold. The only potential
overhead comes from the passing of the fold function (which means one
more indirect call per node traversed), but if you're at this level of
detail you may not want to design your core data structures as object
anyway.