Haskell Design Patterns

Type promotion

Type promotion was introduced in the same paper as kind polymorphism (Giving Haskell a Promotion, by Yorgey et al in 2012). This represented a major leap forward for Haskell's type-level programming capabilities.

Let's explore type promotion in the context of a type-level programming example. We want to create a list where the type itself contains information about the list size.

To represent numbers at type level, we use the age-old Peano numbering which describes the natural numbers (1,2,3, ...) in a recursive manner:

  data Zero = Zero
    deriving Show
  data Succ n = Succ n
    deriving Show

  one = Succ Zero
  two = Succ one

We'll use this with the understanding that certain bad expressions are still allowed:

 badSucc1 = Succ 10 -- :: Succ Int ...