Unification-free ("keyword") type checking

https://www.haskellforall.com/2024/02/unification-free-keyword-type-checking.html

The author claims that by removing some type inference (lambdas and generic instantiation) you can reduce the amount of code required to implement type-checking.

6 points · 3 comments · view on lemmy.world

3 Comments

kogasa@programming.dev · 2 pts · 2y

That's quite the drawback. I'm not sure if I believe a large number of keywords would have a good effect on ergonomics

mrkeen@mastodon.social · 2 pts · 2y (1 reply)

@armchair_progamer no mention of (mutual) recursion? It's been a while since I worked on my type checker, but I thought that you needed to separate inference into unification variable generation and constraint solving so that you don't fall into an infinite loop (each function asking the other functions type - forever).

armchair_progamer@programming.dev · 1 pts · 2y

You probably need to annotate recursive function return values. I know in some languages like Swift and Kotlin, at least in some cases this is required; and other languages have you annotate every function’s return value (or at least, every function which isn’t a lambda expression). So IMO it’s not even as much of a drawback as the other two.