Week 1 Exercises

The best way to understand abstract concepts is through examples and counterexamples, so these exercises involve lots of them.

Exercise 1

Some of the following types admit decidable equivalence relations, while others do not.

1. Instances for Bool.
2. Instances for Maybe a, given instances for a.
3. Instances for Either a b, given instances for a and b.
4. Instances for (a, b), given instances for a and b.
5. Instances for a -> a, given instances for a.
6. Instances for a -> b, given instances for b.
7. Instances for ().
8. Instances for [a], given instances for a.
9. Instances for NonEmpty a, given instances for a.
10. Instances for Void.
11. Instances for IO a, given instances for a.
12. Instances for Map k a, given instances for a.

Figure out which ones do, find out how many options there are, implement the corresponding type class instances and prove that your instances are coherent. Your code must compile, but your proofs may be as informal as you wish.

Since some of these instances already exist in Prelude, you may need to use the following wrappers or introduce new ones to avoid duplicate instance declaration errors. However, be mindful not to accidentally use the existing instances from Prelude!

module Week1.Exercise1 where

import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NonEmpty
import Data.Map (Map (..))
import qualified Data.Map as Map
import Data.Void

newtype Bool' = Bool' {getBool' :: Bool}
  deriving Show

newtype Maybe' a = Maybe' {getMaybe' :: Maybe a}
  deriving Show

newtype Either' a b = Either' {getEither' :: Either a b}
  deriving Show

Exercise 2

Some of the following types admit monoids, while others admit only semigroups.

1. Instances for Bool.
2. Instances for Maybe a, given instances for a.
3. Instances for Either a b.
4. Instances for (a, b), given instances for a and b.
5. Instances for a -> a.
6. Instances for a -> b, given instances for b.
7. Instances for ().
8. Instances for [a].
9. Instances for NonEmpty a.
10. Instances for Void.
11. Instances for IO a, given instances for a.
12. Instances for Map k a, given instances for a.

Figure out which ones admit which, find out how many options there are, implement the corresponding type class instances and prove that your instances are coherent. Your code must compile, but your proofs may be as informal as you wish.

Same considerations apply as in exercise 1.

module Week1.Exercise2 where

import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NonEmpty
import Data.Map (Map (..))
import qualified Data.Map as Map
import Data.Void

Exercise 3

Type classes are usually implemented in such a way that the compiler converts classes into types and instances into inhabitants of said types. As a consequence, class constraints become implicit arguments, whose resolution is based on proof search.

Take the following program and perform this conversion by hand. That is, replace all the familiar classes with types, instances with inhabitants, class constraints with explicit arguments and resolved instances with the appropriate inhabitants. You may leave the Monad class alone, since it is hidden beneath the do notation.

You should be able to get rid of all the language extensions in the process, although you will still need the MagicHash extension if you decide to use primitive operations from the GHC.Exts module.

{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}

module Week1.Exercise3 where

import Control.Monad.State
import Data.List

class Transaction k m a where
  recall :: k -> m a
  store :: k -> a -> m ()

storeFirst :: Transaction Int m a => a -> m ()
storeFirst x = store (0 :: Int) x

data Cursor a = WayBefore | Before [a] | At [a] a [a] | After [a] | WayAfter

navigate :: Int -> [a] -> Cursor a
navigate n xs = case compare n (pred 0) of
  LT -> WayBefore
  EQ -> Before xs
  GT -> let
    f :: Int -> [a] -> Cursor a
    f p []
      | p == 0 = After []
      | otherwise = WayAfter
    f p (z : zs)
      | p == 0 = At [] z zs
      | otherwise = case f (pred p) zs of
        At bs a as -> At (z : bs) a as
        After bs -> After (z : bs)
        c -> c in
    f n xs

database :: FilePath
database = "/tmp/database"

instance Transaction Int IO String where
  recall i = do
    s <- readFile database
    seq (length s) (pure ())
    case navigate i (lines s) of
      At _ c _ -> pure c
      _ -> ioError (userError "Invalid line number")
  store i x = do
    s <- readFile database
    seq (length s) (pure ())
    case navigate i (lines s) of
      Before rs -> writeFile database
        (unlines (x : rs))
      At ls _ rs -> writeFile database
        (unlines (ls <> (x : rs)))
      After ls -> writeFile database
        (unlines (ls <> [x]))
      _ -> ioError (userError "Invalid line number")

instance Transaction Int (State (Int -> String)) String where
  recall i = gets $ \ f -> f i
  store i x = modify $ \ f j -> if j == i then x else f j

work :: IO String
work = do
  storeFirst "zero"
  store (1 :: Int) "one"
  store (2 :: Int) "two"
  x <- recall (0 :: Int)
  y <- recall (1 :: Int)
  z <- recall (2 :: Int)
  pure (intercalate " " [x, y, z])

mock :: String
mock = let
  f :: Int -> String
  f _ = mempty in
  flip evalState f $ do
  storeFirst "zero"
  store (1 :: Int) "one"
  store (2 :: Int) "two"
  x <- recall (0 :: Int)
  y <- recall (1 :: Int)
  z <- recall (2 :: Int)
  pure (intercalate " " [x, y, z])