aez-notes

Type theory
- Skolems constants causing trouble
- Existential types
Functional programming

A monad is just a monoid in the category of endofunctors, what's the problem?

Type theory

Skolems constants causing trouble

The names "skolem" and "rigid" are synonymous for Haskell. Based on this stackoverflow answer it appears that skolem constants (types) cause a error at compile time because they cannot be resolved. Consider the following definition of a wrapper type

{-# LANGUAGE ExistentialQuantification #-}

data AnyFoo = forall a. Eq a => AnyFoo a

If we try and define a function which unwraps,

getFoo (AnyFoo x) = x

it will not lead to a type error because it is unclear what the return type of getFoo should be. However, we can still use the value in a AnyFoo, we just need to avoid it appearing in the type of the function.

boring :: AnyFoo -> Bool
boring (AnyFoo x) = x == x

Existential types

To make use of existential types in Haskell, you need to include the ExistentialQuantification extension. Then you can implement a class such as ShowBox which allows you to wrap up multiple types in a shared wrapper. The significance of this is that it lets you write code such as the following and have it type check.

data ShowBox = forall s. Show s => SB s

instance Show ShowBox where
  show (SB s) = show s

heteroList :: [ShowBox]
heteroList = [SB (), SB 5, SB True]

Functional programming

Functor

<$> is infix for fmap

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

The functor laws are fmap id = id and fmap (f . g) == fmap f . fmap g. The intuition behind this type class is that it should act as a container and the fmap should not disrupt the structure in the container.

Applicative

<*> is infix the "apply" function when working with applicatives.

class Functor f => Applicative f where
  pure  :: a -> f a
  (<*>) :: f (a -> b) -> f a -> f b

This is like a stronger version of functor where the function being applied can also live in the computational context of the container.

Monad

class Applicative m => Monad m where
  (>>=) :: m a -> (a -> m b) -> m b
  return :: a -> m a
  (>>) :: m a -> m b -> m b

join :: Monad m => m (m a) -> m a

Foldable

class Foldable t where
  foldMap :: Monoid m => (a -> m) -> t a -> m
  foldr   :: (a -> b -> b) -> b -> t a -> b

The intuition behind this type class is that it should act as a container that can be collapsed down to a single value.

Traversable

class (Functor t, Foldable t) => Traversable t where
  traverse  :: Applicative f => (a -> f b) -> t a -> f (t b)
  sequenceA :: Applicative f => t (f a) -> f (t a)

This is a bit like a functor where the function returns values in a context. Perhaps a useful way to think about this class is to contrast the types of fmap and traverse:

fmap     :: (a -> f b) -> t a -> t (f b)
traverse :: (a -> f b) -> t a -> f (t b)

where f is an applicative and t is a traversable.

Fold and friends

The friends include: scan, accumulate, and reduce.

Left fold

foldl :: Foldable t => (b -> a -> b) -> b -> t a -> b

foldl f z [x1, x2, ..., xn] == (...((z `f` x1) `f` x2) `f`...) `f` xn

This will build a collections of thunks, to it is probably better to use the strict version foldl'.

Right fold

foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b

foldr f z [x1, x2, ..., xn] == x1 `f` (x2 `f` ... (xn `f` z)...)

This one can be applied to infinte lists and still terminate.

Combinators

on

-- | @'on' b u x y@ runs the binary function @b@ /on/ the results of applying
-- unary function @u@ to two arguments @x@ and @y@. From the opposite
-- perspective, it transforms two inputs and combines the outputs.
on :: (b -> b -> c) -> (a -> b) -> a -> a -> c

&

-- | '&' is a reverse application operator.  This provides notational
-- convenience.  Its precedence is one higher than that of the forward
-- application operator '$', which allows '&' to be nested in '$'.
--
-- >>> 5 & (+1) & show
-- "6"
(&) :: a -> (a -> b) -> b

Total and partial functions

A partial function is a generalisation of a mathematical function which allows the function to be defined on only a subset of the domain. If a function is not partial it is pure.

When programming, partial functions can lead to hard to bugs. Use the of maybe monad or the either monad can be useful to avoid partial functions. Pattern matching as case switches can be a source of partial functions but there are static analysis tools to help with this for strong languages.