3 ms·
I'm sure the typechecker is as simple as you suggest for GP's language; but not showing it at all makes for an unfair comparison with the article. But the evalu
by cvoss 3y ago
I'm sure the typechecker is as simple as you suggest for GP's language; but not showing it at all makes for an unfair comparison with the article. But the evaluator? Without out the trick of notation that is [x/y] substitution? It's not simple!
You are right that the typechecker gets significantly more complicated if type annotations are optional. But the article and the paper are about real implementations of the language, not arm-chair ones where the burden of type annotations isn't important.
- solomonb 3y agoThats fair. I'm not GP but I do tend to agree that the AST used in that paper is overly complicated. Here is an STLC with bidir example which I believe to be easier to understand: https://github.com/solomon-b/lambda-calculus-hs/blob/main/main/01-BidirectionalTypechecking.hs https://github.com/solomon-b/lambda-calculus-hs/blob/main/ma...