On Fri, 2007-11-30 at 00:01 +1100, skaller wrote:
> Now, add::string*string is NOT a binding of Real::add:u * u with
> u->t. This is a bug I think. t here is an abstract *invariant* type.
> It isn't a type variable which can be substituted. If t is float,
> ONLY add:float * float should be callable.
>
> So .. the hiding is correct, abstract t still hides every other type.
> But the *binding* of t to string shown by a subsequent instantiation
> failure is plain wrong. It would be right here:
>
> fun[u with Real[u]] ffmt[t with Real[t]] (v:t ...)
>
> if Felix allowed this, i.e. a type variable which isn't
> fixed by the call (however this isn't allowed).
This is all rather nasty. When I write:
open[t] Real[t];
then in
1 + 1 ... "x" + "x"
virtual bindings Real[int]::add and Real[string]::add should be used,
with distinct bindings for the 'previously free' variable t.
As pointed out, in the function case:
fun ffmt[t with Real[t]] (v:t) =>
1 + 1 ... "x" + "x" .. v+v
only the last addition should use Real::add because here
the variable t is already bound or 'momomorphised'.
Typically that means the binding is pushed into the environment
so it can be found by lookup, in the use expression is would
be called a 'free' variable, whereas when it is quantified
as in the 'open' case it would be called a bound variable..
very confusing because the names are opposite to the variable
status (but there you go!).
IN Felix, a variable is 'free' in MY sense of the word if
it is in a vs list, but not matched by a type in a ts list,
otherwise it is bound to the type in the ts list.
In the function, 't' is free when viewed from OUTSIDE the
function, but bound when viewed from INSIDE the function,
i.e. it switches from being a variable (quantified universally)
to being a constant (but bound to an unknown value).
Deduction cannot be applied in the second case, whereas
in the first case it is applied to each use separately.
The 'free vs. bound' distinction, so misnamed by type theorists <g>
is fundamental to understanding how a type evaluator works:
when drilling down into a type expression, the quantfier is
stripped off and the quantified variable pushed into the
environment, being 'freed' of the 'quantifier binding',
so that it switches from being 'free to bind a value to'
to in fact have a (possibly unknown) value bound to it.
In Felix compiler this actually happens: the variable is
registered in a symbol table and entering the function
that variable .. along with the functions parameters ..
are pushed into the environment.
However this is simply used during lookup to change the text
name of the variable to an integer index into the symbol
table. When examining an 'add' function call during overloading,
lookup will find the 'add' in 'Real' and incorrectly attempt
to bind the type variable in the symbol table .. when in fact
the variable is already bound. Felix should in fact note the
variable is in the vs list, already bound to a ts term,
so it should actually only accept a match of the monomorphised
*parameter* t against the variable used in the type class.
The point again is that in:
fun ffmt[t with Real[t]] (v:t, m: mode) =>
the lookup of a use of ffmt(double, ..) will actually instantiate
the monomorphised t -- the lookup inside the function of 'add'
cannot also bind t.
But it does. The lookup is the same in both this case and
when one says simply 'open[t] Real[t]' and this is just
wrong. It's the same because in the function case, typeclasses
are actually *implemented* exactly the same as for 'open'.
To put this another way the lookup is trying to work on
fun add[t]: t * t // use overloading to bind t
when it should be working on
var add: t * t // no overloading, t is a fixed type
[The actual code handling this is a mess ...]
--
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net
-------------------------------------------------------------------------
SF.Net email is sponsored by: The Future of Linux Business White Paper
from Novell. From the desktop to the data center, Linux is going
mainstream. Let it simplify your IT future.
http://altfarm.mediaplex.com/ad/ck/8857-50307-18918-4
_______________________________________________
Felix-language mailing list
Felix-language@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/felix-language
