4 ms·
> Thus, with type aliases, the type equality problem becomes the higher-order unification problem, which is not decidable. I wonder how much this is a problem
by skulk 2y ago
> Thus, with type aliases, the type equality problem becomes the higher-order unification problem, which is not decidable.
I wonder how much this is a problem in practice, aside from the type-checker taking too long.
- nerdponx 2y agoIt's tractable in practice. That's what the Idris (2) language does, for example.
- dunham 2y agoIf anyone is interested in how this works, I've found András Kovács' "Elaboration Zoo" to be a good tutorial: https://github.com/AndrasKovacs/elaboration-zoo https://github.com/AndrasKovacs/elaboration-zoo It incrementally covers normalization by evaluation, bidirectional typechecking, basic pattern unification, implicit insertion (which relies on unification), and then more sophisticated variants on pattern unification.