**Next message:**skaller: "Re: Rebinding exception declarations"**Previous message:**skaller: "Re: Proposal for study: Add a categorical Initial type to ocaml"**Maybe in reply to:**John Prevost: "Thoughts on O'Labl O'Caml merge."**Next in thread:**skaller: "Re: Thoughts on O'Labl O'Caml merge."**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

Date: Sun, 17 Oct 1999 21:01:37 +1000

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

To: John Prevost <prevost@maya.com>

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

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

**Next message:**skaller: "Re: Rebinding exception declarations"**Previous message:**skaller: "Re: Proposal for study: Add a categorical Initial type to ocaml"**Maybe in reply to:**John Prevost: "Thoughts on O'Labl O'Caml merge."**Next in thread:**skaller: "Re: Thoughts on O'Labl O'Caml merge."**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

*
This archive was generated by hypermail 2b29
: Sun Jan 02 2000 - 11:58:27 MET
*