Hacker News new | past | comments | ask | show | jobs | submit login

The usual justification, within PL Design community is that, similar to Russell 's Paradox, it's said that the anomaly caused by the unsound logic does not come up in practical situations. For example, some (and definitely most if not all mainstream) languages admit `Type: Type` i.e. `Type` itself is a type within the formalism. Of course, this is unsound and one common work-around is to use universe polymorphism such as `Type n: Type (level-suc n)`. But this comes with its own design issues as now you may need to pass level to each type (depends on the language, situation etc). So, some decide, since (as per this reasoning) absurd situations implied by "Type: Type" don't come up in practical situations, it's better have a simpler and more understandable yet unsound Type Theory. (But of course, an inconsistent theory can prove any claim, which is a huge problem in and of itself)

I have to note that I personally do not agree with this reasoning, yet afaik this is one of the justifications used to introduce rules to TT of a PL that is known to be unsound.

Realistically, it all depends on what you want to do with the type system. If you want to have a general purpose programming language that is not restricted by logical technicalities not well-understood by programmers, maybe it's better to admit "Type: Type" or similar. If you want to have a dependently typed programming language where any runtime program can potentially be a compile-time program, you may need more guarantees (e.g. you may need to know certain functions will halt).




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: