Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Haskell Type Level Equality

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?
like image 752
Jogger Avatar asked Jul 24 '17 09:07

Jogger


People also ask

How do you check for equality in Haskell?

We can also compare two numerical values to see which one is larger. Haskell provides a number of tests including: < (less than), > (greater than), <= (less than or equal to) and >= (greater than or equal to). These tests work comparably to == (equal to).

What is a Typeclass in Haskell?

Type Classes are a language mechanism in Haskell designed to support general overloading in a principled way. They address each of the concerns raised above. They provide concise types to describe overloaded functions, so there is no expo- nential blow-up in the number of versions of an overloaded function.


1 Answers

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.

like image 148
pigworker Avatar answered Oct 21 '22 21:10

pigworker