Overview

When programs behave as math functions, standard math techniques can be used to reason about such programs

• Equational reasoning
  • Programs as equations
• Structural induction
  • Use of recursion

Equational Reasoning

Proving Option as Monad

instance Monad Option where 
    return x = Some x 
    None >>= f = None 
    (Some x) >>= f = f x

-- return a >>= k = k a
return a >>= k
{- definition of return -}
= Some a >>= k
{- definition of >>= -}
= k a

-- m >>= return = m
m >>= return
{- Case 1: m is None -}
    = None >>= return
    {- definition of >>= -}
    = None
{- Case 1: m is Some x -}
    = Some x >>= return
    {- definition of >>= -}
    = return x
    {- definition of return -}
    = Some x

-- m >>= (\x -> k x >>= h) = (m >>= k) >>= h
m >>= (\x -> k x >>= h)
{- Case 1: m is None -}
    = None >>= (\x -> k x >>= h)
    {- definition of >>= -}
    = None
    {- definition of >>= -}
    = None >>= h
    {- definition of >>= -}
    = (None >>= k) >>= h
{- Case 2: m is Some y -}
Some y >>= (\x -> k x >>= h)
    {- definition of >>=: ((Some x) >>= f = f x) -}
    = (\x -> k x >>= h) y
    {- simplification -}
    = k y >>= h
    {- definition of bind -}
    = (Some y >>= k) >>= h

Structural Induction

Proving Map Function

map :: (a -> b) -> [a] -> [b] 
map f [] = [] 
map f (x:xs) = f x : map f xs

-- map id xs
map id []
{- xs = [] -}
    {- definition of map -}
    = []
map id (y:ys)
{- xs = (y:ys) -}
    {- definition of map -}
    = id y : map id ys
    {- definition of id -}
    = y : map id ys
    {- induction hypothesis -}
    = y : ys

-- map f (map g xs) = map (f . g) xs
map_dot f (map g [])
{- xs = [] -}
    = map f (map g [])
    {- definition of map -}
    = map f []
    {- definition of map -}
    = []
    {- definition of map -}
    = map (f . g) []
map_dot f (map g (y:ys))
{- xs = y:ys -}
    = map f (map g (y:ys))
    {- definition of map -}
    = map f (g y : map g ys)
    {- definition of map -}
    = f (g y) : map f (map g ys)
    {- induction hypothesis -}
    = f (g y) : map (f . g) ys ? map_dot f (map g ys)
    {- definition of . -}
    = (f . g) y : map (f . g) ys 
    {- definition of map -}
    = map (f . g) (y:ys)

Functors

class Functor f where
    fmap :: (a -> b) -> f a -> f b

-- Laws

fmap f (fmap g fa) = fmap (f . g) fa
fmap id fa = fa

List Functor

instance Functor [] where
    fmap = map

Maybe Functor

instance Functor Maybe where
    fmap f Nothing = Nothing
    fmap f (Just x) = Just (f x)