I have an approximate knowledge of many things

Gytis Å½ilinskas - Adform Â  Â  Â  Â  Â  Â Â gytis.zilinskas@gmail.com

## Prelude #2

{-# LANGUAGE GADTs
, TypeOperators #-}


# 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

### Laws

Things

Ways to make new things

Rules the things follow

## Algebra

### Laws

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

+, -,*, /, ...

0 + x = x, 1 * x = x

## Algebra

### Laws

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

Type constructors (Maybe, Either)

???

Oneâ€‹

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

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

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

Syntax

Maybe

List

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

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 

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

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

Example: SafeLists

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

<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

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

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