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?