Haskell Type Level Equality

Question

Haskell has a resticted syntax to define type families:

(1)   type family Length (xs :: [*]) where
(2)     Length '[] = 0
(3)     Length (x ': xs) = 1 + Length xs

On the lines (2) and (3) on the left side of the equal sign (=) we only have simple pattern matching. On the right side of the equal sign we have just type level function application and as a syntactic sugar there are type operators ((+) in line (3)).

There are no guards, no case expressions, no if-then-else syntax, no let and where's and there is no partial function application. This is not a problem, as the missing case expression can be replaced by a specialized type level function, that pattern matches on the different cases, the missing if-then-else syntax can be replaced by the If function of the Data.Type.Bool package.

Looking at some examples we see, that pattern matching syntax on the type level has at least one additional feature, not available in normal Haskell value level functions:

(1)   type family Contains (lst :: [a]) (elem :: a) where
(2)     Contains (x ': xs) (x) = 'True
(3)     Contains '[]       (x) = 'False
(4)     Contains (x ': xs) (y) = Contains xs (y)

In line (2) we use twice the variable x. Line (2) evaluates to 'True, if the head of the list of the first parameter is equal as the second parameter. If we do the same thing on a value level function, GHC answers with a Conflicting definitions for 'x' error. In value level functions we must add an Eq a => context to compile the function.

Type level pattern matching seems to work similar as unification back in the old times of Prolog. I unsuccessfully googled for some documentation about the syntax of type level functions.

• Why does GHC not require something like an a ~ b type equality constraint in the definition of the Contains type family?
• Is type equality always available?
• Has the type family syntax other additional features, that are unavailable on the value level?
• Where is this documented?

Answer 1

Haskell's type-level language is a purely first-order language, in which "application" is just another constructor, rather than a thing which computes. There are binding constructs, like forall, but the notion of equality for type-level stuff is fundamentally mere alpha-equivalence: structural up to renaming of bound variables. Indeed, the whole of our constructor-class machinery, monads, etc relies on being able to take an application m v apart unambiguously.

Type-level functions don't really live in the type-level language as first-class citizens: only their full applications do. We end up with an equational (for the ~ notion of equality) theory of type-level expressions in which constraints are expressed and solved, but the underlying notion of value that these expressions denote is always first-order, and thus always equippable with equality.

Hence it always makes sense to interpret repeated pattern variables by a structural equality test, which is exactly how pattern matching was designed in its original 1969 incarnation, as an extension to another language rooted in a fundamentally first-order notion of value, LISP.