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