3 ms·
Syntactic closures are a way to hide the fact that lambdas are the only abstraction in lambda calculus. The work that I cited has types _and_ quotation as firs
by llm_trw 3y ago
Syntactic closures are a way to hide the fact that lambdas are the only abstraction in lambda calculus.
The work that I cited has types _and_ quotation as first class abstractions.
It's a bit like asking to explain proof theory in terms of Godel numbers. Sure you can technically do it. You're completely missing the point if you do however.
- kazinator 3y agoI think syntactic closures don't have to be concerned with type, because their job is just to ensure that the symbols included in a quote refer to what they are supposed to refer to, regardless to where that quote is moved. When the closures are evoked, reasoning about types can take place then.