Thoughts on O'Labl O'Caml merge.

Thoughts on O'Labl O'Caml merge.

[John Prevost]

I was recently thinking about row polymorphism, structs and sum types.
It occurred to me that one could do row polymorphism with sum types as
well as with structs.  My model was something like this (thought it
requires a strange kinding system) (Well, it was too long, so I moved
it to the bottom.)


In any case, the point I have is that I came to the realization that
SML (while not allowing row polymorphism) has different (and smaller)
restrictions on the labels of struct types:

fun x { a : int, b : float } = a + round b

fun y { a : float, b : int } = a + float b

You can use the same labels in more than one way.

O'Caml, having taken a different road, requires that struct types be
defined ahead of time, and labels cannot overlap--just like the
current sum types in both languages.  I thought "Hmm, it might be
interesting to set up a language where this property is true of both
sum types and struct types, and then add row polymorphism to it."

Then I saw the messages about merging O'Labl and O'Caml, and started
looking at O'Labl again, and saw the row polymorphism on polymorphic
variants.

And that made me think: "So now O'Caml will have a system which allows
reusable sum labels, and non-reusable struct labels.  And SML will
have a system which has reusable struct labels but not reusable sum
labels."



Important questions:

So--the heart of my question: would it be possible to, while adding
row polymorphism on sum types (or a variation on that theme) also add
it on struct types (or a variation of that theme) outside of objects?


The only other thing I can think of which has been a thorn in my side
is the overreach of the value restriction on functional values--which
hurts a lot when you're doing stuff with purely functional or
otherwise safe combinators.  I don't know if this is open for
discussion, as it's been hashed over on the mailing list in the past,
but I suppose if things are being changed around, there might be a
possibility.





Here's the type system I was working on:

<type> ::= int
         | bool
         | { <label> : <type> }
         | [ <label> : <type> ]
         | <type> + type
         | <type> | <type> 
         | ... other base types, type constructors, etc.

(where that last pipe is a pipe symbol, not another option.  Silly
notation on my part.  :)

Actually, the + and | type operators need to have {} and [] types,
respectively, so:

|- bool : base

|- int  : base

|- { <label> : <type> } : struct

|- [ <label> : <type> ] : sum

|- <type1> : struct    |- <type2> : struct
------------------------------------------
      |- <type1> + <type2> : struct

|- <type1> : sum    |- <type2> : sum
------------------------------------
     |- <type1> | <type2> : sum

Which is a rather overcomplicated kinding system, but oh, well.  I was
just playing.  So, with this system and polymorphism, you could have:

{ a : int } + { b : float } + 'a

represents "any value that has at least fields a : int and b : float", and

[ a : int ] + [ b : float ] + 'a

represents "any value which has at least sum possibilities a : int and
b : float"

Other people have worked this out in better and greater detail than I
have, including the "at least" vs "no more than" issue for sum types.

Re: Thoughts on O'Labl O'Caml merge.

[skaller]

John Prevost wrote:
> Actually, the + and | type operators need to have {} and [] types,
> respectively, so:
> 
> |- bool : base
> |- int  : base
> |- { <label> : <type> } : struct
> 
> |- [ <label> : <type> ] : sum
> 
> |- <type1> : struct    |- <type2> : struct
> ------------------------------------------
>       |- <type1> + <type2> : struct
> 
> |- <type1> : sum    |- <type2> : sum
> ------------------------------------
>      |- <type1> | <type2> : sum
> 
> Other people have worked this out in better and greater detail than I
> have, including the "at least" vs "no more than" issue for sum types.

Excuse me if I think aloud?

When a function requires a struct with certain labels,
we can use a product with 'enough' labels of the right type 
PROVIDED the fields are immuable.

HOWEVER, these rules break down in the presence
of mutable fields. The rule then is the dual,
and combined, we obtain a requirement for
invariance. Consider a representation of complex
numbers using labels

	real, imag, mod, arg

in which the cartesian/polar coordinates
are both given and synched. Functions requiring
either cartesian or polar coordinates will
accept these values, and return either
cartesian, polar, or the dual representation.

But, if the functions _modify_ the record,
the argument must be exactly the right type:
either exactly polar, cartesian, or the dual
representation, will be required. No matter
which is required, no other type is acceptable.

This observation is the key theorem which
utterly destroys object orientation as
a paradigm: because objects are useless
unless mutable, and subtyping only
works with immutable values, Oo is devoid
of polymorphism.

To give the classic example: as values,
a square is a rectangle. Once mutation
is permitted, functions requiring
rectangles or squares require precisely
rectangle or square arguments, and the
other type will never do.

The rectangle method 'set_sides(a,b) cannot
be applied to a square, [overspecification]
and the square method 'set_diagonal(d)' cannot
be applied to a rectangle [underspecification].

[Technically, writing is dual to reading,
however most 'mutators' are to be considered
as requiring both reading and writing, so
that both co- and contra- variance conditions
collapse into invariance conditions]

------------------
What does this mean for the type system?

There is a key theorem, developed for C++
pointer chains, which proves which conversions
are const correct. Here is the theorem
(excuse the C++ terminology):

Let X1 be T1 cv1,1 * ... cv1,N * where T1 is not a pointer type, and
let X2 be T1 cv2,1 * ... cv2,N * and where cvi,j is either 'const' 
or omitted, then a conversion from X1 to X2 is const correct iff

 	1) for all j, if cv1,j is 'const', then so is cv2,j
	2) if there exists j, cv1,j <> cv2,k then
		for all k < j, cv2,j is 'const'

To paraphrase 'it is not enough, to just throw const
into the signature, if you throw one in, it must
propagate to the top'. It is a somewhat surprising
result, that adding in an extra const can destroy
an otherwise safe conversion. Here is an example:

	T *** -> T const ** const*

This conversion isn't safe. The reason is that
the second pointer in the chain is mutable,
and it points to a type which looks like
T const **, so we can assign to it a T const *.
However, the actual pointer is of type T***
which would allow writing into the 'const' field
of the record we just assigned.

The rule can be considered as requiring
top level invariance, down to a certain
location in the chain, where a normal
'subtyping' conversion is allowed
(viewing a mutable value as a subtype of an immutable
one).

This rule must be applied in ocaml if open types
are provided for records with mutable fields,
since in this case, I imagine, the 'type'
of a field in a signature can _also_ be a signature.
Please read:

	C++: X const * as ocaml: { pointer: X }
	C++: X *       as ocaml: { mutable pointer: X }

where X can itself be a signature [or record type].
[I have modified the C++ theorem to elide reference
to 'volatile']

What I _think_ this all means for ocaml, is that
the rule for matching records with signatures
must be extended to handle mutable fields,
as described per field by the above theorem,
on a field by field basis.

-- 
John Skaller, mailto:skaller@maxtal.com.au
1/10 Toxteth Rd Glebe NSW 2037 Australia
homepage: http://www.maxtal.com.au/~skaller
downloads: http://www.triode.net.au/~skaller

Re: Thoughts on O'Labl O'Caml merge.

[John Prevost]

skaller <skaller@maxtal.com.au> writes:

> When a function requires a struct with certain labels,
> we can use a product with 'enough' labels of the right type 
> PROVIDED the fields are immuable.
> 
> HOWEVER, these rules break down in the presence
> of mutable fields. The rule then is the dual,
  ... covariant, contravariant, invariant ...

Ahh.  Yeah, I'd forgotten this since I'm usually thinking in terms of
immutable values.  This gives, I think, greater understanding of why
O'Caml's object system is made more powerful by not allowing object
fields to be accessed outside the object they're part of.  (As opposed
to more traditional languages, which allow it within the entire
class.)

Guess that row-polymorphic structs aren't such a good idea, then.  :)


An aside about object design and O'Caml:

Something I noted when explaining the O'Caml object system to some
friends was a couple of places where choice of interface can be rather
more subtle than, say, in Java.  Specifically in the
point/colored_point, circle/colored_circle examples from the manual
(which I changed a little in my examples).

class point =
  object
    val mutable x = 0
    method get_x = x
    method move d = x <- x + d
  end

type color =
  | Red
  | Green
  | Blue

class colored_point =
  object
    val mutable c = Red
    method get_color = c
    method set_color nc = c <- nc
  end

class ['a] circle (center : 'a) =
  object
    constraint 'a = #point
    val mutable center = center
    method get_center = center
    method set_center x = center <- x
    method move = center #move
  end

This was my first quick pass (you can tell I wasn't referring to the
manual too much.)  To my chagrin, even without the colored_circle
class, this doesn't perform the way you want it to:

# let p = new point
# let cp = new colored_point;;

> val p : point = <obj>
> val cp : colored_point = <obj>

# let c = new circle p
# let cc = new circle cp;;

> val c : point circle = <obj>
> val cc : colored_point circle = <obj>

# (cc :> point circle);;

> Characters 1-3:
> This expression cannot be coerced to type
>   point circle =
>     < get_center : point; move : int -> unit; set_center : point -> unit >;
> it has type
>   colored_point circle =
>     < get_center : colored_point; move : int -> unit;
>       set_center : colored_point -> unit >
> ... removed

Without even thinking, I chose a poor interface for my circle class.
In fact, the type of colored_point is unfortunate, too.  But since I
can't have subtypes of sum types in O'Caml, it's not really a problem.
If I were to use a class for this, or an O'Labl polymorphic variant,
then it becomes an issue.

The real problem in both of these cases is that in a powerfully typed
OO world like O'Caml, it's dangerous to treat a class as a container
when it isn't really.  First, it constrains the type overmuch, making
types you'd think to be subtypes not.  Second, a major part of what
this constraint is doing in the above case is revealing the
implementation details of the class.  I repeat the poor definition of
'a circle with notes and its class type:

# class ['a] circle (center : 'a) =
#   object
#     constraint 'a = #point
#     val mutable center = center
#     method get_center = center
#     method set_center x = center <- x
#     method move = center #move
#   end;;

> class ['a] circle :                    (* invariant 'a *)
>   'a ->
>   object
>     constraint 'a = #point
>     val mutable center : 'a
>     method get_center : 'a             (* covariant 'a *)
>     method set_center : 'a -> unit     (* contravariant 'a *)
>     method move : int -> unit
>   end

Okay, so the obvious symptom of the disease is that 'a appears
covariantly in get_center, and contravariantly in set_center.  But
what's the root cause of these symptoms?

Quite simply, I was clever and decided that if there were a get_blah
method, and blah is mutable, there ought to be a set_blah method.  Of
course, I was wrong.  Or was I?

The other aspect of this definition is that it reveals the type of the
center.  This is useful in one respect--we can use it to define
colored_circle:

# class ['a] colored_circle (p : 'a) =
#   object
#     inherit ['a] circle p
#     method get_color = p #get_color
#     method set_color = p #set_color
#   end

But here's a question: why do we want to expose the fact that the
implementation uses a colored_circle to contain its center??  This may
be a perfectly fine representation, but it's not really reasonable to
expose it in this way.

The model used by the documentation to get around this (though there
was no discussion of what was going on) was to delegate to the point
rather than allow it to be set.  But getting the center was still
allowed.  I don't think it should have been.  Here's are reasonable
class types for circle and colored_circle, assuming that the rest of
things (like how color works) are reasonable:

class type circle :
  object
    method set_center : point -> unit
    method get_center : point
    method move : int -> unit
  end

class type colored_circle :
  object
    inherit circle
    method set_color : color -> unit
    method get_color : color
  end

Now.  Why are these types appropriate?  Don't they restrict the
implementations to use only points?  Not in the least!  But what they
do do is hide the implementation from the user of the above interface.

The new semantics is that set_center means "move to the same position
as the passed-in point" and get_center means "return a point
representing the position of the center of the circle".  Of course,
one must also define whether or not changes in these points will
affect the circle.

Notice that colored_circle does not demand colored_points here.  We
can now write:

class colored_circle2 =
  object
    val mutable p = new point
    val mutable c = Red
    method set_center p' =
      let cx = p #get_x in
      let dx = p' #get_x - cx
      in p #move dx (* Whoops.  Point has no "set" method. *)
    method get_center = Oo.clone p
    method set_color c' = c <- c'
    method get_color = c
  end

This shows how something can satisfy the colored_circle interface more
easily now.

Finally, what we really want to say about the circle class type is (in
the latest O'Labl notation):

class type circle :
  object
    method set_center : 'a . #point as 'a -> unit
    method get_center : point
    method move : int -> unit
  end

This definition shows that anything implementing the same interface as
point may be used.  I'm still not entirely sure about this feature of
O'Labl.  Having the ability to make polymorphic methods is nice, but
the greater need to specify types of values in O'Labl is rather
upsetting.


So, I think the result of this experience is as follows:

  * Treating classes as containers when they're really only delegating
    work to another class is dangerous--you expose the nature of the
    class you're delegating to, and make it difficult for subtypes of
    your class to delegate to different types of objects.

  * Sometimes it is appropriate to use a specific type instead of an
    object-scope type variable.  Especially when you're setting up an
    API.  This allows you to further hide the implementation details
    from API users.

  * Finally, method-scope polymorphism makes life simpler since you
    can pass subtypes more freely, as you can do with function
    polymorphism.  (i.e. no more "circ #set_center (cp :> point)", or
    at least not as much.)


John.

Re: Thoughts on O'Labl O'Caml merge.

[skaller]

John Prevost wrote:
 
> Guess that row-polymorphic structs aren't such a good idea, then.  :)

	I don't follow your reasoning: the rules are more complex
than it might first seem just considering immutable fields.
But the correct rules are known, and easy enough to implement.

	The fact that these rules restrict the correctness of
use of mutable fields, is a consequence of correct typing,
not an obstacle to implementing the correct rules. :-)

> Something I noted when explaining the O'Caml object system to some
> friends was a couple of places where choice of interface can be rather
> more subtle than, say, in Java.  

	The ocaml object system has the advantage of type correctness,
which means that the limitations of object orientation are readily
apparent. This is not so obvious in an 'object oriented' language,
which is based from the start on a incoherent paradigm.

> Specifically in the
> point/colored_point, circle/colored_circle examples from the manual

> The real problem in both of these cases is that in a powerfully typed
> OO world like O'Caml, it's dangerous to treat a class as a container
> when it isn't really.  

	My opinion is quite different: object orientation
cannot possibly work. It is completely unsupported by any
coherent theory and can be so easily discredited by a single
example that it is clear adherents were simply ignorant
of basic theory. [no binary operator can be correctly
represented; more generally, no n-ary relation for n>1]

> Okay, so the obvious symptom of the disease is that 'a appears
> covariantly in get_center, and contravariantly in set_center.  But
> what's the root cause of these symptoms?

	Simple. The covariance problem is a direct consequence of
the incorrect assumption that a class can represent an abstraction.
We know from category theory that a CATEGORY and NOT a class
represents an abstraction, and an instance of the abstraction
must be a functor.

	If you examine 'inheritance' you find it is not
functorial. That is the problem. The paradigm is fatally
flawed because it fails to obey simple rules of mathematics.

	An abstract function A --> B in a category
must be instantiated as a function A' --> B',
and that function is specific. There is no 'polymorphism'
here. The polymorphism is entirely contained in the
choice of instantiating functor. The different instances
are 'unrelated' and cannot interoperate.

	Object orientation works in exactly one,
well defined, case: when the methods of the class
all have no arguments. [Technically, a function
with an invariant argument is to be viewed as
a family of functions with no arguments, for the
purpose of this theorem]

	As I undertand it, in ocaml, a module
is effectively a category, so we have the _correct_
model of abstraction in ocaml (even if it is restricted).
Furthermore, type variables are simply a shorthand for
using modules (with the advantage of implicit instantiation
rather than the explicit instantiation required for modules)

	Please note: this does not mean that classes
are useless! Contrarily, they're very convenient.
What it means is that _abstraction_ is not representable
this way, in general. Some cases are conveniently constructed
using classes: since I have an OO background, I do this
in my Python compiler. But I use ocaml signature
matching .. not inheritance .. and the covariance problem
is kept away only with some care, and because the use
of the classes and interfaces is not really 'abstract'.
[There are a finite set of classes with the signature,
which is adjusted to accomdate all the required uses,
sometimes with a little hackery thrown in]

-- 
John Skaller, mailto:skaller@maxtal.com.au
1/10 Toxteth Rd Glebe NSW 2037 Australia
homepage: http://www.maxtal.com.au/~skaller
downloads: http://www.triode.net.au/~skaller

Semantics for objects [Was: Thoughts on O'Labl O'Caml merge.]

[Francisco Valverde Albacete]

Il y a un petit resume en francais a la fin.
-----------------------

skaller wrote:

>         My opinion is quite different: object orientation
> cannot possibly work. It is completely unsupported by any
> coherent theory and can be so easily discredited by a single
> example that it is clear adherents were simply ignorant
> of basic theory. [no binary operator can be correctly
> represented; more generally, no n-ary relation for n>1]
>
> > Okay, so the obvious symptom of the disease is that 'a appears
> > covariantly in get_center, and contravariantly in set_center.  But
> > what's the root cause of these symptoms?
>
>         Simple. The covariance problem is a direct consequence of
> the incorrect assumption that a class can represent an abstraction.
> We know from category theory that a CATEGORY and NOT a class
> represents an abstraction, and an instance of the abstraction
> must be a functor.

I think there's some people trying to give final coalgebra semantics to
objects, certainly to "states". I have only began to understand the issue (I
look at it from the perspective of labelled transition systems), but the
landscape looks beautiful (if daunting!). Have a look at J.J.M.J. Rutten's
page

 http://www.cwi.nl/~janr/

or specifically for objects B. Jacobs:

 http://www.cwi.nl/~bjacobs/

I think you'll find this interesting:

B. Jacobs, Objects and classes, co-algebraically. In: B. Freitag, C.B.
Jones, C. Lengauer, and H.-J. Schek (eds)  Object-Orientation with
Parallelism and Persistence Kluwer Acad. Publ., 1996, p. 83--103.

Regards,

        Francisco Valverde
--------------------------------------
Resume en (affreux) francais:

Il semble qu'on peut assigner une semantique de coalgebre finale aux objects
et ses classes. V. les URL cites en haut.