search

AndrasKovacs / elaboration-zoo

Minimal implementations for dependent type checking and elaboration
BSD 3-Clause "New" or "Revised" License
600 stars 34 forks source link

Should types be unified when unifying lambdas? #24

Closed atennapel closed 4 years ago

atennapel commented 4 years ago

I was looking at your implementation of Setoid Type Theory and I saw that there you do have types for lambda parameters in your core language. But during unification \(x : A). t1 ~ \(x : B). t2 then A ~ B is not unifed. Is there are a reason to not unify the types of lambda parameters?

AndrasKovacs commented 4 years ago

The precondition of unification is that the types of the sides are the same. When we get to unify two lambdas, we know that the types are the same, hence the domain types are also the same, so it's redundant to unify them.

atennapel commented 4 years ago

Ah yes, that makes total sense, thanks.