Thoughts on O'Labl O'Caml merge.
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  19991018 (14:10) 
From:  skaller <skaller@m...> 
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