Haskell Singleton Pattern

A singleton is a value that mirrors one type exactly. It lets a runtime function learn a type-level fact, such as a length, that types alone cannot pass to runtime.

A singleton counts at runtime

natToInt turns a singleton natural into an ordinary number. Two successors give the number two.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
data Nat = Z | S Nat
data SNat (n :: Nat) where
  SZ :: SNat 'Z
  SS :: SNat n -> SNat ('S n)
natToInt :: SNat n -> Int
natToInt SZ = 0
natToInt (SS n) = 1 + natToInt n
main :: IO ()
main = print (natToInt (SS (SS SZ)))

A singleton fixes a vector length

rep builds a vector with one copy per successor in the singleton. A two-successor singleton builds a vector of 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
data SNat (n :: Nat) where
  SZ :: SNat 'Z
  SS :: SNat n -> SNat ('S n)
vlen :: Vec n a -> Int
vlen VNil = 0
vlen (VCons _ xs) = 1 + vlen xs
rep :: SNat n -> a -> Vec n a
rep SZ _ = VNil
rep (SS n) x = VCons x (rep n x)
main :: IO ()
main = print (vlen (rep (SS (SS SZ)) 9))

Matching a singleton names the count

singName matches the shape of a singleton natural. One successor is named one and two successors are named many.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
data Nat = Z | S Nat
data SNat (n :: Nat) where
  SZ :: SNat 'Z
  SS :: SNat n -> SNat ('S n)
singName :: SNat n -> String
singName SZ = "zero"
singName (SS SZ) = "one"
singName (SS (SS _)) = "many"
main :: IO ()
main = do
  putStrLn (singName (SS SZ))
  putStrLn (singName (SS (SS SZ)))

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
data SNat (n :: Nat) where
  SZ :: SNat 'Z
  SS :: SNat n -> SNat ('S n)
vlen :: Vec n a -> Int
vlen VNil = 0
vlen (VCons _ xs) = 1 + vlen xs
vhead :: Vec ('S n) a -> a
vhead (VCons x _) = x
rep :: SNat n -> a -> Vec n a
rep SZ _ = VNil
rep (SS n) x = VCons x (rep n x)
vec :: Vec ('S ('S ('S 'Z))) Int
vec = rep (SS (SS (SS SZ))) 5
main :: IO ()
main = do
  print (vhead vec)
  print (vlen vec)

Key points

Mirror: a singleton type has exactly one value for each type it mirrors.
SNat: a singleton for naturals, with SZ for zero and SS for a successor.
Runtime bridge: passing a singleton gives a runtime function the type-level number.
Use a singleton to build a value whose length is fixed by its type.
Pattern matching: matching on a singleton reveals the mirrored type in each branch.

In this example, the three-successor singleton is the runtime witness for a length of three. rep uses that singleton to build a vector of three copies of 5. vhead reads the first copy and vlen counts all three copies. main prints the head first and the length second.

Note

a singleton carries no extra data beyond the mirrored choice itself.

Try it Yourself

Edit the code, then press Run.

Running is simulated · Haskell Playground

{-# 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
data SNat (n :: Nat) where
  SZ :: SNat 'Z
  SS :: SNat n -> SNat ('S n)
vlen :: Vec n a -> Int
vlen VNil = 0
vlen (VCons _ xs) = 1 + vlen xs
vhead :: Vec ('S n) a -> a
vhead (VCons x _) = x
rep :: SNat n -> a -> Vec n a
rep SZ _ = VNil
rep (SS n) x = VCons x (rep n x)
vec :: Vec ('S ('S ('S 'Z))) Int
vec = rep (SS (SS (SS SZ))) 5
main :: IO ()
main = do
  print (vhead vec)
  print (vlen vec)

Exercise

What does SS SZ mirror?

Zero Two One An unknown length