Type-Level List Search


We will take a quick look at how to handle element search in two kinds of type lists: cons style lists and native Haskell lists. We only need three language pragmas.

For the cons style list, we can actually build it without relying on TypeOperators. We will work with simple data types of kind * -> * so we can make a simple cons like list. They do not need constructors because we will not make any values.

Next we define a type family to encapsulate the idea of equality between types. We just pattern match on the types.

The list is not empty and the single type is the same type as the item in

The list is empty.

The list is not empty, but it does not match the type on the right-hand side. Run ConsContains again but without the head of the list.

This function will only compile if you pass a type that is in the cons list. It uses ~ to try to match TypeLevelTrue with the result of ConsContains.

This function will only compile if you pass a type that is not in the cons list. The same idea as above but it tries to match TypeLevelFalse.

Now we will do the same thing but use native Haskell type level lists.

This is quite similar to the code above with a few small changes. The list type is now a list of kind*, written as [*]. We need to use ' to promote the list splitter : to a type level list splitter ':. Then we return type level boolean values 'True and 'False.

Now we can use lists instead of types that are embedded in each other. A type level list needs to be declared with '[] and the result of Contains should match 'True or 'False.

All of the uncommented code will compile.

If you uncomment any of the other lines you will see an error like this.