Week 6 Exercises
These exercises take a dive into the abstract nonsense that motivates the things we take for granted. While the words are big and daunting, the code that follows is rarely longer than a line.
Exercise 1
The base library functions pertaining to foldables and traversables are related to each other in several different ways. However, this is obscured by the type class hierarchy and the clever default definitions it hides.
Implement the instances that witness the relations between the different functions. While doing so, try to find a way to avoid using the unwrapped functions with the respective wrappers.
This is trickier than it might seem, so be patient!
module Week6.Exercise1 where
import Data.Functor.Compose
import Data.Functor.Const
import Data.Functor.Identity
newtype WrappedTraversable m a = WrapTraversable {unwrapTraversable :: m a}
instance Traversable m => Functor (WrappedTraversable m) where
fmap f (WrapTraversable xs) = _
instance Traversable m => Foldable (WrappedTraversable m) where
foldMap f (WrapTraversable xs) = _
instance Traversable m => Traversable (WrappedTraversable m) where
sequenceA (WrapTraversable xs) = _
traverse k (WrapTraversable xs) = _Exercise 2
Type classes sometimes admit several formulations that end up being equivalent. Such formulations can be very useful if, for instance, one is more convenient to use and another has laws that are easier to prove, because it allows us to pick the best parts from each formulation and transport them along the equivalences.
Let us consider the case of functors, applicative functors and monads. They are defined in the base library as follows.
-- | ==== Laws
--
-- prop> fmap id = id
-- prop> fmap (g . f) = fmap g . fmap f
class Functor m where
fmap :: (a -> b) -> m a -> m b
-- | ==== Laws
--
-- prop> pure id <*> xs = xs
-- prop> pure (.) <*> fs <*> gs <*> xs = fs <*> (gs <*> xs)
-- prop> pure f <*> pure x = pure (f x)
-- prop> fs <*> pure x = pure ($ x) <*> fs
class Functor m => Applicative m where
pure :: a -> m a
(<*>) :: m (a -> b) -> m a -> m b
infixl 4 <*>
-- | ==== Laws
--
-- prop> pure x >>= k = k x
-- prop> xs >>= pure = xs
-- prop> xs >>= (\ x -> k x >>= m) = xs >>= k >>= m
class Applicative m => Monad m where
(>>=) :: m a -> (a -> m b) -> m b
infixl 1 >>=We can define them in another way, such that we obtain
- functors via pure bind, which we call covariant for the lack of a better term,
- applicative functors via lifted zip, which are traditionally called monoidal, and
- monads via join, which we dub triads to pay homage to old mathematical literature.
They are customarily defined as follows.
-- | ==== Laws
--
-- prop> xs <&> id = xs
-- prop> xs <&> g . f = xs <&> f <&> g
class Covariant m where
(<&>) :: m a -> (a -> b) -> m b
infixl 1 <&>
-- | ==== Laws
--
-- prop> unit >*< ys <&> snd = ys
-- prop> xs >*< unit <&> fst = xs
-- prop> let a (x, (y, z)) = ((x, y), z) in a <$> xs >*< (ys >*< zs) = (xs >*< ys) >*< zs
class Covariant m => Monoidal m where
unit :: m ()
(>*<) :: m a -> m b -> m (a, b)
infix 5 >*<
-- | ==== Laws
--
-- prop> join . pure = id
-- prop> join . fmap pure = id
-- prop> join . fmap join = join . join
class Monoidal m => Triad m where
join :: m (m a) -> m aShow that our hierarchy is equivalent to the one in the base library by implementing the classes in terms of each other and proving that the laws are preserved. Your code must compile, but your proofs may be as informal as you wish.
{-# LANGUAGE ViewPatterns #-}
module Week6.Exercise2 where
class Covariant m where
(<&>) :: m a -> (a -> b) -> m b
infixl 1 <&>
class Covariant m => Monoidal m where
unit :: m ()
(>*<) :: m a -> m b -> m (a, b)
infix 5 >*<
class Monoidal m => Triad m where
join :: m (m a) -> m a
newtype WrappedFunctor m a = WrapFunctor {unwrapFunctor :: m a}
instance Covariant m => Functor (WrappedFunctor m) where
fmap f (WrapFunctor xs) = _
instance Functor m => Covariant (WrappedFunctor m) where
WrapFunctor xs <&> f = _
newtype WrappedCovariant m a = WrapCovariant {unwrapCovariant :: m a}
instance Covariant m => Functor (WrappedCovariant m) where
fmap f (WrapCovariant xs) = WrapCovariant
(unwrapFunctor (fmap f (WrapFunctor xs)))
instance Functor m => Covariant (WrappedCovariant m) where
WrapCovariant xs <&> f = WrapCovariant (unwrapFunctor (WrapFunctor xs <&> f))
newtype WrappedApplicative m a = WrapApplicative {unwrapApplicative :: m a}
instance Covariant m => Functor (WrappedApplicative m) where
fmap f (WrapApplicative xs) = WrapApplicative
(unwrapFunctor (fmap f (WrapFunctor xs)))
instance Functor m => Covariant (WrappedApplicative m) where
WrapApplicative xs <&> f = WrapApplicative
(unwrapFunctor (WrapFunctor xs <&> f))
instance Monoidal m => Applicative (WrappedApplicative m) where
pure x = _
WrapApplicative fs <*> WrapApplicative xs = _
instance Applicative m => Monoidal (WrappedApplicative m) where
unit = _
WrapApplicative xs >*< WrapApplicative ys = _
newtype WrappedMonoidal m a = WrapMonoidal {unwrapMonoidal :: m a}
instance Covariant m => Functor (WrappedMonoidal m) where
fmap f (WrapMonoidal xs) = WrapMonoidal
(unwrapFunctor (fmap f (WrapFunctor xs)))
instance Functor m => Covariant (WrappedMonoidal m) where
WrapMonoidal xs <&> f = WrapMonoidal (unwrapFunctor (WrapFunctor xs <&> f))
instance Monoidal m => Applicative (WrappedMonoidal m) where
pure x = WrapMonoidal (unwrapApplicative (pure x))
WrapMonoidal fs <*> WrapMonoidal xs = WrapMonoidal
(unwrapApplicative (WrapApplicative fs <*> WrapApplicative xs))
instance Applicative m => Monoidal (WrappedMonoidal m) where
unit = WrapMonoidal (unwrapApplicative unit)
WrapMonoidal xs >*< WrapMonoidal ys = WrapMonoidal
(unwrapApplicative (WrapApplicative xs >*< WrapApplicative ys))
newtype WrappedMonad m a = WrapMonad {unwrapMonad :: m a}
instance Covariant m => Functor (WrappedMonad m) where
fmap f (WrapMonad xs) = WrapMonad (unwrapFunctor (fmap f (WrapFunctor xs)))
instance Functor m => Covariant (WrappedMonad m) where
WrapMonad xs <&> f = WrapMonad (unwrapFunctor (WrapFunctor xs <&> f))
instance Monoidal m => Applicative (WrappedMonad m) where
pure x = WrapMonad (unwrapApplicative (pure x))
WrapMonad fs <*> WrapMonad xs = WrapMonad
(unwrapApplicative (WrapApplicative fs <*> WrapApplicative xs))
instance Applicative m => Monoidal (WrappedMonad m) where
unit = WrapMonad (unwrapApplicative unit)
WrapMonad xs >*< WrapMonad ys = WrapMonad
(unwrapApplicative (WrapApplicative xs >*< WrapApplicative ys))
instance Triad m => Monad (WrappedMonad m) where
WrapMonad xs >>= ((unwrapMonad .) -> k) = _
instance Monad m => Triad (WrappedMonad m) where
join (WrapMonad xs) = _
newtype WrappedTriad m a = WrapTriad {unwrapTriad :: m a}
instance Covariant m => Functor (WrappedTriad m) where
fmap f (WrapTriad xs) = WrapTriad (unwrapFunctor (fmap f (WrapFunctor xs)))
instance Functor m => Covariant (WrappedTriad m) where
WrapTriad xs <&> f = WrapTriad (unwrapFunctor (WrapFunctor xs <&> f))
instance Monoidal m => Applicative (WrappedTriad m) where
pure x = WrapTriad (unwrapApplicative (pure x))
WrapTriad fs <*> WrapTriad xs = WrapTriad
(unwrapApplicative (WrapApplicative fs <*> WrapApplicative xs))
instance Applicative m => Monoidal (WrappedTriad m) where
unit = WrapTriad (unwrapApplicative unit)
WrapTriad xs >*< WrapTriad ys = WrapTriad
(unwrapApplicative (WrapApplicative xs >*< WrapApplicative ys))
instance Triad m => Monad (WrappedTriad m) where
WrapTriad xs >>= ((unwrapTriad .) -> k) = WrapTriad
(unwrapMonad (WrapMonad xs >>= WrapMonad . k))
instance Monad m => Triad (WrappedTriad m) where
join ((<&> unwrapTriad) -> WrapTriad xs) = WrapTriad
(unwrapMonad (join (WrapMonad (fmap WrapMonad xs))))Exercise 3
There is a deep reason for why algebraic data types are called just that. In order to explore the reason fully, we need to push the definition of a semiring beyond what is normally considered to be in good taste.
Let a commutative exponential semiring be such a thing that consists of
- a type, \(A : \mathcal U\),
- an binary relation for equivalence, \((\sim) : A \to A \to \mathcal U\),
- a binary operator for addition, \((+) : A \to A \to A\),
- a point for zero, \(0 : A\),
- a binary operator for addition, \((\times) : A \to A \to A\),
- a point for one, \(1 : A\),
- a binary operator for exponentiation, \((\uparrow) : A \to A \to A\),
- a proof that equivalence is reflexive, \(r_{(\sim)} : \forall_{x : A} x \sim x\),
- a proof that equivalence is symmetric, \(s_{(\sim)} : \forall_{x y : A} x \sim y \to y \sim x\),
- a proof that equivalence is transitive, \(t_{(\sim)} : \forall_{x, y, z : A} x \sim y \to y \sim z \to x \sim z\),
- a proof that addition is proper, \(p_{(\sim), (+)} : \forall_{x, y, z, w : A} x \sim y \to z \sim w \to x + z \sim y + w\),
- a proof that addition is associative, \(a_{(\sim), (+)} : \forall_{x, y, z : A} x + (y + z) \sim (x + y) + z\),
- a proof that addition is commutative, \(c_{(\sim), (+)} : \forall_{x, y : A} x + y \sim y + x\),
- a proof that zero is unitary with respect to addition on the left, \(l_{(\sim), (+), 0} : \forall_{x : A} 0 + x \sim x\),
- a proof that zero is unitary with respect to addition on the right, \(r_{(\sim), (+), 0} : \forall_{x : A} x + 0 \sim x\),
- a proof that multiplication is proper, \(p_{(\sim), (\times)} : \forall_{x, y, z, w : A} x \sim y \to z \sim w \to x \times z \sim y \times w\),
- a proof that multiplication is associative, \(a_{(\sim), (\times)} : \forall_{x, y, z : A} x \times (y \times z) \sim (x \times y) \times z\),
- a proof that multiplication is commutative, \(c_{(\sim), (\times)} : \forall_{x, y : A} x \times y \sim y \times x\),
- a proof that one is unitary with respect to multiplication on the left, \(l_{(\sim), (\times), 1} : \forall_{x : A} 1 \times x \sim x\),
- a proof that one is unitary with respect to multiplication on the right, \(r_{(\sim), (\times), 1} : \forall_{x : A} x \times 1 \sim x\),
- a proof that multiplication is distributive over addition on the left, \(l_{(\sim), (+), (\times)} : \forall_{x, y, z : A} x \times (y + z) \sim x \times y + x \times z\),
- a proof that multiplication is distributive over addition on the right, \(r_{(\sim), (+), (\times)} : \forall_{x, y, z : A} (x + y) \times z \sim x \times z + y \times z\),
- a proof that zero is absorbing with respect to multiplication on the left, \(l_{(\sim), 0, (\times)} : \forall_{x : A} 0 \times x \sim 0\),
- a proof that zero is absorbing with respect to multiplication on the right, \(r_{(\sim), 0, (\times)} : \forall_{x : A} x \times 0 \sim 0\),
- a proof that exponentiation is proper, \(p_{(\sim), (\uparrow)} : \forall_{x, y, z, w : A} x \sim y \to z \sim w \to z^x \sim w^y\),
- a proof that exponentiation is distributive over addition and multiplication on the right, \(r_{(\sim), (+), (\times), (\uparrow)} : \forall_{x, y, z : A} x^{y + z} \sim x^y \times x^z\),
- a proof that exponentiation is associative over multiplication on the right, \(r_{(\sim), (\times), (\uparrow)} : \forall_{x, y, z : A} x^{y \times z} \sim (x^y)^z\),
- a proof that exponentiation is distributive over multiplication on the left, \(l_{(\sim), (\times), (\uparrow)} : \forall_{x, y, z : A} (x \times y)^z \sim x^z \times y^z\),
- a proof that one is a unit of exponentiation on the left, \(l_{(\sim), 1, (\uparrow)} : \forall_{x : A} x^1 \sim x\),
- a proof that one is absorbing with respect to exponentiation on the right, \(r_{(\sim), 1, (\uparrow)} : \forall_{x : A} 1^x \sim 1\), and
- a proof that zero is absorbing with respect to exponentiation on the left, \(l_{(\sim), 0, 1, (\uparrow)} : \forall_{x : A} x^0 \sim 1\).
This may seem like a ridiculously complicated definition, but, upon closer inspection, it merely captures those parts of algebra that are taught to children in primary school. It does not even touch the questions of expanding \((x + y)^z\) or deciding whether \(0^x\) should be \(0\) or \(1\).
One of the most obvious examples of a commutative exponential semiring is that of natural numbers, where the equivalence relation is decidable equality \((x, y) \mapsto (x = y) + (x \ne y)\), the operations are addition \((x, y) \mapsto x + y\), multiplication \((x, y) \mapsto x \times y\) and exponentiation \((x, y) \mapsto y^x\) and the points are zero \(0\) and one \(1\).
Another example, which we are particularly interested in, is that of types, where the equivalence relation of choice is isomorphism over extensional equality \((A, B) \mapsto A \cong B\), the operations are sum type formation \((A, B) \mapsto A + B\), product type formation \((A, B) \mapsto A \times B\) and function type formation \((A, B) \mapsto A \to B\) and the points are the empty type \(\mathbf 0\) and the unit type \(\mathbf 1\). While these types should be familiar to you, the equivalence relation probably requires some explanation.
Two types are isomorphic precisely when all their inhabitants can be converted into each other without losing information. More precisely, an isomorphism between any two types is witnessed by the relation \[\begin{eqnarray} (\cong) & : & \mathcal U \times \mathcal U \to \mathcal U \\ A \cong B & \equiv & \exists_{f : A \to B} \exists_{g : B \to A} g \circ f = \mathrm{id}\wedge f \circ g = \mathrm{id}. \end{eqnarray}\] If the inhabitants happen to be functions, we assume them to be equal precisely when they produce the same results for the same arguments. This assumption is known as the axiom of functional extensionality and manifests as the opaque inhabitant \[\begin{eqnarray} \mathrm{funext}& : & \forall_{A, B : \mathcal U} \forall_{f, g : A \to B} (\forall_{x : A} f (x) = g (x)) \to f = g. \end{eqnarray}\] The other direction can be proven without assumptions, so that functional extensionality can be seen to witness an equivalence as well.
To see how these definitions actually form a commutative exponential semiring, let us go through an exemplary proof of \[\forall_{x, y, z : A} x^{y \times z} \cong (x^y)^z.\] We begin by unfolding \(\sim\), \(\times\) and \(\uparrow\) to obtain \[\forall_{A, B, C : \mathcal U} \exists_{f : (B \times C \to A) \to (C \to (B \to A))} \exists_{g : (C \to (B \to A)) \to (B \times C \to A)} \\ g \circ f = \mathrm{id}\wedge f \circ g = \mathrm{id}.\] In order to get rid of the universal quantifiers, we assume \(A, B, C : \mathcal U\) to be arbitrary, and, to get rid of the existential quantifiers, we define the witnesses \[\begin{eqnarray} f & : & (B \times C \to A) \to (C \to (B \to A)) \\ f (m) & \equiv & z \mapsto y \mapsto m (y, z) \\ g & : & (C \to (B \to A)) \to (B \times C \to A) \\ g (m) & \equiv & (y, z) \mapsto m (z) (y). \end{eqnarray}\] We are left with having to prove \(g \circ f = \mathrm{id}\wedge f \circ g = \mathrm{id}\), which we can do in two parts.
- If we apply \(\mathrm{funext}\) twice to \(g \circ f = \mathrm{id}\), we get \[\forall_{m : B \times C \to A} \forall_{(y, z) : B \times C} (g \circ f) (m) (y, z) = \mathrm{id}(m) (y, z).\] Having done this, we assume \(m : B \times C \to A\) and \((y, z) : B \times C\) to be arbitrary, so that we are left with \((g \circ f) (m) (y, z) = \mathrm{id}(m) (y, z)\). We can finally unfold \(\circ\) and \(\mathrm{id}\) to obtain \(g (f (m)) (y, z) = m (y, z)\) and further unfold \(g\) and \(f\) to end up with \(m (y, z) = m (y, z)\). This is true by the reflexivity of \(=\).
- If we follow the same reasoning for \(f \circ g = \mathrm{id}\), we can draw a similar conclusion (try it and see).
This concludes the proof, but also lets us make a curious observation.
If we implement the conversion functions \(f\) and \(g\) in Haskell as arrow_right_associator and arrow_right_coassociator respectively, we will quickly notice that arrow_right_associator = flip . curry and arrow_right_coassociator = uncurry . flip. Indeed, we have inadvertently rediscovered slighly wonky versions of two very familiar functions. As you might have guessed, this is not the only proof, where such a thing happens.
Figure out the types of the conversion functions behind the remaining proofs, implement them in Haskell and see if they look familiar. You do not need to write the corresponding proofs, but you should be mindful of your functions not losing information.