🎓 A1Learner
🔍
0 of 47 lessons completed

Haskell DataKinds Idea

DataKinds is a GHC extension that promotes an ordinary data type into a kind. Its constructors then become types that can mark other types.

A data type becomes a kind

Switch is an ordinary data type with two values. With DataKinds it also becomes a kind for marking lamps.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
data Switch = On | Off
data Lamp (s :: Switch) = Lamp String
lampName :: Lamp s -> String
lampName (Lamp name) = name
lampOn :: Lamp 'On
lampOn = Lamp "desk"
main :: IO ()
main = putStrLn (lampName lampOn)

Two marks give two different types

One box can carry the Red mark and another the Green mark. Both hold a plain string, but their types differ.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
data Colour = Red | Green
data Box (c :: Colour) = Box String
boxName :: Box c -> String
boxName (Box name) = name
boxRed :: Box 'Red
boxRed = Box "rose"
boxGreen :: Box 'Green
boxGreen = Box "leaf"
main :: IO ()
main = putStrLn (boxName boxRed ++ " " ++ boxName boxGreen)

A function can demand one mark

onlyRed accepts only a Red box. Passing it a Red box prints its content.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
data Colour = Red | Green
data Box (c :: Colour) = Box String
boxName :: Box c -> String
boxName (Box name) = name
onlyRed :: Box 'Red -> String
onlyRed box = boxName box
boxRed :: Box 'Red
boxRed = Box "rose"
main :: IO ()
main = putStrLn (onlyRed boxRed)

Example

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
data Signal = Stop | Go
data Sign (s :: Signal) = Sign String
signText :: Sign s -> String
signText (Sign message) = message
stopSign :: Sign 'Stop
stopSign = Sign "halt"
goSign :: Sign 'Go
goSign = Sign "move"
main :: IO ()
main = do
  putStrLn (signText stopSign)
  putStrLn (signText goSign)

Key points

  • Promotion: a data type lifted by DataKinds gains a second life at the type level.
  • Kind: a kind is the type of a type, and a promoted type becomes a new kind.
  • Tick: a tick before a constructor marks it as a promoted type, not a value.
  • Marking: a promoted type can mark a type argument, so the mark travels with the type.
  • Restriction: a function can demand one promoted mark, and the type checker rejects the other marks.

In this example, Signal is an ordinary data type with two constructors. Sign is marked by a promoted Signal, so stopSign carries the Stop mark and goSign carries the Go mark. signText reads the message stored in any sign. main prints the stop message first and the go message second.

Note

DataKinds needs its pragma at the top of the file, and kind annotations need KindSignatures.

Try it Yourself

Edit the code, then press Run.

Running is simulated · Haskell Playground

Exercise

What does DataKinds promote a data type into?