On Wed, 2004-10-27 at 11:54, Rhythmic Fistman wrote:
> Ok, I've condensed it to this:
OK, i've posted new tarball to fix this.
The fix isn't guarranteed: a pair of lvalue prefixes
could creep in somewhere I didn't modify.
There is a way to guarratee that the idempotent lvalue
combinator is uniquely represented by a single lvalue term
wherever a term is analysed -- I can write a routine
that fixes up such terms. However it is expensive
to do the requisite recursive descent when it should
be possible to prove such a term cannot be constructed.
So I'm going to try to do the checking only when
converting a term to its lvalue equivalent.
When an unbound term is bound, this needs to be done too.
var x : lvalue [lvalue [ lvalue [int ] ] ];
however this is slightly messier .. you might also have
fun f: lvalue[lvalue[int]] -> int
and now the 'lvalue' isn't at the top level.
BTW: the current unification algorithm is almost certainly
WRONG. The decay
lvalue[int] -> int
in an argument is just like the decay
derived_type -> base_type
in a C++ pointer, from a subtype to a supertype.
When a *function* is used as an argument, however,
the rule is that you can accept a function with
a weaker precondition and stronger post condition,
which means the function may accept a supertype as its
argument, and return a subtype. For example:
fun f (g: b -> b') (x:b) => g x;
If you have classes:
b : a b' : a'
c : b c' : c'
Then you can pass f a function of type
a -> c'
and everything will work. This is because x is type b,
and every b is an a, and the result will be a c',
and every c' is a b'.
So you can see for a *subtype* a -> c of b-> b'
the rule is that b must be a subtype of a, and b'
must be a supertype of c'.
We say this compactly by saying the domain is
contravariant, and the codomain is covariant.
This means that for the arrow
t ---- subtype ----> t'
the arrows for domain and codomain when t = b -> b' go in the
opposite and same direction, respectively, as the whole subtype
b <-----subtype ------ a // contra variant
| ----- subtype ----> |
b' ---- subtype -----> c' // co variant
This is the rule that totally destroys Object Orientation
as a useful general development paradigm. OO requires
arguments to be covariant, and mathematics tells us
that they have to be contravariant for the type system
to be sound. In particular for addition:
add: a -> a -> a
where 'a' is an abstract type, the first a is the 'object',
the second 'a' the method argument, and the final 'a' the result,
we need to implement for a concrete subtype b : a the following:
add: b -> b -> b
which is covariant in all three terms. The problem is that
the second 'b' must be *contravariant*, and the only
way to be contra and co variant at once is to be invariant,
so the only possible sound signature is actually:
add : b -> a -> b
which means the method argument has to be of the abstract type.
But then, you cannot implement the method! You can't add
a concrete b kind of number to an abstract one because
addition is a primitive defining operation.
What do people do? They cheat and use downcasts a -> b
inside the method, which means it isn't fully polymorphic:
it won't work, if you add new subtypes b', b'', b''' of a,
without invading the add method and adding a case
for each one. The problem here is that if you forget,
you will just get a run time error. The type system
has failed to ensure soundness, by *requiring*
the programmer to use casts to work around a flawed
design concept .. namely OO itself.
Well the bottom line is that the unification algorithm
must respect covariance/contravariance rules for function
subtypes. In particular,
lvalue[t] is a subtype of t
The current unification algorithm is unsound, because it
actually allows a function of type
lvalue[d] -> lvalue[c]
to be used where one of type
d -> c
is required. I hope this will not cause any problems
in the short term -- the fix isn't entirely trivial.
I will need to upgrade the unification algorithm to
support subtyping. The rules and algorithm are well
known for *functional* programs .. but Felix isn't
entirely functional .. :)
For example, I think in a purely functional FP
using boxed representations, a struct is a subtype
of another if (a) it has missing fields (some can
be added though) and (b) each field is a supertype.
Thus in C++ terms the extra field can be sliced off,
since the function isn't using them, and we need
the remaining fields to be contravariant -- we're
happy if the supplied field is a supertype, because
any use of it will be a function application, which
will accept any supertype of its specified argument type.
However with *mutable* structures, the result type
matters as well -- when you modify something it is both
an argument and a result of a functional interpretation
which means it must be both contravariant and covariant,
which implies invariance.
lvalues are intended to represent mutable storage .. :)
In addition, there is an issue for overload resolution.
Specialisation of generics is a kind of subtyping,
but it is different for plain subtyping, and handling
both is hard, since it is never clear which
of a set of overloads is 'most specialised'.
C++ has to handle this already but I doubt many people
know which is prefered .. a template accepting a more general
type with a the argument being upcast, or a more specialised
template with no cast .. especially when you need to do
BOTH kinds of subtyping to get any kind of match at all.
Felix currently avoids that by not implementing any subtyping,
and requiring the client to do any casting needed to get
the right 'exact' match... except in one case .. lvalues :)
John Skaller, mailto:skaller@...
snail: PO BOX 401 Glebe NSW 2037 Australia
Checkout the Felix programming language http://felix.sf.net