0
$\begingroup$

I was reading about type unification and it moves through of substitution of variables. To me it looks like a search for an alpha equivalence... I mean, two types are unifiable if they are alpha equivalent, at last if they are in polymorphic form, is this right?

If I have forall a.a -> a and forall b.b -> b I can apply [b/a]forall a.a -> a to achieve forall a.a -> a. So they are unifiable!?

Going deeper I could unify forall a.a -> a to int -> int and then deduce that the first is more general because I can achieve the second by [a/int] substitution on the first right?

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ Where were you reading this? It might help to know the context of your question. Certainly unification is not $\alpha$-equivalence in general, if that's all you're asking. $\endgroup$
    – cody
    Dec 10 '20 at 18:38
  • $\begingroup$ cs.cornell.edu/courses/cs3110/2011sp/Lectures/… It was just a reasoning, I read about substitution and then this come to me that type unification may have some parallel with alpha equivalence $\endgroup$
    – geckos
    Dec 10 '20 at 20:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.