Hacker News Reader

Comment by somewhereoutth | Hacker News Reader

Should a language be able to form predicates total over all possible expressions in the language (including these predicate expressions) in a non trivial way, could these be then identified as 'types' in the sense that each can partition the set of all expressions in the language into 'of the type' and 'not of the type'? Is this still type theory, or something else?

View on HN

Usually it's not possible to form such a predicate. If we have impredicative base universe, then it's possible to form a predicate over all types in the base universe (which may or may not be all types in the language), including the predicate itself. However, this feature is rarely used in type theory, because it is incompatible with classical logic.

In programming, this is more commonly available, because we don't necessarily care about propositions, let alone classical logical proofs. The polymorphic identity function type `forall a. a -> a` in System F quantifies over all types including itself.

> Should a language be able to form predicates total over all possible expressions in the language (including these predicate expressions) in a non trivial way, could these be then identified as 'types' in the sense that each can partition the set of all expressions in the language into 'of the type' and 'not of the type'?

Normally you'd want to give each term a single type, rather than say that terms do or don't have a bunch of different predicate types.

> Is this still type theory, or something else?

If your predicates apply opaquely to complete expressions then it's not (nontrivial) type theory. The point of type theory is that your typing rules tell you the types of your expressions (or whether they're validly typed at all) in terms of the types of their subexpressions.

Reply on news.ycombinator.com