On Sep 11, 2006, at 9:34 PM, skaller wrote:
> Ok, typeclasses are up to the critical point. The data flow works
> up to overload resolution now.
While you have been hard at work on Felix, I have been out climbing--
just kidding. I have three projects I am attempting to work on
simultaneously and they all seem to require further study (on my
part) to be done well. Felix seems to fill out the free time (and
makes a sometimes too interesting diversion).
> Here's the problem. At present Felix uses something like a list
> of hastables for lookup. The tables go:
>
> string -> int
>
> The result of a lookup is roughly
>
> int, ts
>
> where ts is a list of types. This list represents a type substitution
> as follows: when we lookup the integer key in the symbol table,
> we get a list of type variables used as universal quantifiers.
> For example
>
> fun f[t,u] (x:t, y:u) => ...
>
> Here function f is entry 1234 in the symbol table, and the
> symbol record contains the list
>
> t,u
>
> The ts list might be
>
> int, float
>
> which makes a binding:
>
> t-> int, u-> float
>
>
> This is encoded directly into the generated intermediate
> language with an Ocaml combinator such as
>
> `BEXPR_closure (1234,[int_term;float_term])
>
> The instantiator tracks that
>
> i, [int;float]
>
> is required, and generates an instantiation j
>
> (i,[int;float]) -> j
>
> stored in another hashtable. This is used to (a) uniquely
> number the C++ class which will be generated, (b) ensure
> instantiations are unique, and (c) ensure unused combinations
> do NOT get instantiated.
>
> Now, if we 'add' the scope of a typeclass into the environment,
> everything will work very well.
>
> The problem is it will work TOO well. It will bind function
> calls by specialising the type variables of the typeclass
> separately on EVERY call.
There are two problems, aside from those you mentioned:
(1) the typeclass should redirect to the typeclass instantiation
_for_that_type_. In your example:
> typeclass X[u,v] { fun add: u * v -> u; }
> fun f[s,t where X[s,t]] (x:s,y:t) { .. add(x,y) .. }
somewhere there should have been an instance of typeclass X:
instance X[s,t] {
fun add: s * t -> u;
}
Note: "instance" here, and probably the same for open X[s,t] in your
module example, means a user-defined instance which creates a
separate instance-held hash table for lookup.
(2) the lookup does not replace type variables (that would, as you
noted, override the function definition); the lookup should *match*
the corresponding types of the function's type variables (the current
hash table) and the types of the typeclass/module instance (the
separate table created by the user-defined "instance X[s,t]"). If
the corresponding types to not match, it is a type error.
For a parametrically polymorphic function, there are two times type
checking by matching occurs:
(a) when the function is defined, for any typeclass-bound functions
used inside the checked function
(b) when the parametrically polymorphic function is used in a
concrete instance: the call signature (when the type variables are
resolved to their real types).
> What we ACTUALLY need to do is: specialise the typeclass
> based on the types supplied in the function in the
> where clause,
This specialisation should be done only in the user-defined instance
declaration for the typeclass.
> [If the typeclass itself, or the candidate function,
> is parametrically polymorphic THAT type variable
> will be bound however.]
It is not the type variable but the type that should be bound, at (a)
or (b), as above.
> The problem here is exactly equivalent to this:
>
> open X[s,t];
>
> were X a module: we want to open an *instance* of X
> for lookup, for which u,v are replaced by the arguments s,t.
It is the replacement that is a problem.
> I want to be very clear what the problem is: the Felix lookup
> routines expect a symbol table entry with a list of type
> variable names, meta-variable 'vs', and it uses a match
> of the function signature, expressed in these variables,
> against the actual call signature, to find a most general
> unifier, using unification, with a constraint on the unification
> algorithm it is only permitted to find substitutions for the vs.
> [In other words, 'solves these equations for a specified set
> of dependent variables, the RHS containing independent variables]
If you try to retain only one hash table for the program, this will
fail (as it has). What you need are separate hash tables for the
instances of modules/typeclasses so the variables won't be replaced
and you can match the actual call signature types against the module/
typeclass instances.
> The ONLY way to do this is to create a completely new symbol table
> which contains the specialised version of the typeclass,
This should have been created *only* at the user-defined typeclass/
module instance, it should not have been created when used in the
function.
> We have to do all this, to ensure the bindings all
> go to the one typeclass instance X[s,t] specified
> in the function.
Exactly the problem. The typeclass instance should not be specified
here but separately.
Would you be able to point out exactly where all this is in the OCaml
code? I can find some of it but if I had a general idea of which
source code files & lines things belonged to I might be able to
figure it out and help more. My simple problem is that I am getting
lost and wasting time trying to map everything out myself :(
-Pete
-------------------------------------------------------------------------
Using Tomcat but need to do more? Need to support web services, security?
Get stuff done quickly with pre-integrated technology to make your job easier
Download IBM WebSphere Application Server v.1.0.1 based on Apache Geronimo
http://sel.as-us.falkag.net/sel?cmd=lnk&kid=120709&bid=263057&dat=121642
_______________________________________________
Felix-language mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/felix-language
