2 ms·
Personally, I consider teaching the lambda calculus to be a real-life situation. Teaching the lambda calculus is no less real to me than any other part of my l
by lisper 6y ago
Personally, I consider teaching the lambda calculus to be a real-life situation. Teaching the lambda calculus is no less real to me than any other part of my life. But OK, self-apply is not something you're likely to see in production code, and neither are Church numerals, which is where this problem shows up for real. But MAP, REDUCE, and APPLY are, and they all have the same problem as self-apply: their static types are infinite.
This is a general problem with all static type systems. There are only two possibilities: either your type system is Turing complete or it is not. If it is not, then there are things that one might reasonably want to express that cannot be expressed, and if it is, then it is undecidable. Static typing is either constraining, or it is a Turing Tarpit (https://en.wikipedia.org/wiki/Turing_tarpit https://en.wikipedia.org/wiki/Turing_tarpit).
- adwn 6y ago> But MAP, REDUCE, and APPLY are, and they all have the same problem as self-apply: their static types are infinite. Huh? Any semi-decent static type system has no problems modeling higher-order functions, and static types can easily be infinite via parametric polymorphism ("generics"). > Static typing is either constraining, or it is a Turing Tarpit You're letting the perfect be the enemy of the good. Static type systems can be beneficial even when they don't solve every conceivable problem.
- lisper 6y ago> Static type systems can be beneficial I don't deny that. The problem is not with the idea, it's with the (usual) implementation, which is that if you don't appease the type-checker it won't let you run your program. I'm perfectly fine with a type checker that only gives me warnings but still allows me to run the code even if it isn't satisfied.