Re: [Caml-list] Hashtbl iter semantics

[John Max Skaller <skaller@ozemail.com.au>]

Francois Pottier wrote:

>but the usual way to perform unification
>in the presence of cyclic (equi-recursive) terms is to physically unify two
>nodes *before* looking at their sub-terms (instead of *after*, or not at all,
>in the non-cyclic case). This way, if you run into a cycle and you end up
>attempting to unify the same two nodes, you will succeed immediately, provided
>your first step is to check for physical equality. I can provide some sample
>code if that helps.
>
Should be ok: that's what Cardelli's comparison does (which I have 
implemented).

>
>That said, type inference in the presence of equi-recursive types is considered
>difficult for the user to figure out... many intuitively `meaningless' programs
>admit (weird) recursive types.
>
Sure, but I'm not doing "type inference", but "type deduction".
The types of function arguments *must* be declared.
Felix deduces the type of expressions, and thus variables,
and also function return types (in most cases :-))

I chose that strategy for two reasons: (1) full scale type inference
is difficult to implement, difficult to understand, and very difficult to
give good error messages. (2) Felix supports overloading.
If type inference with overloading is tractible, it is surely even
more difficult to implement and understand.

The current rule for generic functions is that type arguments
must be explicitly given. (I hope to relax that later ..)

Actually, I uave two kinds of type variables;

    1) initially unknown function return types
    2) variables in generics

The first kind aren't 'variable'  (they have single type, it just isn't
known yet). The second kind are just parameters which
have to be explicitly bound to types by the client.

So the scope of the 'unification' algorithm is (1) deducing
function return types, and (2) comparing two generic
types to see if one matches the other.

(1) is implemented, but the algorithm is very unsatisfying.
The problem is that during deduction it is necessary to
perform overload resoliution: I can't handle partial matching
here, so all the type variables have to be eliminated at that point.

-- 
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850




-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners