Fwd: "ocaml_beginners"::[] Trouble combining polymorphic classes and polymorphic methods

Fwd: "ocaml_beginners"::[] Trouble combining polymorphic classes and polymorphic methods

[Geoffrey Romer]

[escalated from ocaml_beginners, where I got no response]

I'm trying to create a polymorphic class 'a foo which has a
polymorphic method that takes as a parameter another foo object, but
one with arbitrary type. In other words, something like this:

class virtual ['a] foo =
object (self)
  method virtual bar : 'b. 'b foo -> unit
end;;

When I try to compile this, though, I get a warning that I "cannot
quantify 'b because it escapes this scope". When I drop the " 'b. " it
compiles fine, but the reported type for bar is 'a foo -> unit; i.e.
it's no longer polymorphic.

Is there a problem with trying to make a method polymorphic with
respect to the class type in this way? How can I make this work?

Re: [Caml-list] Fwd: "ocaml_beginners"::[] Trouble combining polymorphic classes and polymorphic methods

[Jacques Garrigue]

From: "Geoffrey Romer" <geoff.romer@gmail.com>
> [escalated from ocaml_beginners, where I got no response]
> 
> I'm trying to create a polymorphic class 'a foo which has a
> polymorphic method that takes as a parameter another foo object, but
> one with arbitrary type. In other words, something like this:
> 
> class virtual ['a] foo =
> object (self)
>   method virtual bar : 'b. 'b foo -> unit
> end;;
> 
> When I try to compile this, though, I get a warning that I "cannot
> quantify 'b because it escapes this scope". When I drop the " 'b. " it
> compiles fine, but the reported type for bar is 'a foo -> unit; i.e.
> it's no longer polymorphic.
> 
> Is there a problem with trying to make a method polymorphic with
> respect to the class type in this way? How can I make this work?

The reason it does not work is that recursive object types have to be
regular. That is, when using foo inside its own definition, the
parameters must be the same. Since 'a <> 'b, this fails.

This restriction is due to the structural typing of objects, and as
such it does not apply to records, which are nominal. So you can
write:
  type 'a foo = { bar : 'b. 'b foo -> unit; }
which has basically the same meaning.

You can also mix classes and records:
  type 'a foo_t = <get : 'a; bar : 'b. 'b foo_r -> unit>
  and 'b foo_r = {foo: 'b foo_t}
This way, you only need to wrap foo objects in foo_r when you want to
pass them to bar.

If you want to define a class type rather than an object type (class
types are more versatile), you can use the following trick to create a
recursion between a class type and a normal type;

  module rec M : sig            
    class type ['a] foo = object
      method get : 'a
      method bar : 'b. 'b M.foo_r -> unit
    end
    type 'a foo_r = {foo: 'a foo}
  end = M

You cannot define your virtual class directly inside the recursive
module, because it would require an implementation, but this can be
done easily afterwards:
  # class virtual ['a] foo = object (_ : 'a #M.foo) end;;
  class virtual ['a] foo :
    object method virtual bar : 'b M.foo_r -> unit method virtual get : 'a end

Hope this helps.

Jacques Garrigue

Re: [Caml-list] Fwd: "ocaml_beginners"::[] Trouble combining polymorphic classes and polymorphic methods

[Lukasz Stafiniak]

On 2/28/07, Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> wrote:
> From: "Geoffrey Romer" <geoff.romer@gmail.com>
> >
> > I'm trying to create a polymorphic class 'a foo which has a
> > polymorphic method that takes as a parameter another foo object, but
> > one with arbitrary type. In other words, something like this:
> >
> > class virtual ['a] foo =
> > object (self)
> >   method virtual bar : 'b. 'b foo -> unit
> > end;;
> >
> > When I try to compile this, though, I get a warning that I "cannot
> > quantify 'b because it escapes this scope". When I drop the " 'b. " it
> > compiles fine, but the reported type for bar is 'a foo -> unit; i.e.
> > it's no longer polymorphic.
> >
> > Is there a problem with trying to make a method polymorphic with
> > respect to the class type in this way? How can I make this work?
>
> The reason it does not work is that recursive object types have to be
> regular. That is, when using foo inside its own definition, the
> parameters must be the same. Since 'a <> 'b, this fails.
>
> This restriction is due to the structural typing of objects, and as
> such it does not apply to records, which are nominal. So you can
> write:
>   type 'a foo = { bar : 'b. 'b foo -> unit; }
> which has basically the same meaning.
>
Thank you for the answer. Let's play the dual of this game:

# type 'a sty = [`Foo of (int * 'a) sty | `Bar];;
Characters 4-45:
  type 'a sty = [`Foo of (int * 'a) sty | `Bar];;
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
In the definition of sty, type (int * 'a) sty should be 'a sty
# type 'a nty = Foo of (int * 'a) nty | Bar;;
type 'a nty = Foo of (int * 'a) nty | Bar

(I wonder if this is the reason when people rant that structural types
are a weaker form of type control... ;) Recently I've started using
closed polymorphic variant types to build subtyping hierarchies and
this gives more type control to me, I think.)

Re: [Caml-list] Fwd: "ocaml_beginners"::[] Trouble combining polymorphic classes and polymorphic methods

[Jacques Garrigue]

From: "Lukasz Stafiniak" <lukstafi@gmail.com>
> Thank you for the answer. Let's play the dual of this game:
> 
> # type 'a sty = [`Foo of (int * 'a) sty | `Bar];;
> Characters 4-45:
>   type 'a sty = [`Foo of (int * 'a) sty | `Bar];;
>       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
> In the definition of sty, type (int * 'a) sty should be 'a sty
> # type 'a nty = Foo of (int * 'a) nty | Bar;;
> type 'a nty = Foo of (int * 'a) nty | Bar

Indeed, this is to be expected. Again, if one needs both polymorphic
variants and irregular types, it is possible to combine both, but not
very natural.

> (I wonder if this is the reason when people rant that structural types
> are a weaker form of type control... ;) Recently I've started using
> closed polymorphic variant types to build subtyping hierarchies and
> this gives more type control to me, I think.)

For your first point, I don't think so. Irregular types are quite rare
in practice, though they arise rather naturally when combining objects
and polymorphism. What some people do not like about structural types
is that they do not "brand" types: you can define the same type
elsewhere, possibly with a different intended meaning, and the
compiler will not distinguish between the two. This type equality also
means that you cannot rely on type identity for privacy features: this
is the reason why ocaml private methods are not like Java.
But on the other hand, in many cases you precisely want this equality.

Jacques Garrigue

Re: [Caml-list] Fwd: "ocaml_beginners"::[] Trouble combining polymorphic classes and polymorphic methods

[skaller]

On Wed, 2007-02-28 at 10:34 +0900, Jacques Garrigue wrote:

> and polymorphism. What some people do not like about structural types
> is that they do not "brand" types: you can define the same type
> elsewhere, possibly with a different intended meaning, and the
> compiler will not distinguish between the two. 

Of course you CAN brand types if you want to!

type 'a metres = Metres of 'a 
type 'a feet = Feet of 'a 

type int_metres = int metres
type int_feet = int feet

or perhaps 

type metres = { metre: int }
type feets  = { feet: int }

or some other trick with phantom types I'm sure someone will
point out.

After all a nominal type is just a structural type with
a unique tag representing its unique name.

Look at in the converse: a structural type is just the
canonical representative of nominal types with the
same structure.

Or perhaps i'm confused .. :)

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] Fwd: "ocaml_beginners"::[] Trouble combining polymorphic classes and polymorphic methods

[Daniel Bünzli]

Le 28 févr. 07 à 02:57, skaller a écrit :

> After all a nominal type is just a structural type with
> a unique tag representing its unique name.

What you miss here is the _process_ behind nominal types.

(paraphrasing Jacques) Types are not precise enough to define the  
semantic of a function, multiplication and addition have the same  
type but in many cases you cannot exchange one for the other. With  
that respect structural typing is a fallacy, it is not because types  
match that you can replace a function by another.

With a nominal type the programmer signals explicitely its intent to  
support a semantic. Notably you cannot use a function in a given  
context if it was not designed for that purpose which sounds  
fascistic but makes sense from a software development point of view.

Structural typing would make sense if it involved the weakest  
invariants a function. But for now, because of the poor information  
types give about semantics, structural typing is just bureaucratic  
compliance whereas nominal typing is a semantic contract --- whether  
actually fulfilled or not is another (undecidable) question.

Daniel

Re: [Caml-list] Fwd: "ocaml_beginners"::[] Trouble combining polymorphic classes and polymorphic methods

[Jacques Garrigue]

From: Daniel Bünzli <daniel.buenzli@epfl.ch>
> Le 28 févr. 07 à 02:57, skaller a écrit :
> 
> > After all a nominal type is just a structural type with
> > a unique tag representing its unique name.
> 
> What you miss here is the _process_ behind nominal types.
> 
> (paraphrasing Jacques) Types are not precise enough to define the  
> semantic of a function, multiplication and addition have the same  
> type but in many cases you cannot exchange one for the other. With  
> that respect structural typing is a fallacy, it is not because types  
> match that you can replace a function by another.
> 
> With a nominal type the programmer signals explicitely its intent to  
> support a semantic. Notably you cannot use a function in a given  
> context if it was not designed for that purpose which sounds  
> fascistic but makes sense from a software development point of view.
> 
> Structural typing would make sense if it involved the weakest  
> invariants a function. But for now, because of the poor information  
> types give about semantics, structural typing is just bureaucratic  
> compliance whereas nominal typing is a semantic contract --- whether  
> actually fulfilled or not is another (undecidable) question.

Wow, here is a strong statement. Basically, you seem to be saying that
types are useless for safety if they don't ensure full correctness,
and that in the absence of safety they need to be nominal in order to
declare any intent?

I personally would contradict you on both counts.

The first point is that type safety is already an important form of
safety. Even if it is purely bureaucratic, at least it ensures that
there is no contradiction _at the level of types_. If you are an ML
programmer, you must know that this is useful.

The second point is on the extra semantic advantage of using nominal
types. I think there is some mixing up here. You can perfectly put a
name on a value without using a nominal type. Using good function
names, labelled arguments, etc... And writing (`Metre 3) gives you
exactly the same information as (Metre 3). By naming things, even
structurally, you can express informal contracts.

The theoretical problem with structural types is more about very bad
luck: you may be using two libraries, which seem to be using the same
type (same constructor or method names), but actually have different
semantics.  And you might end up mixing data from the two libraries by
error. The probability of this happening is so incredibly low that I
often wonder why people see this as a real problem, but this reflects
the lack of proper identity in structural types. This lack of identity
may become a problem when you want to use identity for other things,
like privacy. But it is not really relevant for normal public types,
since you may easily deconstruct and reconstruct them. On the other
hand, if you (rightly) decide to use abstract types in an API, whether
they are internally nominal or structural is not relevant.

If I may add a 3rd point, I believe that structural types sometimes
allow you to give more precise specifications of functions, that would
be hard to obtain with nominal types. See the use of polymorphic
variants in lablGL for instance. This is certainly not a complete
specification, all the less as the API is imperative. But this
information can work as documentation, and removes an important
category of runtime errors.

Jacques Garrigue

Re: [Caml-list] Fwd: "ocaml_beginners"::[] Trouble combining polymorphic classes and polymorphic methods

[skaller]

On Wed, 2007-02-28 at 13:01 +0900, Jacques Garrigue wrote:
> From: Daniel Bünzli <daniel.buenzli@epfl.ch>
[]
> The theoretical problem with structural types is more about very bad
> luck: you may be using two libraries, which seem to be using the same
> type (same constructor or method names), but actually have different
> semantics.

This is possible with nominal typing too, it just requires
even 'badder' luck .. we probably all know the famous OO
example of a 'drawable' abstraction with instance 'gun' :)


-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] Fwd: "ocaml_beginners"::[] Trouble combining polymorphic classes and polymorphic methods

[Daniel Bünzli]

Le 28 févr. 07 à 05:01, Jacques Garrigue a écrit :

> Wow, here is a strong statement. Basically, you seem to be saying that
> types are useless for safety if they don't ensure full correctness,
> and that in the absence of safety they need to be nominal in order to
> declare any intent?

I think you took the statement stronger that I intended (my fault).  
I'm certainly not saying types are useless for safety without  
correctness. I find it _immensely_ usefull that a machine takes care  
of the bureaucracy of types and I often wonder, when the compiler  
reminds me, how bad my software development would be in a dynamically  
typed language -- not even talking about those in which you don't  
declare your identifiers.

My statement was really about the module system part of the type  
system. I sometimes find it a little bit artificial that if your  
module structuraly matches a signature you can pass it to a functor.  
If you take the point of view of a programmer who is provided with  
modules he didn't write, I think it makes it easier for him to make  
correct functor applications in a nominal setting because modules  
explictely indicate that they were designed to support a given  
interface. On the other hand, nominality hinders code reuse since you  
may found a use that the initial programmer couldn't ever foresee.  
But this problem can be alleviated by a simple construct that allows  
to extend a module to support a new interface (even if no new code  
needs to be written).

Besides that, I agree with most of your points, even though your  
`Apples may be oranges to me but I quite buy your probabilistic  
argument.

Best,

Daniel