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 ...

Get Haskell Design Patterns now with the O’Reilly learning platform.

O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.