14 ms·
Given that it appears that this type system has a universal type (or top type) in the form of the "term()" type in this paper, how does it avoid Girard's parado
by tolmasky 3y ago
Given that it appears that this type system has a universal type (or top type) in the form of the "term()" type in this paper, how does it avoid Girard's paradox[1]? Is it because the the rest of the type system isn't sufficiently expressive to run into it (by allowing dependent types or other higher-order polymorphism?). If so, does this mean it will be difficult to add such features?
1. Scroll down to "Girard's Paradox" here: https://en.wikipedia.org/wiki/System_U https://en.wikipedia.org/wiki/System_U
- weatherlight 3y agoThe proposed type system for Elixir doesn't run into Girard's paradox because it doesn't allow for impredicative polymorphism, which is where the paradox arises. The type system is based on set-theoretic types and includes a top type (the term() type), but it doesn't allow for types to be quantified over all types. As for adding features like dependent types or higher-order polymorphism, these would increase the type system's complexity and could potentially lead to issues like Girard's paradox. The authors don't discuss adding such features, so it's unclear how difficult it would be.
- samth 3y agoEvery type is inhabited in most type systems for general-purpose programming languages. For example, to inhabit a type T in Haskell syntax (the same approach works in basically any language): f :: () -> T f x = f x myT = f () What this shows is that Haskell types are not sound as a logic, but that doesn't mean they aren't a fine type system.