🎓 A1Learner
🔍
0 of 47 lessons completed

Haskell Promoted Types

A promoted type is a data constructor used as a type. It carries a fixed choice, such as True or Small, into the type of a value.

True and False become types

Flag is marked by a promoted Bool. A True flag holds the word ready.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
data Flag (b :: Bool) = Flag String
flagName :: Flag b -> String
flagName (Flag name) = name
flagTrue :: Flag 'True
flagTrue = Flag "ready"
main :: IO ()
main = putStrLn (flagName flagTrue)

A custom constructor becomes a type

Size is a custom data type with two constructors. A Small parcel and a Large parcel hold different weights.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
data Size = Small | Large
data Parcel (s :: Size) = Parcel Int
parcelWeight :: Parcel s -> Int
parcelWeight (Parcel weight) = weight
smallParcel :: Parcel 'Small
smallParcel = Parcel 3
largeParcel :: Parcel 'Large
largeParcel = Parcel 40
main :: IO ()
main = do
  print (parcelWeight smallParcel)
  print (parcelWeight largeParcel)

Both promoted Bool types can be used

A True flag and a False flag are different types. Both hold a plain string that can be printed.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
data Flag (b :: Bool) = Flag String
flagName :: Flag b -> String
flagName (Flag name) = name
flagTrue :: Flag 'True
flagTrue = Flag "ready"
flagFalse :: Flag 'False
flagFalse = Flag "waiting"
main :: IO ()
main = putStrLn (flagName flagTrue ++ " " ++ flagName flagFalse)

Example

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
data Level = Guest | Admin
data Account (l :: Level) = Account String Int
accountName :: Account l -> String
accountName (Account name _) = name
accountBalance :: Account l -> Int
accountBalance (Account _ balance) = balance
adminAccount :: Account 'Admin
adminAccount = Account "Ada" 500
main :: IO ()
main = do
  putStrLn (accountName adminAccount)
  print (accountBalance adminAccount)

Key points

  • Tick: a tick before a constructor shows it is used as a type.
  • Built-in promotion: ordinary constructors such as True and False also promote to types.
  • Custom promotion: constructors of a custom data type promote in the same way.
  • Fixed choice: a promoted type fixes one choice for every value of that type.
  • Use a promoted type to mark a value with a choice the type checker can see.

In this example, Level is a custom data type with Guest and Admin constructors. Account is marked by a promoted Level, and adminAccount carries the Admin mark. accountName and accountBalance read the two fields of any account. main prints the admin name first and the admin balance second.

Note

a promoted constructor is not a value, so it cannot be printed or passed at runtime.

Try it Yourself

Edit the code, then press Run.

Running is simulated · Haskell Playground

Exercise

Which spelling uses Small as a type?