Notes for ‘Thinking with Types: Type-level Programming in Haskell’, Chapters 1–5

Haskell—with its powerful type system—has a great support for type-level programming and it has gotten much better in the recent times with the new releases of the GHC compiler. But type-level programming remains a daunting topic even with seasoned haskellers. Thinking with Types: Type-level Programming in Haskell by Sandy Maguire is a book which attempts to fix that. I’ve taken some notes to summarize my understanding of the same.

Introduction

  • Type-level Programming (TLP) is writing programs that run at compile-time, unlike term-level programming which is writing programs that run at run-time.
  • TLP should be used in moderation.
  • TLP should be mostly used
    • for programs that are catastrophic to get wrong (finance, healthcare, etc).
    • when it simplifies the program API massively.
    • when power-to-weight ratio of adding TLP is high.
  • Types are not a silver bullet for fixing all errors:
    • Correct programs can be not well-typed.
    • It can be hard to assign type for useful programs. e.g. printf from C.
  • Types can turn possible runtime errors into compile-time errors.

Chapter 1. The Algebra Behind Types

Isomorphisms and Cardinalities

  • Cardinality of a type is the number of values it can have ignoring bottoms. The values of a type are also called the inhabitants of the type.
data Void
 -- no possible values. cardinality: 0
data Unit = Unit
 -- only one possible value. cardinality: 1
data Bool = True | False
 -- only two possible values. cardinality: 2
  • Cardinality is written using notation: |Void| = 0
  • Two types are said to be Isomorphic if they have same cardinality.
  • An isomorphism between types a and b is a pair of functions to and from such that:
to :: a -> b
from :: b -> a
to . from = id
from . to = id

Sum, Product and Exponential Types

  • Either a b is a Sum type. Its number of inhabitants is sum of the number of inhabitants of type a and b like so: |a| possible values with the Left constructor and |b| possible values with the Right constructor. Formally:
|Either a b| = |a| + |b|
  • (a, b) is a Product type. Its number of inhabitant is the product of the number of inhabitants of types a and b. Formally:
|(a, b)| = |a| * |b|
  • Some more examples:
|Maybe a| = |Nothing| + |Just a| = 1 + |a|
|[a]| = 1 + |a| + |a|^2 + |a|^3 + ...
|Either a Void| = |a| + 0 = |a|
|Either Void a| = 0 + |a| = |a|
|(a, Unit)| = |a| * 1 = |a|
|(Unit, a)| = 1 * |a| = |a|
  • Function types are exponentiation types.
|a -> b| = |b|^|a|

For every value in domain a there can be |b| possible values in the range b. And there are |a| possible values in domain a. So:

|a -> b|
  = |b| * |b| * ... * |b| -- (|a| times)
  = |b|^|a|
  • Data can be represented in many possible isomorphic types. Some of them are more useful than others. Example:
data TicTacToe1 a = TicTacToe1
  { topLeft      :: a
  , topCenter    :: a
  , topRight     :: a
  , middleLeft   :: a
  , middleCenter :: a
  , middleRight  :: a
  , bottomLeft   :: a
  , bottomCenter :: a
  , bottomRight  :: a
  }

|TicTacToe1 a|
  = |a| * |a| * ... * |a| -- 9 times
  = |a|^9

emptyBoard1 :: TicTacToe1 (Maybe Bool)
emptyBoard1 =
  TicTacToe1 Nothing Nothing Nothing
             Nothing Nothing Nothing
             Nothing Nothing Nothing

-- Alternatively

data Three = One | Two | Three
data TicTacToe2 a =
  TicTacToe2 (Three -> Three -> a)

|TicTacToe2 a| = |a|^(|Three| * |Three|)
               = |a|^(3*3)
               = |a|^9

emptyBoard2 :: TicTacToe2 (Maybe Bool)
emptyBoard2 =
  TicTacToe2 $ const $ const Nothing

The Curry-Howard Isomorphism

  • Every logic statement can be expressed as an equivalent computer program.
  • Helps us analyze mathematical theorems through programming.

Canonical Representations

  • Since multiple equivalent representations of a type are possible, the representation in form of sum of products is considered the canonical representation of the type. Example:
Either a (Either b (c, d)) -- canonical

(a, Bool) -- not canonical
Either a a
-- same cardinality as above but canonical

Chapter 2. Terms, Types and Kinds

The Kind System

  • Terms are things manipulated at runtime. Types of terms are used by compiler to prove “things” about the terms.
  • Similarly, Types are things manipulated at compile-time. Kinds of types are used by the compiler to prove “things” about the types.
  • Kinds are “the types of the Types”.
  • Kind of things that can exist at runtime (terms) is *. That is, kind of Int, String etc is *.
> :type True
True :: Bool
> :kind Bool
Bool :: *
  • There are kinds other than *. For example:
> :kind Show Int
Show Int :: Constraint
  • Higher-kinded types have (->) in their kind signature:
> :kind Maybe
Maybe :: * -> *
> :kind Maybe Int
Maybe Int :: *

> :type Control.Monad.Trans.Maybe.MaybeT
Control.Monad.Trans.Maybe.MaybeT
  :: m (Maybe a) -> Control.Monad.Trans.Maybe.MaybeT m a
> :kind Control.Monad.Trans.Maybe.MaybeT
Control.Monad.Trans.Maybe.MaybeT :: (* -> *) -> * -> *
> :kind Control.Monad.Trans.Maybe.MaybeT IO Int
Control.Monad.Trans.Maybe.MaybeT IO Int :: *

Data Kinds

  • DataKinds extension lets us create new kinds.
  • It lifts data constructors into type constructors and types into kinds.
> :set -XDataKinds
> data Allow = Yes | No
> :type Yes -- Yes is data constructor
Yes :: Allow
> :kind Allow -- Allow is a type
Allow :: *
> :kind 'Yes -- 'Yes is a type too. Its kind is 'Allow.
'Yes :: Allow
  • Lifted constructors and types are written with a preceding ' (called tick).

Promotion of Built-In Types

  • DataKinds extension promotes built-in types too.
  • Strings are promoted to the kind Symbol.
  • Natural numbers are promoted to the kind Nat.
> :kind "hi" -- "hi" is a type-level string
"hi" :: GHC.Types.Symbol
> :kind 123 -- 123 is a type-level natural number
123 :: GHC.Types.Nat
  • We can do type level operations on Symbols and Nats.
> :m +GHC.TypeLits
> :kind AppendSymbol
AppendSymbol :: Symbol -> Symbol -> Symbol
> :kind! AppendSymbol "hello " "there"
AppendSymbol "hello " "there" :: Symbol
= "hello there"
> :set -XTypeOperators
> :kind! (1 + 2) ^ 7
(1 + 2) ^ 7 :: Nat
= 2187
  • TypeOperators extension is needed for applying type-level functions with symbolic identifiers.
  • There are type-level lists and tuples:
> :kind '[ 'True ]
'[ 'True ] :: [Bool]
> :kind '[1,2,3]
'[1,2,3] :: [Nat]
> :kind '["abc"]
'["abc"] :: [Symbol]
> :kind 'False ': 'True ': '[]
'False ': 'True ': '[] :: [Bool]
> :kind '(6, "x", 'False)
'(6, "x", 'False) :: (Nat, Symbol, Bool)

Type-level Functions

  • With the TypeFamilies extension, it’s possible to write new type-level functions as closed type families:
> :set -XDataKinds
> :set -XTypeFamilies
> :{
> type family And (x :: Bool) (y :: Bool) :: Bool where
>   And 'True 'True = 'True
>   And _     _     = 'False
> :}
> :kind And
And :: Bool -> Bool -> Bool
> :kind! And 'True 'False
And 'True 'False :: Bool
= 'False
> :kind! And 'True 'True
And 'True 'True :: Bool
= 'True
> :kind! And 'False 'True
And 'False 'True :: Bool
= 'False

Chapter 3. Variance

  • There are three types of Variance (T here a type of kind * -> *):
    • Covariant: any function of type a -> b can be lifted into a function of type T a -> T b. Covariant types are instances of the Functor typeclass:
    class Functor f where
  fmap :: (a -> b) -> f a -> f b
    • Contravariant: any function of type a -> b can be lifted into a function of type T b -> T a. Contravariant functions are instances of the Contravariant typeclass:
    class Contravariant f where
  contramap :: (a -> b) -> f b -> f a
    • Invariant: no function of type a -> b can be lifted into a function of type T a. Invariant functions are instances of the Invariant typeclass:
    class Invariant f where
  invmap :: (a -> b) -> (b -> a) -> f a -> f b
  • Variance of a type T is specified with respect to a particular type parameter. A type T with two parameters a and b could be covariant wrt. a and contravariant wrt. b.
  • Variance of a type T wrt. a particular type parameter is determined by whether the parameter appears in positive or negative positions.
    • If a type parameter appears on the left-hand side of a function, it is said to be in a negative position. Else it is said to be in a positive position.
    • If a type parameter appears only in positive positions then the type is covariant wrt. that parameter.
    • If a type parameter appears only in negative positions then the type is contravariant wrt. that parameter.
    • If a type parameter appears in both positive and negative positions then the type is invariant wrt. that parameter.
    • positions follow the laws of multiplication for their signs.
a b a * b
+ + +
+ - -
- + -
- - +
  • Examples:
newtype T1 a = T1 (Int -> a)
-- a is in +ve position, T1 is covariant wrt. a.
newtype T2 a = T2 (a -> Int)
-- a is in -ve position, T2 is contravariant wrt. a.
newtype T3 a = T3 (a -> a)
-- a is in both -ve and +ve position. T3 is invariant wrt. a.
newtype T4 a = T4 ((Int -> a) -> Int)
-- a is in +ve position but (Int -> a) is in -ve position.
-- So a is in -ve position overall. T4 is contravariant wrt. a.
newtype T5 a = T5 ((a -> Int) -> Int)
-- a is in -ve position but (a -> Int) is in -ve position.
-- So a is in +ve position overall. T5 is covariant wrt. a.
  • Covariant parameters are said to be produced or owned by the type.
  • Contravariant parameters are said to be consumed by the type.
  • A type that has two parameters and is covariant in both of them is an instance of BiFunctor.
  • A type that has two parameters and is contravariant in first parameter and covariant in second parameter is an instance of Profunctor.

Chapter 4. Working with Types

  • Standard Haskell has no notion of scopes for types.
  • ScopedTypeVariables extension lets us bind type variables to a scope. It requires an explicitly forall quantifier in type signatures.
> -- This does not compile.
> :{
> comp :: (a -> b) -> (b -> c) -> a -> c
> comp f g a = go f
>  where
>   go :: (a -> b) -> c
>   go f' = g (f' a)
> :}

<interactive>:11:11: error:
    • Couldn't match expected type ‘c1’ with actual type ‘c’
      ‘c1’ is a rigid type variable bound by
        the type signature for:
          go :: forall a1 b1 c1. (a1 -> b1) -> c1
        at <interactive>:10:3-21
      ‘c’ is a rigid type variable bound by
        the type signature for:
          comp :: forall a b c. (a -> b) -> (b -> c) -> a -> c
        at <interactive>:7:1-38
    • In the expression: g (f' a)

<interactive>:11:14: error:
    • Couldn't match expected type ‘b’ with actual type ‘b1’
      ‘b1’ is a rigid type variable bound by
        the type signature for:
          go :: forall a1 b1 c1. (a1 -> b1) -> c1
        at <interactive>:10:3-21
      ‘b’ is a rigid type variable bound by
        the type signature for:
          comp :: forall a b c. (a -> b) -> (b -> c) -> a -> c
        at <interactive>:7:1-38
    • In the first argument of ‘g’, namely ‘(f' a)’

<interactive>:11:17: error:
    • Couldn't match expected type ‘a1’ with actual type ‘a’
      ‘a1’ is a rigid type variable bound by
        the type signature for:
          go :: forall a1 b1 c1. (a1 -> b1) -> c1
        at <interactive>:10:3-21
      ‘a’ is a rigid type variable bound by
        the type signature for:
          comp :: forall a b c. (a -> b) -> (b -> c) -> a -> c
        at <interactive>:7:1-38
    • In the first argument of ‘f'’, namely ‘a’

> -- But this does.
> :set -XScopedTypeVariables
> :{
> comp :: forall a b c. (a -> b) -> (b -> c) -> a -> c
> comp f g a = go f
>  where
>   go :: (a -> b) -> c
>   go f' = g (f' a)
> :}
> :set -XTypeApplications
> :type traverse
traverse
  :: (Traversable t, Applicative f) =>
     (a -> f b) -> t a -> f (t b)
> :type traverse @Maybe
traverse @Maybe
  :: Applicative f =>
     (a -> f b) -> Maybe a -> f (Maybe b)
> :type traverse @Maybe @[]
traverse @Maybe @[]
  :: (a -> [b]) -> Maybe a -> [Maybe b]
> :type traverse @Maybe @[] @Int
traverse @Maybe @[] @Int
  :: (Int -> [b]) -> Maybe Int -> [Maybe b]
> :type traverse @Maybe @[] @Int @String
traverse @Maybe @[] @Int @String
  :: (Int -> [String]) -> Maybe Int -> [Maybe String]
  • Types are applied in the order they appear in the type signature. It is possible to avoid applying types by using a type with an underscore: @_
> :type traverse @Maybe @_ @_ @String
traverse @Maybe @_ @_ @String
  :: Applicative w1 =>
     (w2 -> w1 String) -> Maybe w2 -> w1 (Maybe String)
  • Sometimes the compiler cannot infer the type of an expression. AllowAmbiguousTypes extension allow such programs to compile.
> :set -XScopedTypeVariables
> :{
> f :: forall a. Show a => Bool
> f = True
> :}

<interactive>:7:6: error:
    • Could not deduce (Show a0)
      from the context: Show a
        bound by the type signature for:
                   f :: forall a. Show a => Bool
        at <interactive>:7:6-29
      The type variable ‘a0’ is ambiguous
    • In the ambiguity check for ‘f’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature: f :: forall a. Show a => Bool
  • Proxy is a type isomorphic to () except with a phantom type parameter:
data Proxy a = Proxy
  • With all the three extensions enabled, it is possible to get a term-level representation of types using the Data.Typeable module:
> :set -XScopedTypeVariables
> :set -XTypeApplications
> :set -XAllowAmbiguousTypes
> :m +Data.Typeable
> :{
> typeName :: forall a. Typeable a => String
> typeName = show . typeRep $ Proxy @a
> :}
> typeName @String
"[Char]"
> typeName @(IO Int)
"IO Int"

Chapter 5. Constraints and GADTs

Constraints

  • Constraints are a kind different than the types (*).
  • Constraints are what appear on the left-hand side on the fat context arrow =>, like Show a.
> :k Show
Show :: * -> Constraint
> :k Show Int
Show Int :: Constraint
> :k (Show Int, Eq String)
(Show Int, Eq String) :: Constraint
  • Type equalities (Int ~ a) are another way of creating Constraints. (Int ~ a) says a is same as Int.
  • Type equalities are
    • reflexive: a ~ a always
    • symmetrical: a ~ b implies b ~ a
    • transitive: a ~ b and b ~ c implies a ~ c

GADTs

  • GADTs are Generalized Algebraic DataTypes. They allow writing explicit type signatures for data constructors. Here is the code for a length-typed list using GADTs:
> :set -XGADTs
> :set -XKindSignatures
> :set -XTypeOperators
> :set -XDataKinds
> :m +GHC.TypeLits
> :{
> data List (a :: *) (n :: Nat) where
>   Nil  :: List a 0
>   (:~) :: a -> List a n -> List a (n + 1)
> infixr 5 :~
> :}
> :type Nil
Nil :: List a 0
> :type 'a' :~ Nil
'a' :~ Nil :: List Char 1
> :type 'b' :~ 'a' :~ Nil
'b' :~ 'a' :~ Nil :: List Char 2
> :type True :~ 'a' :~ Nil

<interactive>:1:9: error:
    • Couldn't match type ‘Char’ with ‘Bool’
      Expected type: List Bool 1
        Actual type: List Char (0 + 1)
    • In the second argument of ‘(:~)’, namely ‘'a' :~ Nil’
      In the expression: True :~ 'a' :~ Nil
  • GADTs are just syntactic sugar for ADTs with type equalities. The above definition is equivalent to:
> :set -XGADTs
> :set -XKindSignatures
> :set -XTypeOperators
> :set -XDataKinds
> :m +GHC.TypeLits
> :{
> data List (a :: *) (n :: Nat)
>   = (n ~ 0) => Nil
>   | a :~ List a (n - 1)
> infixr 5 :~
> :}
> :type 'a' :~ Nil
'a' :~ Nil :: List Char 1
> :type 'b' :~ 'a' :~ Nil
'b' :~ 'a' :~ Nil :: List Char 2
  • Type-safety of this list can be used to write a safe head function which does not compile for an empty list:
> :{
> safeHead :: List a (n + 1) -> a
> safeHead (x :~ _) = x
> :}
> safeHead ('a' :~ 'b' :~ Nil)
'a'
> safeHead Nil

<interactive>:21:10: error:
    • Couldn't match type ‘1’ with ‘0’
      Expected type: List a (0 + 1)
        Actual type: List a 0
    • In the first argument of ‘safeHead’, namely ‘Nil’
      In the expression: safeHead Nil
      In an equation for ‘it’: it = safeHead Nil

Heterogeneous Lists

We can use GADTs to build heterogeneous lists which can store values of different types and are type-safe to use.

First, the required extensions and imports:

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}

module HList where

import Data.Typeable

HList is defined as a GADT:

data HList (ts :: [*]) where
  HNil :: HList '[]
  (:#) :: t -> HList ts -> HList (t ': ts)
infixr 5 :#

Example usage:

> :type HNil
HNil :: HList '[]
> :type 'a' :# HNil
'a' :# HNil :: HList '[Char]
> :type True :# 'a' :# HNil
True :# 'a' :# HNil :: HList '[Bool, Char]

We can write operations on HList:

hLength :: HList ts -> Int
hLength HNil = 0
hLength (x :# xs) = 1 + hLength xs

hHead :: HList (t ': ts) -> t
hHead (t :# _) = t

Example usage:

> hLength $ True :# 'a' :# HNil
2
> hHead $ True :# 'a' :# HNil
True
> hHead HNil

<interactive>:7:7: error:
    • Couldn't match type ‘'[]’ with ‘t : ts0’
      Expected type: HList (t : ts0)
        Actual type: HList '[]
    • In the first argument of ‘hHead’, namely ‘HNil’
      In the expression: hHead HNil
      In an equation for ‘it’: it = hHead HNil
    • Relevant bindings include it :: t (bound at <interactive>:7:1)

We need to define instances of typeclasses like Eq, Ord etc. for HList because GHC cannot derive them automatically yet:

instance Eq (HList '[]) where
  HNil == HNil = True
instance (Eq t, Eq (HList ts))
    => Eq (HList (t ': ts)) where
  (x :# xs) == (y :# ys) =
    x == y && xs == ys

instance Ord (HList '[]) where
  HNil `compare` HNil = EQ
instance (Ord t, Ord (HList ts))
    => Ord (HList (t ': ts)) where
  (x :# xs) `compare` (y :# ys) =
    x `compare` y <> xs `compare` ys

instance Show (HList '[]) where
  show HNil = "[]"
instance (Typeable t, Show t, Show (HList ts))
    => Show (HList (t ': ts)) where
  show (x :# xs) =
    show x 
    ++ "@" ++ show (typeRep (Proxy @t))
    ++ " :# " ++ show xs

The instances are defined recursively: one for the base case and one for the inductive case.

Example usage:

> True :# 'a' :# HNil == True :# 'a' :# HNil
True
> True :# 'a' :# HNil == True :# 'b' :# HNil
False
> True :# 'a' :# HNil == True :# HNil

<interactive>:17:24: error:
    • Couldn't match type ‘'[]’ with ‘'[Char]’
      Expected type: HList '[Bool, Char]
        Actual type: HList '[Bool]
    • In the second argument of ‘(==)’, namely ‘True :# HNil’
      In the expression: True :# 'a' :# HNil == True :# HNil
      In an equation for ‘it’: it = True :# 'a' :# HNil == True :# HNil
> show $ True :# 'a' :# HNil
"True@Bool :# 'a'@Char :# []"

Creating New Constraints

  • Type families can be used to create new Constraints:
> :set -XKindSignatures
> :set -XDataKinds
> :set -XTypeOperators
> :set -XTypeFamilies
> :m +Data.Constraint
> :{
> type family AllEq (ts :: [*]) :: Constraint where
>   AllEq '[] = ()
>   AllEq (t ': ts) = (Eq t, AllEq ts)
> :}
> :kind! AllEq '[Bool, Char]
AllEq '[Bool, Char] :: Constraint
= (Eq Bool, (Eq Char, () :: Constraint))
  • AllEq is a type-level function from a list of types to a constraint.
  • With the ConstraintKinds extension, AllEq can be made polymorphic over all constraints instead of just Eq:
> :set -XConstraintKinds
> :{
> type family All (c :: * -> Constraint)
>                 (ts :: [*]) :: Constraint where
>   All c '[] = ()
>   All c (t ': ts) = (c t, All c ts)
> :}
  • With All, instances for HList can be written non-recursively:
instance All Eq ts => Eq (HList ts) where
  HNil == HNil = True
  (a :# as) == (b :# bs) = a == b && as == bs

Conclusion

I’m still in the process of reading the book and I’ll post the notes for the rest of the chapters in a later post. The complete code for HList can be found here.

Like, repost, or comment

Send a Webmention for this post

Posted by

Like this post? Subscribe to get future posts by email.

Got suggestions, corrections, or thoughts? Post a comment!

Cancel Reply
Markdown is allowed
Email is used just to show an avatar image and is not displayed.
Comments are moderated. They will appear below after they are approved.

7 comments

Thanks a lot for sharing it <3

Thanks, I just started reading this book.

Here’s a video playlist from Barry going through the whole book:

https://www.youtube.com/playlist?list=PLW_sOzxD_4gQok1m4uH05zI993SV-uXsI

nice write up. i’m always on the lookout for some way to bridge the gap between beginner/intermediate Haskell (things in Haskell that I understand) and advanced Haskell (things in Haskell that I don’t understand). I’ve been on the fence with this book for a while, but it seems like it might be a worthwhile purchase

Thanks. The book is definitely useful to understand more sophisticated type-level stuff in Haskell but IMO that’s just one of many things about advanced Haskell.

Thank you for sharing the nice notes

Florian

amazing, thanks!

I think that using multiline ({:) makes it mush less readable. Any reason for doing this?

Abhinav Sarkar

Thanks Florian. I copied the code directly from GHCi, hence the multiline.

29 Mentions

9 Reposts abhin4vankur sethi is alive and wellStephen DiehlnilensoArun RaghavanƛSanchayan Maityjenix21N (\dev\ice)