DataKinds and Type-Level Programming

Libraries: singletons (generate singletons with TH), servant (APIs as types, Module 49), vinyl (extensible records), generics-sop, first-class-families (type-level combinators).

Type-level programming is powerful but adds complexity. Use it where it removes real classes of bugs.

{-# LANGUAGE DataKinds, KindSignatures, GADTs, TypeApplications, ScopedTypeVariables, AllowAmbiguousTypes #-}
import GHC.TypeLits
import Data.Proxy

-- Promoted data: values become types, types become kinds
data DoorState = Opened | Closed | Locked

data Door (s :: DoorState) where
  MkDoor :: String -> Door s

openDoor :: Door 'Closed -> Door 'Opened
openDoor (MkDoor n) = MkDoor n

lockDoor :: Door 'Closed -> Door 'Locked
lockDoor (MkDoor n) = MkDoor n
-- lockDoor (openDoor ...)  -- compile error: can't lock an open door

-- Type-level strings and numbers
newtype Tagged (tag :: Symbol) a = Tagged a

describe :: forall tag a. (KnownSymbol tag, Show a) => Tagged tag a -> String
describe (Tagged x) = symbolVal (Proxy @tag) ++ ": " ++ show x
-- describe (Tagged 42 :: Tagged "answer" Int) == "answer: 42"

-- Units of measure style safety
newtype Quantity (unit :: Symbol) = Quantity Double deriving Show
addQ :: Quantity u -> Quantity u -> Quantity u
addQ (Quantity a) (Quantity b) = Quantity (a + b)
-- addQ (Quantity 1 :: Quantity "m") (Quantity 2 :: Quantity "s")   -- compile error

-- Singletons: connect runtime values with type-level values
data SDoorState (s :: DoorState) where
  SOp
…