🎓 A1Learner
🔍
0 of 47 lessons completed

Haskell Type-Level Naturals

A type-level natural is a natural number that lives in a type. It lets a type record a count, such as the length of a vector.

A vector type records its length

vlen counts the elements of any vector. A vector built from two elements has length two.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
data Nat = Z | S Nat
data Vec (n :: Nat) a where
  VNil :: Vec 'Z a
  VCons :: a -> Vec n a -> Vec ('S n) a
vlen :: Vec n a -> Int
vlen VNil = 0
vlen (VCons _ xs) = 1 + vlen xs
main :: IO ()
main = print (vlen (VCons 7 (VCons 8 VNil)))

A non-empty vector always has a head

vhead demands a vector whose type starts with a successor. The one-element vector yields its single element.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
data Nat = Z | S Nat
data Vec (n :: Nat) a where
  VNil :: Vec 'Z a
  VCons :: a -> Vec n a -> Vec ('S n) a
vhead :: Vec ('S n) a -> a
vhead (VCons x _) = x
main :: IO ()
main = print (vhead (VCons 7 VNil))

A tail drops exactly one element

vtail removes the head of a non-empty vector. The tail of a two-element vector has length one.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
data Nat = Z | S Nat
data Vec (n :: Nat) a where
  VNil :: Vec 'Z a
  VCons :: a -> Vec n a -> Vec ('S n) a
vlen :: Vec n a -> Int
vlen VNil = 0
vlen (VCons _ xs) = 1 + vlen xs
vtail :: Vec ('S n) a -> Vec n a
vtail (VCons _ xs) = xs
main :: IO ()
main = print (vlen (vtail (VCons 5 (VCons 6 VNil))))

Example

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
data Nat = Z | S Nat
data Vec (n :: Nat) a where
  VNil :: Vec 'Z a
  VCons :: a -> Vec n a -> Vec ('S n) a
vlen :: Vec n a -> Int
vlen VNil = 0
vlen (VCons _ xs) = 1 + vlen xs
vhead :: Vec ('S n) a -> a
vhead (VCons x _) = x
vtail :: Vec ('S n) a -> Vec n a
vtail (VCons _ xs) = xs
vec :: Vec ('S ('S ('S 'Z))) Int
vec = VCons 7 (VCons 8 (VCons 9 VNil))
main :: IO ()
main = do
  print (vhead vec)
  print (vlen vec)
  print (vlen (vtail vec))

Key points

  • Nat: a small data type with Z for zero and S for the successor of another natural.
  • Promotion: DataKinds turns Nat into a kind and Z and S into types.
  • Tick form: the type for two is written with ticks and nested successors.
  • Vector: a length-indexed vector carries its length in its type.
  • Use a length-indexed vector to make an empty vector impossible to pass where a non-empty one is needed.

In this example, vec is a three-element vector whose type records three successors. vhead reads its first element and vlen counts all three elements. vtail drops the first element, so its length counts two. main prints the head, the full length, and the tail length in that order.

Note

a type-level natural is checked at compile time, so a wrong length never reaches a run.

Try it Yourself

Edit the code, then press Run.

Running is simulated · Haskell Playground

Exercise

What does the type of VCons 7 VNil record?