5 ms·
Rich brought this up in his Strange Loop talk [1]. All the attempts he had seen either disallowed perfectly valid uses or allowed invalid ones. I believe to rea
by asolove 12y ago
Rich brought this up in his Strange Loop talk [1]. All the attempts he had seen either disallowed perfectly valid uses or allowed invalid ones. I believe to really guarantee early termination and a few other tricky invariants of reducers you would need a linear type system. [2]
[1] https://www.youtube.com/watch?v=6mTbuzafcII https://www.youtube.com/watch?v=6mTbuzafcII
[2] http://en.wikipedia.org/wiki/Substructural_type_system#Linear_type_systems http://en.wikipedia.org/wiki/Substructural_type_system#Linea...
- tome 12y agoWhat's wrong with allowing invalid ones? Surely transducers in an untyped language allow invalid ones too.
- icambron 12y agoTo the degree that it allows invalid types, it's weakly typed. That's fine as a compromise (no type system is perfect), but the same impulse that says you should type in the first place also says you should only allow valid types. It's a challenge type systems should aspire to solve.
- tome 12y agoThey should certainly aspire to solve it, but the inability to type one aspect of your program isn't an argument against types.
- icambron 12y agoThat you can't type it isn't an argument against types, but that you can't type it and that's perfectly fine with you suggests you don't actually think types are that important.
- eli_gottlieb 12y agoType systems do aspire to solve it, but we run into Rice's Theorem pretty quickly.
- mej10 12y agoThen perhaps it is a great example for the author's thesis.