Matthias Benkard, Type Checking Without Types

Matthias Benkard
Type Checking Without Types

We propose a programming language with a type system roughly based on dependent types, but built on top of mereology rather than set theory (and thus without the need for a Set type). In our formalism, typing is equivalent to subtyping; that is, a value is a member of the type T iff it is a subtype of T.

Since every value is a type, there is no need for special syntax for the declaration or definition of types. In particular, algebraic data types can be defined through the same fixed-point mechanism that is used for recursive function definitions. Similarly, arrow types are functions, employing pattern matching just as their ``members'' do. Finally, Sigma-types can be represented by object comprehensions.