data H = H -- hydrogen
data O = O -- oxygen
data C = C -- carbon
type H₂O = (H, O, H) -- water
type O₂ = (O, O) -- oxygen (gas)
type CO₂ = (O, C, O) -- carbon dioxide
makeWater :: H -> H -> O -> H₂O
makeOxygen :: O -> O -> O₂
burnOxygen :: C -> O₂ -> CO₂
makeWater :: H -> H -> O -> H₂O
makeWater h1 h2 o = (h1, o, h2)
~
makeOxygen :: O -> O -> O₂
makeOxygen o1 o2 = (o1, o2)
~
burnOxygen :: C -> O₂ -> CO₂
burnOxygen c (o1, o2) = (o1, c, o2)
.
$
λ> :type makeOxygen
makeOxygen :: O -> O -> O₂
λ> :type makeOxygen O
makeOxygen O :: O -> O₂
λ> :type makeOxygen O O
makeOxygen O O :: O₂
λ> :type burnOxygen
burnOxygen :: C -> O₂ -> CO₂
λ> :type burnOxygen C
burnOxygen C :: O₂ -> CO₂
λ> :type burnOxygen C (O, O)
burnOxygen C O₂ :: CO₂
f1 :: O -> O₂
f1 = makeOxygen O
f2 :: O₂ -> CO₂
f2 = burnOxygen C
f3 = f2 . f1
f3 :: O -> CO₂
f1 :: { O -> O₂ }
f2 :: [ O₂ -> CO₂ ]
f3 :: {O -> [ O₂ } -> CO₂ ]
f3 :: O -> CO₂
f3' o = f2 . f1 o
Diagnostics:
1. • Couldn't match type: (O, O)
with: a -> O₂
Expected: a -> O₂
Actual: O₂
• Possible cause: ‘f1’ is applied to too many arguments
In the second argument of ‘(.)’, namely ‘f1 o’
In the expression: f2 . f1 o
In an equation for ‘f3'’: f3' o = f2 . f1 o
• Relevant bindings include
f3' :: O -> a -> CO₂
(bound at Script.hs:112:1) [-Wdeferred-type-errors]
f3' o = f2 . f1 o
f3' o = f2 . f1 $ o
-- OR
f3' o = f2 $ f1 o
infixr 9 .
(.) :: (b -> c) -> (a -> b) -> (a -> c)
(f . g) x = f (g x)
infixr 0 $
($) :: (a -> b) -> a -> b
f $ x = f x
data H'
= H¹-- protium
| H²-- deuterium
| H³-- tritium
type H2O' = (H', O, H') -- water
makeWater' :: H' -> H' -> O -> H2O'
makeWater' h1 h2 o = (h1, o, h2)
How many values inhibit each of these?
Type | Possibilities |
---|---|
() | ? |
O | ? |
H' | ? |
(H', H') | ? |
()
()
1
()
O
O
1
O
H'
H'
3
H¹
H²
H³
(H', H')
(H', H')
9
(H¹, H¹)
(H¹, H²)
(H¹, H³)
(H², H¹)
(H², H²)
(H², H³)
(H³, H¹)
(H³, H²)
(H³, H³)
(H', Bool)
(H', Bool)
6
(H¹, True)
(H¹, False)
(H², True)
(H², False)
(H³, True)
(H³, False)
Type | Inhibitants |
---|---|
() | 1 |
Bool | 2 |
H' | 3 |
A | a |
B | b |
(A, B) | a × b |
A | B | a + b |
Product types Π
Type | Inhibitants |
---|---|
() | 1 |
Bool | 2 |
((), Bool) | 1 × 2 = 2 |
(H’, Bool) | 3 × 2 = 6 |
data Pair a b = Pair a b
type Pair a b = (a, b)
data Pair a b = Pair a b
data Pair a b = Pair
{ fieldA :: a
, fieldB :: b
}
Sum types Σ
Type | Inhibitants |
---|---|
() | 1 |
Bool | 2 |
() | Bool | 1 + 2 = 3 |
H’ | Bool | 3 + 2 = 5 |
data Either a b = Left a | Right b
Why not both?
Why not both?
data Crazy a b
= CrazyA a
| CrazyB b
| Both a b
| Neither
data Crazy a b
= CrazyA a
| CrazyB b
| Both a b
| Neither
Member | Inhibitants |
---|---|
CrazyA a | a |
CrazyB b | b |
Both a b | a × b |
Neither | 1 |
Σ | a + b + a × b + 1 |
Can there be a “0”?
Can there be a “0”?
Yes
Crazy Void ()
= CrazyA Void
| CrazyB ()
| Both Void ()
| Neither
Σ = 0 + 1 + 0 × 1 + 1 = 2
How do lists fit into this?
How do lists fit into this?
data List a
= Nil
| Cons a (List a)
-- [1, 2, 3] or 1 : 2 : 3 []
list1 = Cons 1 (Cons 2 (Cons 3 Nil))
-- []
list2 = Nil
data List a
= Nil
| Cons a (List a)
x = 1 + a * x
data List a
= Nil
| Cons a (List a)
x = 1 + a * x
x = 1 + a * (1 + a * x)
x = 1 + a * (1 + a * (1 + a * (...)))
data List a
= Nil
| Cons a (List a)
x = 1 + a * x
x = 1 + a * (1 + a * x)
x = 1 + a * (1 + a * (1 + a * (...)))
x = 1 + a + a² + a³ + a⁴ + a⁵ + ...
data List a
= Nil
| Cons a (List a)
x = 1 + a * x
x = 1 + a * (1 + a * x)
x = 1 + a * (1 + a * (1 + a * (...)))
x = 1 + a + a² + a³ + a⁴ + a⁵ + ...
data List a = () | (a) | (a, a) | (a, a, a) | ...
Element name | Color |
---|---|
Helium | orange |
Neon | red |
Argon | lavender |
Krypton | white |
Xenon | blue |
Radon | red |
data He = He -- Helium
data Ne = Ne -- Neon
data Ar = Ar -- Argon
data Kr = Kr -- Krypton
data Xe = Xe -- Xenon
data Rn = Rn -- Radon
How to convert noble gases to color?
toColor :: ? -> String
What about allowing everything in?
toColor :: a -> String
toColor a
| a == He = "orange"
| a == Ne = "red"
| otherwise = undefined
-- ???
_ = toColor "anything in"
_ = toColor 1234
What about treating noble gases as a sum type?
data Noble
= He
| Ne
| Ar
| Kr
| Xe
| Rn
a -> String
^
???
^
Noble -> String
class Noble a where
toColor :: a -> String
~
instance Noble He where
toColor _ = "orange"
instance Noble Ne where
toColor _ = "red"
instance Noble Ar where
toColor _ = "lavender"
Works:
λ> toColor He
"orange"
λ> toColor Ne
"red"
Doesn’t work:
λ> toColor C
<interactive>:6:1: error:
• No instance for (Noble C) arising from a use of ‘toColor’
• In the expression: toColor C
In an equation for ‘it’: it = toColor C
mixNoble :: (Noble n1, Noble n2) => n1 -> n2 -> String
mixNoble n1 n2 = toColor n1 <> "-" <> toColor n2
λ> mixNoble He Ne
"orange-red"
data Box a
= Has a
| Empty
deriving Show
data Cat = Cat String deriving Show
data Dog = Dog String deriving Show
class Mappable box where
map' :: (a -> b) -> box a -> box b
class Mappable box where
map' :: (a -> b) -> box a -> box b
instance Mappable Box where
map' _ Empty = Empty
map' f (Has a) = Has (f a)
instance Mappable [] where
map' _ [] = []
map' f xs = [f x | x <- xs]
instance Mappable [] where
map' _ [] = []
map' f xs = [f x | x <- xs]
λ> a = Has $ Cat "cat"
λ> :type a
a :: Box Cat
λ> :type map' toDog a
map' toDog a :: Box Dog
λ> :type map toDog [Cat "a", Cat "b"]
map toDog [Cat "a", Cat "b"] :: [Dog]
toDog :: Cat -> Dog
toDog (Cat name) = Dog name
convertAllCats :: Mappable box => box Cat -> box Dog
convertAllCats cs = map' toDog cs
Any “box” can go in 👍
convertAllCats :: Mappable box => box Cat -> box Dog
convertAllCats cs = map' toDog cs
λ> convertAllCats [Cat "a", Cat "b"]
[Dog "a",Dog "b"]
λ> convertAllCats $ Has $ Cat "a"
Has (Dog "a")
merge :: Cat -> Cat -> Dog
merge (Cat c1) (Cat c2) = Dog $ c1 <> " & " <> c2
catA = Cat "Meow"
catB = Cat "Nyaa"
λ> merge catA catB
Dog "Meow & Nyaa"
boxA = Has $ Cat "Meow" :: Box Cat
boxB = Has $ Cat "Nyaa" :: Box Cat
empty = Empty :: Box Cat
boxA = Has $ Cat "Meow" :: Box Cat
boxB = Has $ Cat "Nyaa" :: Box Cat
empty = Empty :: Box Cat
λ> merge boxA catB
<interactive>:7:7: error:
• Couldn't match expected type ‘Cat’ with actual type ‘Box Cat’
• In the first argument of ‘merge’, namely ‘boxA’
In the expression: merge boxA catB
In an equation for ‘it’: it = merge boxA catB
boxA = Has $ Cat "Meow" :: Box Cat
boxB = Has $ Cat "Nyaa" :: Box Cat
empty = Empty :: Box Cat
merge' :: Box Cat -> Box Cat -> Box Dog
merge' Empty _ = Empty
merge' _ Empty = Empty
merge' (Has c1) (Has c2) = Has $ merge c1 c2
merge' :: Box Cat -> Box Cat -> Box Dog
merge' Empty _ = Empty
merge' _ Empty = Empty
merge' (Has c1) (Has c2) = merge c1 c2
λ> merge' boxA boxB
Has (Dog "Meow & Nyaa")
λ> merge' boxA (Has catB)
Has (Dog "Meow & Nyaa")
λ> merge' boxA empty
Empty
class Appliable box where
wrap :: a -> box a
apply' :: box (a -> b) -> box a -> box b
class Appliable box where
wrap :: a -> box a
apply' :: box (a -> b) -> box a -> box b
instance Appliable Box where
wrap = Has
apply' Empty _ = Empty
apply' _ Empty = Empty
apply' (Has f) (Has a) = Has $ f a
instance Appliable [] where
wrap x = [x]
apply' [] _ = []
apply' _ [] = []
apply' fs xs = [f x | f <- fs, x <- xs]
instance Appliable Box where
wrap = Has
apply' Empty _ = Empty
apply' _ Empty = Empty
apply' (Has f) (Has a) = Has $ f a
instance Appliable [] where
wrap x = [x]
apply' [] _ = []
apply' _ [] = []
apply' fs xs = [f x | f <- fs, x <- xs]
λ> apply' (apply' (wrap merge) boxA) boxB
Has (Dog "Meow & Nyaa")
λ> apply' (apply' (wrap merge) boxA) empty
Empty
instance Appliable Box where
wrap = Has
apply' Empty _ = Empty
apply' _ Empty = Empty
apply' (Has f) (Has a) = Has $ f a
instance Appliable [] where
wrap x = [x]
apply' [] _ = []
apply' _ [] = []
apply' fs xs = [f x | f <- fs, x <- xs]
λ> apply' (apply' (wrap merge) [Cat "A"]) [Cat "B1", Cat "B2"]
[Dog "A & B1",Dog "A & B2"]
λ> apply' (apply' (wrap merge) [Cat "A"]) []
[]
λ> apply' (apply' (wrap merge) [Cat "A"]) [Cat "B1", Cat "B2"]
[Dog "A & B1",Dog "A & B2"]
λ> apply' (apply' (wrap merge) [Cat "A"]) []
[]
λ> wrap merge `apply'` [Cat "A"] `apply'` [Cat "B1", Cat "B2"]
[Dog "A & B1",Dog "A & B2"]
λ> wrap merge `apply'` [Cat "A"] `apply'` []
[]
λ> wrap merge `apply'` [Cat "A"] `apply'` [Cat "B1", Cat "B2"]
[Dog "A & B1",Dog "A & B2"]
λ> wrap merge `apply'` [Cat "A"] `apply'` []
[]
λ> wrap merge `apply'` boxA `apply'` boxB
Has (Dog "Meow & Nyaa")
λ> wrap merge `apply'` boxA `apply'` empty
Empty
merge4 :: Cat -> Cat -> Cat -> Cat -> Dog
merge4 (Cat a) (Cat b) (Cat c) (Cat d) = Dog $ a <> b <> c <> d
λ> wrap merge4 `apply'` boxA `apply'` boxB `apply'` boxA `apply'` boxB
Has (Dog "MeowNyaaMeowNyaa")
λ> wrap merge4 `apply'` boxA `apply'` boxB `apply'` empty `apply'` boxB
Empty
killOrSave :: Cat -> Box Cat
killOrSave cat@(Cat name) = case name of
"Meow" -> Empty
_ -> Has cat
(no animals were harmed in the making of this slideshow)
killOrSave :: Cat -> Box Cat
killOrSave cat@(Cat name) = case name of
"Meow" -> Empty
_ -> Has cat
λ> wrap killOrSave `apply'` Has (Cat "Meow")
Has Empty
λ> wrap killOrSave `apply'` Has (Cat "Nyaa")
Has (Has (Cat "Nyaa"))
λ> wrap killOrSave `apply'` Empty
Empty
class Chainable box where
chain :: box a -> (a -> box b) -> box b
class Chainable box where
chain :: box a -> (a -> box b) -> box b
instance Chainable Box where
chain Empty _ = Empty
chain (Has a) f = f a
instance Chainable [] where
chain [] _ = []
chain xs f = [x' | x <- xs, x' <- f x]
instance Chainable Box where
chain Empty _ = Empty
chain (Has a) f = f a
instance Chainable [] where
chain [] _ = []
chain xs f = [x' | x <- xs, x' <- f x]
kill :: Cat -> Box Cat
kill _ = Empty
save :: Cat -> Box Cat
save = Has
λ> boxA `chain` save `chain` save `chain` save
Has (Cat "Meow")
λ> boxA `chain` save `chain` kill `chain` save
Empty
kill' :: Cat -> [Cat]
kill' _ = []
save' :: Cat -> [Cat]
save' c = [c]
clone :: Cat -> [Cat]
clone (Cat c) = [Cat $ c <> "L" , Cat $ c <> "R"]
kill' :: Cat -> [Cat]
kill' _ = []
save' :: Cat -> [Cat]
save' c = [c]
clone :: Cat -> [Cat]
clone (Cat c) = [Cat $ c <> "L" , Cat $ c <> "R"]
λ> [catA] `chain` save' `chain` save' `chain` save'
[Cat "Meow"]
λ> [catA] `chain` save' `chain` clone `chain` save'
[Cat "MeowL",Cat "MeowR"]
λ> [catA] `chain` more' `chain` clone `chain` save'
[Cat "MeowLL",Cat "MeowLR",Cat "MeowRL",Cat "MeowRR"]
λ> [catA] `chain` clone `chain` clone `chain` kill'
[]
λ> [catA] `chain` save' `chain` save' `chain` save'
[Cat "Meow"]
λ> [catA] `chain` save' `chain` clone `chain` save'
[Cat "MeowL",Cat "MeowR"]
λ> [catA] `chain` more' `chain` clone `chain` save'
[Cat "MeowLL",Cat "MeowLR",Cat "MeowRL",Cat "MeowRR"]
λ> [catA] `chain` clone `chain` clone `chain` kill'
[]
What’s a Mappable
?
It’s a Functor
It’s a Functor
class Mappable box where
map' :: (a -> b) -> box a -> box b
class Functor f where
fmap :: (a -> b) -> f a -> f b
(<$) :: a -> f b -> f a
It’s a Functor
λ> map' (+1) []
[]
λ> map' (+1) [1, 2, 3]
[2,3,4]
λ> map' (*3) [1, 2, 3]
[3,6,9]
λ> fmap (+1) []
[]
λ> fmap (+1) [1, 2, 3]
[2,3,4]
λ> fmap (*3) [1, 2, 3]
[3,6,9]
λ> 1 <$ [1, 2, 3]
[1,1,1]
It’s a Functor
It’s a Functor
main :: IO ()
main = print "Hello World!"
What’s a Appliable
?
It’s an Applicative
It’s an Applicative
class Appliable box where
wrap :: a -> box a
apply' :: box (a -> b) -> box a -> box b
class (Functor f) => Applicative f where
pure :: a -> f a
(<*>) :: f (a -> b) -> f a -> f b
It’s an Applicative
λ> wrap merge `apply'` [catA] `apply'` []
[]
λ> wrap merge `apply'` [catA] `apply'` [catB]
[Dog "Meow & Nyaa"]
λ> wrap merge `apply'` [catA] `apply'` [catB, Cat "C"]
[Dog "Meow & Nyaa",Dog "Meow & C"]
λ> pure merge <*> [catA] <*> []
[]
λ> pure merge <*> [catA] <*> [catB]
[Dog "Meow & Nyaa"]
λ> pure merge <*> [catA] <*> [catB, Cat "C"]
[Dog "Meow & Nyaa",Dog "Meow & C"]
λ> pure merge <*> [catA] <*> []
[]
λ> pure merge <*> [catA] <*> [catB]
[Dog "Meow & Nyaa"]
λ> pure merge <*> [catA] <*> [catB, Cat "C"]
[Dog "Meow & Nyaa",Dog "Meow & C"]
λ> merge <$> [catA] <*> []
[]
λ> merge <$> [catA] <*> [catB]
[Dog "Meow & Nyaa"]
λ> merge <$> [catA] <*> [catB, Cat "C"]
[Dog "Meow & Nyaa",Dog "Meow & C"]
merge :: Cat -> Cat -> Dog
_ = merge catA catB
What’s a Chainable
?
It’s a monad
It’s a monad
class Chainable box where
chain :: box a -> (a -> box b) -> box b
class Applicative m => Monad m where
(>>=) :: m a -> (a -> m b) -> m b
(>>) :: m a -> m b -> m b
m >> k = m >>= \_ -> k
return :: a -> m a
return = pure
It’s a monad
λ> [catA] `chain` save' `chain` save' `chain` save'
[Cat "Meow"]
λ> [catA] `chain` save' `chain` clone `chain` save'
[Cat "MeowL",Cat "MeowR"]
λ> [catA] `chain` save' `chain` clone `chain` kill'
[]
λ> [catA] >>= save' >>= save' >>= save'
[Cat "Meow"]
λ> [catA] >>= save' >>= clone >>= save'
[Cat "MeowL",Cat "MeowR"]
λ> [catA] >>= save' >>= clone >>= kill'
[]