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.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
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
.
consContains :: (TypeLevelTrue ~ ConsContains (A (B ())) a) => a -> IO ()
consContains _ = print "Type found in cons list."
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
.
consDoesNotContain :: (TypeLevelFalse ~ ConsContains (A (B ())) a) => a -> IO ()
consDoesNotContain _ = print "Type not in the cons list."
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
.
type family Contains (list :: [*]) (single :: *) where
Contains (x ': xs) (x) = 'True
Contains '[] (x) = 'False
Contains (x ': xs) (y) = Contains xs (y)
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
.
contains :: ('True ~ Contains '[X,Y] a) => a -> IO ()
contains _ = print "Type found in list."
doesNotContain :: ('False ~ Contains '[X,Y] a) => a -> IO ()
doesNotContain _ = print "Type not in list."
All of the uncommented code will compile.
main = do
consContains (undefined :: A ())
-- consContains (undefined :: C ()) -- the compiler will not compile this
consDoesNotContain (undefined :: C ())
-- conDoesNotContain (undefined :: A ()) -- the compiler will not compile this
contains (undefined :: Y)
-- contains (undefined :: Z) -- the compiler will not compile this
doesNotContain (undefined :: Z)
-- doesNotContain (undefined :: Y) -- the compiler will not compile this
If you uncomment any of the other lines you will see an error like this.
• Couldn't match type ‘TypeLevelTrue’ with ‘TypeLevelFalse’
arising from a use of ‘consContains’
• In a stmt of a 'do' block: consContains (undefined :: C ())
In the expression:
do { consContains (undefined :: A ());
consContains (undefined :: C ());
consDoesNotContain (undefined :: C ());
contains (undefined :: Y);
.... }
In an equation for ‘main’:
main
= do { consContains (undefined :: A ());
consContains (undefined :: C ());
consDoesNotContain (undefined :: C ());
.... }