<__DL__>
the usage of 'a 'b and 'c would be only when printing the type and reading it..
<smimou>
another way to cheat would be to use freshocaml
<__DL__>
yes, may be it would be more clean
<Axioplase>
__DL__: in fact, i have this types: type typ = Bool |Int | Star of typ*typ | Arrow of typ*ty | Var of string
<Axioplase>
and no a,b,c's...
<mattam>
is the problem with unifying a->b->c and b->c->a or ?
<Axioplase>
it is
<Axioplase>
can unify inductive or "weirdly" recursive types
<mattam>
you mean your unification function does not work for these types then ?
<Axioplase>
But at least, I raise an exception when not unifiable
<Axioplase>
mattam: yes, that's what i meant. sorry if i wasn't clear enough
<Axioplase>
(gosh i lag... 797seconds to sync with this channel)
<__DL__>
well, you have not given us a lot of information, but the idea (as I see it) is that unifying should be some recursive function that give not only the type, but the unification that have been done
<Axioplase>
well... unify (arrow(Var a, Bool)) (Arrow (Int,Var b)) shuold return [(Var a, Int);(Var b, Bool)] (which it does with such a simple test)
<__DL__>
what does it does on unify (Var a) (Var b) ?
<Axioplase>
[(Var a, Var b)]
<__DL__>
well, I don't see where is the probleme then...
<Axioplase>
unification (Fleche (Var"a",Var"b")) (Fleche (Int,Var"b"));; gives (typ * typ) list = [(Var "a", Int); (Var "b", Var "b")]
<Axioplase>
That is a problem... (fleche means "Arrow" but whatever)
<Axioplase>
errr
<Axioplase>
stupid me
<Axioplase>
__DL__: ok, unify ((a->b)->c)*a ((b->c)->a)*Int returns a=b, b=c, c=a, a=Int if i remove the Not_unifiable exception check, ot raises the exception. *Now* that is not a normal behaviour
<__DL__>
Bon, ben je vais te laisser a tes probleme d'unification, moi demain, je vais topologicet complet, mais tot... bonne nuit et bon courage...