🎓 A1Learner
🔍
0 of 47 lessons completed

Haskell Type-Level Lists

A type-level list is a list that lives in a type. It lets a type record a sequence of types, such as the types in a mixed row.

A mixed row has a head of its own type

hhead reads the first element of a non-empty mixed row. The row starting with 7 yields 7.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
import Data.Kind (Type)
data HList (ts :: [Type]) where
  HNil :: HList '[]
  HCons :: t -> HList ts -> HList (t ': ts)
hhead :: HList (t ': ts) -> t
hhead (HCons x _) = x
main :: IO ()
main = print (hhead (HCons 7 (HCons True HNil)))

A mixed row has a countable length

hlen counts the cells of any mixed row. A row with three cells has length three.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
import Data.Kind (Type)
data HList (ts :: [Type]) where
  HNil :: HList '[]
  HCons :: t -> HList ts -> HList (t ': ts)
hlen :: HList ts -> Int
hlen HNil = 0
hlen (HCons _ xs) = 1 + hlen xs
main :: IO ()
main = print (hlen (HCons "hi" (HCons 3 (HCons True HNil))))

A tail exposes the second position

htail drops the first cell of a mixed row. The head of that tail is the second element.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
import Data.Kind (Type)
data HList (ts :: [Type]) where
  HNil :: HList '[]
  HCons :: t -> HList ts -> HList (t ': ts)
hhead :: HList (t ': ts) -> t
hhead (HCons x _) = x
htail :: HList (t ': ts) -> HList ts
htail (HCons _ xs) = xs
main :: IO ()
main = print (hhead (htail (HCons "a" (HCons 42 (HCons True HNil)))))

Example

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
import Data.Kind (Type)
data HList (ts :: [Type]) where
  HNil :: HList '[]
  HCons :: t -> HList ts -> HList (t ': ts)
hhead :: HList (t ': ts) -> t
hhead (HCons x _) = x
htail :: HList (t ': ts) -> HList ts
htail (HCons _ xs) = xs
row :: HList '[String, Int, Bool]
row = HCons "Ana" (HCons 31 (HCons True HNil))
main :: IO ()
main = do
  putStrLn (hhead row)
  print (hhead (htail row))
  print (hhead (htail (htail row)))

Key points

  • Heterogeneous list: a list whose elements may have different types.
  • Promotion: DataKinds turns the list type into a kind for type-level lists.
  • Empty form: the empty type-level list is written as an empty ticked list.
  • Cons form: a type-level cons joins one type to a type-level list.
  • Use a type-level list to give each position in a mixed row its own type.

In this example, row is a mixed row whose type records String, then Int, then Bool. hhead reads the name and htail moves one position along the row. main prints the name, then the age from the second position, then the flag from the third position.

Note

the heterogeneous list uses the GADT form, where each constructor picks its own result type.

Try it Yourself

Edit the code, then press Run.

Running is simulated · Haskell Playground

Exercise

What does HCons 7 (HCons True HNil) record at the type level?