GADTs

I have an approximate knowledge of many things

Gytis Žilinskas - Adform             gytis.zilinskas@gmail.com

Prelude

Prelude #2

{-# LANGUAGE GADTs
           , EmptyDataDecls
           , TypeOperators #-}

ADTs

G

algebraic data types

Generalized

Algebraic data types

Haskell's algebraic data types are named such since they correspond to an initial algebra in category theory, giving us some laws, some operations and some symbols to manipulate.

-- Don Stewart

Symbols

Operations

Laws

Things

Ways to make new things

Rules the things follow

Algebra

Symbols

Operations

Laws

0, 1, 2, x, y, z, ...

+, -,*, /, ...

0 + x = x, 1 * x = x

Algebra

Symbols

Operations

Laws

Types((), Int, Bool, . . .)

Type constructors (Maybe, Either)

???

Algebra

One

Addition

Multiplication

Foundation

data Unit = Unit
data a :+ b = AddL a | AddR b
data Either a b = Left a | Right b
data a :* b = Mul a b
data (a, b) = (a, b)

Zero

data Void

Two

Derivations

type Two = Unit :+ Unit
data Bool = False | True

0 + x = x

Laws

Either Void x ≅ x

0 * x = x

(Void, x) ≅ Void

1 * x = x

((), x) ≅ x

x + y = y + x

Either x y ≅ Either y x

x * y = y * x

(x, y) ≅ (y, x)

Functions

data a -> b = ???

Domain

Range

True

False

True

False

2 ^ 2

Functions

data a -> b = ???

Domain

Range

A

B

True

False

2 ^ 3

C

Functions

a -> b 
<=>
b ^ a

Laws (once again)

1 ^ a = 1

a -> () ≅ ()

a ^ 1 = a

() -> a ≅ a

(b * c)^a = b^a * c^a

a -> (b, c) ≅ (a -> b, a -> c)

c ^ (ba) = (c^b) ^ a

(a, b) -> c ≅ a -> b -> c

Lists

data List x = Nil | Cons x (List x)
L = 1 + x L
L = 1 + x (1 + x L)
L = 1 + x + x^2 (1 + x L)
L = 1 + x + x^2 + x^3 + x^4 + ...

Trees

data Tree x = Tip | Node (Tree x) x (Tree x)
T = 1 + x T^2
x T^2 - T + 1 = 0
T = (1 - sqrt(1 - 4x)) / 2x
T = 1 + x + 2x^2 + 5x^3 + 14x^4 + ...

Back to GADTs

data Expr = I Int

Language of arithmetic expressions

          | Add Expr Expr
          | Mul Expr Expr
(5 + 1) * 7
(I 5 `Add` I 1) `Mul` I 7 :: Expr

Back to GADTs

eval :: Expr -> Int

Evaluating our expressions

eval (I n) = n
eval (Add e1 e2) = eval e1 + eval e2
(5 + 1) * 7
> let a = (I 5 `Add` I 1) `Mul` I 7
eval (Mul e1 e2) = eval e1 * eval e2
> :t a
a :: Expr
> eval a
42

Extend it with Booleans!

Example
(I 5 `Add` I 1) `Eq` I 42 :: Expr
eval :: Expr ->
eval (I n) = Left n
data Expr = I Int
          | Add Expr Expr
          | Mul Expr Expr
          | B Bool
          | Eq Expr Expr
Either Int Bool
eval (B b) = Right b
eval (Add e1 e2) = eval e1 + eval e2

Extend it with Booleans!

> let a = I 7 `Add` Bool True
> :t a
a :: Expr

Problem

eval :: Expr ->
eval (I n) = Just $ Left n
Maybe (Either Int Bool)
eval (B b) = Just $ Right b
eval (Add e1 e2) = ...

Solution

?

UNACCEPTABLE!

Phantom types

data Expr a = I Int
            | Add (Expr a) (Expr a)
            | Mul (Expr a) (Expr a)
            | B Bool
            | Eq (Expr a) (Expr a)

a - phantom

There is no value of type a "inside" Expr a

Smart constructors

Add :: Expr a -> Expr a -> Expr a
add :: Expr Int -> Expr Int -> Expr Int
add = Add
i :: Int -> Expr Int
b :: Bool -> Expr Bool
I 7 `Add` B True
i 7 `add` b True

becomes

> let a = i 7 `add` b True

<interactive>:15:19:
    Couldn't match type ‘Bool’ with ‘Int’
    Expected type: Expr Int
      Actual type: Expr Bool
    In the second argument of ‘add’, namely ‘b True’
    In the expression: i 7 `add` b True

Back to evaluating

eval :: Expr a -> a
eval (I n) = n
(I n) :: Expr a

and `a` can be anything

GADTs!

Syntax

Maybe

List

data Maybe a = Nothing
             | Just a 
data List a = Nil
            | Cons a (List a) 

GADTs!

Syntax

Maybe

List

> :t Nothing
Nothing :: Maybe a
> :t Just
Just :: a -> Maybe a 
> :t Nil
Nil :: List a
> :t Cons
Cons :: a -> List a -> List a 

GADTs!

Syntax

Maybe

List

data Maybe a where
   Nothing :: Maybe a
   Just :: a -> Maybe a
data List a where
   Nil  :: List a
   Cons :: a -> List a -> List a

GADTs!

Example: SafeLists

data Empty
data NonEmpty

data SafeList a b where
 -- to be implemented
safeHead :: SafeList a NonEmpty -> a
data SafeList a b where
  Nil  :: SafeList a Empty
  Cons :: a -> SafeList a b -> SafeList a NonEmpty
safeHead :: SafeList a NonEmpty -> a
safeHead (Cons x _) = x

GADTs!

Example: SafeLists

> safeHead (Cons "hi" Nil)
"hi"
> safeHead Nil

<interactive>:1:9:
    Couldn't match `NonEmpty' against `Empty'
      Expected type: SafeList a NonEmpty
      Inferred type: SafeList a Empty
    In the first argument of `safeHead', namely `Nil'
    In the definition of `it': it = safeHead Nil

GADTs!

data Expr a where
    I :: Int -> Expr Int
    B :: Bool -> Expr Bool
    Add :: Expr Int -> Expr Int -> Expr Int
    Mul :: Expr Int -> Expr Int -> Expr Int
    Eq :: Expr Int -> Expr Int -> Expr Bool
eval :: Expr a -> a
eval (I n) = n
eval (B b) = b
eval (Add e1 e2) = eval e1 + eval e2
eval (Mul e1 e2) = eval e1 * eval e2
eval (Eq eq1 e2) = eval e1 == eval e2

GADTs!

> let a = (I 5 `Add` I 1) `Eq` I 42
> :t a
a :: Expr Bool
> eval a
False 
> let b = I 7 `Add` B True

<interactive>:6:19:
    Couldn't match type ‘Bool’ with ‘Int’
    Expected type: Expr Int
      Actual type: Expr Bool
    In the second argument of ‘Add’, namely ‘B True’
    In the expression: I 7 `Add` B True

Questions?