I need to revisit my notes on how I was going to compile pattern matching down to unification in my metalanguage.

I'm pretty sure it's possible, but it's always going to be pretty tricky.

but the basic idea is that if you're reading typechecking judgments from a lens of unification (not bidirectional), every pattern match is actually unification, not a literal pattern match on AST

the interesting stuff I want to handle is ambiguity … how do you deal with ambiguous typings (this requires an actual algebra of unification, via (semi)lattices)

edit: I should clarify

typechecking should proceed by induction on syntax of terms, you expect to have one case for each part of syntax, and there's no unification there (it doesn't really make sense)

but when you mention types, that acts via unification


You must log in to comment.