InitialHEADmaster

33 files changed, 1427 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..c33954f
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+dist-newstyle/
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..c114dbd
--- /dev/null
+++ b/README.md
@@ -0,0 +1,4 @@
+My solutions to Sandy's amazing book.
+https://thinkingwithtypes.com/
+
+Not all exercises are included. I focused on those that require actual coding.
diff --git a/ch01_01.4-ii.hs b/ch01_01.4-ii.hs
new file mode 100644
index 0000000..552c1e5
--- /dev/null
+++ b/ch01_01.4-ii.hs
@@ -0,0 +1,8 @@
+-- Exercise 1.4-ii
+-- Give a prove of the exponent law that `a^b * a^c == a^(b+c)`.
+tup2Either :: (b -> a, c -> a) -> Either b c -> a
+tup2Either (f, _) (Left b) = f b
+tup2Either (_, g) (Right c) = g c
+
+either2Tup :: (Either b c -> a) -> (b -> a, c -> a)
+either2Tup f = (f . Left, f . Right)
diff --git a/ch01_01.4-iii.hs b/ch01_01.4-iii.hs
new file mode 100644
index 0000000..78885aa
--- /dev/null
+++ b/ch01_01.4-iii.hs
@@ -0,0 +1,14 @@
+-- Exercise 1.4-iii
+-- Prove `(a * b)^c == a^c * b*c`.
+func2Tup :: (c -> (a, b)) -> (c -> a, c -> b)
+func2Tup f = (fst . f, snd . f)
+
+-- This version takes in a tuple of functions, which is equivalent to them
+-- being separate arguments:
+tup2Func :: (c -> a, c -> b) -> c -> (a, b)
+tup2Func (f, g) v = (f v, g v)
+
+-- This version has the same signature as Sandy's version, and calls `curry`
+-- against my tupled rendition above:
+tup2Func' :: (c -> a) -> (c -> b) -> c -> (a, b)
+tup2Func' = curry tup2Func
diff --git a/ch02_02.4-i.hs b/ch02_02.4-i.hs
new file mode 100644
index 0000000..a311096
--- /dev/null
+++ b/ch02_02.4-i.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE DataKinds #-}
+
+-- Exercise 2.4-i
+-- Write a closed type family to compute `Not`.
+
+-- I use my own boolean data type and generated kinds. But it's the same as
+-- just using plain `Bool`:
+data MyBool
+  = MyTrue
+  | False
+
+type family Not (x :: MyBool) :: MyBool where
+  Not 'MyTrue = 'MyFalse
+  Not 'MyFalse = 'MyTrue
diff --git a/ch03_03-i.hs b/ch03_03-i.hs
new file mode 100644
index 0000000..ec12e08
--- /dev/null
+++ b/ch03_03-i.hs
@@ -0,0 +1,25 @@
+-- Exercise 3-i
+-- Which of these types are `Functor`s? Give instances for the ones that are.
+
+-- `T1` is a `Functor`:
+newtype T1 a
+  = T1 (Int -> a)
+
+instance Functor T1 where
+  fmap f (T1 g) = T1 $ f <$> g
+
+newtype T2 a
+  = T2 (a -> Int)
+
+newtype T3 a
+  = T3 (a -> a)
+
+newtype T4 a
+  = T4 ((Int -> a) -> Int)
+
+-- `T5` is a `Functor`:
+newtype T5 a
+  = T5 ((a -> Int) -> Int)
+
+instance Functor T5 where
+  fmap f (T5 g) = T5 $ \f' -> g $ f' . f
diff --git a/ch05_05.3-i_ii.hs b/ch05_05.3-i_ii.hs
new file mode 100644
index 0000000..3d73229
--- /dev/null
+++ b/ch05_05.3-i_ii.hs
@@ -0,0 +1,34 @@
+import Data.Kind
+
+data HList (ts :: [Type]) where
+  HNil :: HList '[]
+  (:#) :: t -> HList ts -> HList (t ': ts)
+
+infixr 5 :#
+
+instance Eq (HList '[]) where
+  HNil == HNil = True
+
+instance (Eq t, Eq (HList ts)) => Eq (HList (t ': ts)) where
+  (a :# as) == (b :# bs) = a == b && as == bs
+
+-- Exercise 5.3-i
+-- Implement `Ord` for `HList`:
+instance Ord (HList '[]) where
+  compare HNil HNil = EQ
+
+-- I always forget `Ord` is a monoid. This version is less elegant, but works
+-- just as well as Sandy's:
+instance (Ord t, Ord (HList ts)) => Ord (HList (t ': ts)) where
+  compare (a :# as) (b :# bs) =
+    case compare a b of
+      EQ -> compare as bs
+      other -> other
+
+-- Exercise 5.3-ii
+-- Implement `Show` for `HList`:
+instance Show (HList '[]) where
+  show HNil = "HNil"
+
+instance (Show t, Show (HList ts)) => Show (HList (t ': ts)) where
+  show (a :# as) = show a <> " :# " <> show as
diff --git a/ch05_05.3-iii.hs b/ch05_05.3-iii.hs
new file mode 100644
index 0000000..b1c0865
--- /dev/null
+++ b/ch05_05.3-iii.hs
@@ -0,0 +1,25 @@
+import Data.Kind
+
+data HList (ts :: [Type]) where
+  HNil :: HList '[]
+  (:#) :: t -> HList ts -> HList (t ': ts)
+
+infixr 5 :#
+
+type family All (c :: Type -> Constraint) (ts :: [Type]) :: Constraint where
+  All c '[] = ()
+  All c (t ': ts) = (c t, All c ts)
+
+instance All Eq ts => Eq (HList ts) where
+  HNil == HNil = True
+  (a :# as) == (b :# bs) = a == b && as == bs
+
+-- Exercise 5.3-iii
+-- Rewrite the `Ord` and `Show` instances in terms of `All`:
+instance (All Eq ts, All Ord ts) => Ord (HList ts) where
+  compare HNil HNil = EQ
+  compare (a :# as) (b :# bs) = compare a b <> compare as bs
+
+instance All Show ts => Show (HList ts) where
+  show HNil = "HNil"
+  show (a :# as) = show a <> " :# " <> show as
diff --git a/ch06_06.4-i_ii_iii.hs b/ch06_06.4-i_ii_iii.hs
new file mode 100644
index 0000000..13a4fa3
--- /dev/null
+++ b/ch06_06.4-i_ii_iii.hs
@@ -0,0 +1,42 @@
+newtype Cont a = Cont
+  { unCont :: forall r. (a -> r) -> r
+  }
+
+-- I could not figure out `Functor`. After peeking Sandy's solution I was able
+-- to figure out `Applicative`, but failed miserably with `Monad`. I added
+-- annotations on the types of all the terms on my attempt to figure it out.
+
+-- Exercise 6.4-i
+-- Provide a `Functor` instance for `Cont`.
+instance Functor Cont where
+  -- fmap      :: (a -> b) -> Cont a -> Cont b
+  -- f         :: a -> b
+  -- a         :: (a -> r) -> r
+  -- c         :: b -> r
+  -- c . f     :: a -> r
+  -- a $ c . f :: r
+  fmap f (Cont a) = Cont $ \c -> a $ c . f
+
+-- Exercise 6.4-ii
+-- Provide a `Applicative` instances for `Cont`.
+instance Applicative Cont where
+  pure a = Cont $ \c -> c a
+
+  -- (<*>) :: Cont (a -> b) -> Cont a -> Cont b
+  -- f     :: ((a -> b) -> r) -> r
+  -- a     :: (a -> r) -> r
+  -- c     :: b -> r
+  -- c'    :: a -> b
+  Cont f <*> Cont a = Cont $ \c -> f $ \c' -> a $ c . c'
+
+-- Exercise 6.4-iii
+-- Provide a `Monad` instances for `Cont`.
+instance Monad Cont where
+  -- (>>=)      :: Cont a -> (a -> Cont b) -> Cont b
+  -- a          :: (a -> r) -> r
+  -- b          :: (b -> r) -> r
+  -- f          :: a -> Cont b
+  -- unCont . f :: a -> (b -> r) -> r
+  -- c          :: b -> r
+  -- c'         :: a
+  Cont a >>= f = Cont $ \c -> a $ \c' -> unCont (f c') c
diff --git a/ch06_06.4-iv.hs b/ch06_06.4-iv.hs
new file mode 100644
index 0000000..205606a
--- /dev/null
+++ b/ch06_06.4-iv.hs
@@ -0,0 +1,15 @@
+-- Exercise 6.4-iv
+-- There is also a monad transformer version of `Cont`. Implement it.
+newtype ContT t a = ContT
+  { unContT :: forall r. (a -> t r) -> t r
+  }
+
+instance Functor (ContT t) where
+  fmap f (ContT a) = ContT $ \c -> a $ c . f
+
+instance Applicative (ContT t) where
+  pure a = ContT $ \c -> c a
+  ContT f <*> ContT a = ContT $ \c -> f $ \c' -> a $ c . c'
+
+instance Monad (ContT t) where
+  ContT a >>= f = ContT $ \c -> a $ \c' -> unContT (f c') c
diff --git a/ch07_07.1-ii.hs b/ch07_07.1-ii.hs
new file mode 100644
index 0000000..91abc8d
--- /dev/null
+++ b/ch07_07.1-ii.hs
@@ -0,0 +1,14 @@
+-- Exercise 7.1-ii
+-- What happens to this instance if you remove the `Show t =>` constraint from
+-- `HasShow`.
+
+-- Removing `Show t =>` below makes GHC angry:
+--
+-- • No instance for ‘Show t’ arising from a use of ‘show’
+--   Possible fix:
+--     add (Show t) to the context of the data constructor ‘HasShow’
+data HasShow where
+  HasShow :: Show t => t -> HasShow
+
+instance Show HasShow where
+  show (HasShow t) = "HasShow " <> show t
diff --git a/ch07_07.1-iii.hs b/ch07_07.1-iii.hs
new file mode 100644
index 0000000..1285fd9
--- /dev/null
+++ b/ch07_07.1-iii.hs
@@ -0,0 +1,11 @@
+-- Exercise 7.1-iii
+-- Write the `Show` instance for `HasShow` in terms of `elimHasShow`.
+data HasShow where
+  HasShow :: Show t => t -> HasShow
+
+elimHasShow :: (forall a. Show a => a -> r) -> HasShow -> r
+elimHasShow f (HasShow a) = f a
+
+-- This version also prepends the `HasShow` name to the result of `show`:
+instance Show HasShow where
+  show = mappend "HasShow " . elimHasShow show
diff --git a/ch09_09.2.example.hs b/ch09_09.2.example.hs
new file mode 100644
index 0000000..bcecf7a
--- /dev/null
+++ b/ch09_09.2.example.hs
@@ -0,0 +1,33 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+
+import Data.Kind (Type)
+import Data.Proxy (Proxy (Proxy))
+import GHC.TypeLits (KnownSymbol, Symbol, symbolVal)
+
+data (a :: k1) :<< (b :: k2)
+
+infixr 5 :<<
+
+class HasPrintf a where
+  type Printf a :: Type
+  format :: String -> Proxy a -> Printf a
+
+instance KnownSymbol text => HasPrintf (text :: Symbol) where
+  type Printf text = String
+  format s _ = s <> symbolVal (Proxy @text)
+
+instance (HasPrintf a, KnownSymbol text) => HasPrintf ((text :: Symbol) :<< a) where
+  type Printf (text :<< a) = Printf a
+  format s _ = format (s <> symbolVal (Proxy @text)) (Proxy @a)
+
+instance (HasPrintf a, Show param) => HasPrintf ((param :: Type) :<< a) where
+  type Printf (param :<< a) = param -> Printf a
+  format s _ param = format (s <> show param) (Proxy @a)
+
+instance {-# OVERLAPPING #-} HasPrintf a => HasPrintf (String :<< a) where
+  type Printf (String :<< a) = String -> Printf a
+  format s _ param = format (s <> param) (Proxy @a)
+
+printf :: HasPrintf a => Proxy a -> Printf a
+printf = format ""
diff --git a/ch10_10.0.example.hs b/ch10_10.0.example.hs
new file mode 100644
index 0000000..2ab1d84
--- /dev/null
+++ b/ch10_10.0.example.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+
+import Data.Kind (Type)
+
+type Exp a = a -> Type
+
+type family Eval (e :: Exp a) :: a
+
+data Fst :: (a, b) -> Exp a
+
+data Snd :: (a, b) -> Exp b
+
+type instance Eval (Fst '(a, b)) = a
+
+type instance Eval (Snd '(a, b)) = b
diff --git a/ch10_10.1-i.hs b/ch10_10.1-i.hs
new file mode 100644
index 0000000..d76160f
--- /dev/null
+++ b/ch10_10.1-i.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE FunctionalDependencies #-}
+
+-- Exercise 10.1-i
+-- Defunctionalize `listToMaybe :: [a] -> Maybe a`.
+newtype ListToMaybe a = ListToMaybe [a]
+
+class Eval l t | l -> t where
+  eval :: l -> t
+
+instance Eval (ListToMaybe a) (Maybe a) where
+  eval (ListToMaybe []) = Nothing
+  eval (ListToMaybe (x : _)) = Just x
diff --git a/ch10_10.2-i.hs b/ch10_10.2-i.hs
new file mode 100644
index 0000000..a8f1d20
--- /dev/null
+++ b/ch10_10.2-i.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+
+-- Exercise 10.2-i
+-- Defunctionalize `listToMaybe` at the type-level.
+
+import Data.Kind (Type)
+
+type Exp a = a -> Type
+
+type family Eval (e :: Exp a) :: a
+
+data ListToMaybe :: [a] -> Exp (Maybe a)
+
+type instance Eval (ListToMaybe '[]) = 'Nothing
+
+type instance Eval (ListToMaybe (x ': _)) = 'Just x
diff --git a/ch10_10.2-ii.hs b/ch10_10.2-ii.hs
new file mode 100644
index 0000000..d8b1275
--- /dev/null
+++ b/ch10_10.2-ii.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- Exercise 10.2-ii
+-- Defunctionalize `foldr :: (a -> b -> b) -> b -> [a] -> b`.
+
+import Data.Kind (Type)
+
+type Exp a = a -> Type
+
+type family Eval (e :: Exp a) :: a
+
+data Foldr :: (a -> b -> Exp b) -> b -> [a] -> Exp b
+
+type instance Eval (Foldr f z '[]) = z
+
+type instance Eval (Foldr f z (x ': xs)) = Eval (f x (Eval (Foldr f z xs)))
diff --git a/ch10_10.4-i.hs b/ch10_10.4-i.hs
new file mode 100644
index 0000000..3e7606a
--- /dev/null
+++ b/ch10_10.4-i.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+
+-- Exercise 10.4-i
+-- Write a promoted functor instance for tuples.
+
+import Data.Kind (Type)
+
+type Exp a = a -> Type
+
+type family Eval (e :: Exp a) :: a
+
+data Map :: (a -> Exp b) -> f a -> Exp (f b)
+
+type instance Eval (Map f '(a, b)) = '(a, Eval (f b))
diff --git a/ch11_11.2-i.hs b/ch11_11.2-i.hs
new file mode 100644
index 0000000..ab9b0c2
--- /dev/null
+++ b/ch11_11.2-i.hs
@@ -0,0 +1,49 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+
+import Data.Functor.Identity (Identity (Identity))
+import Data.Kind (Type)
+import Data.Proxy (Proxy (Proxy))
+import Fcf (Eval, FindIndex, FromMaybe, Stuck, TyEq, type (=<<))
+import GHC.TypeLits (KnownNat, natVal)
+import Unsafe.Coerce (unsafeCoerce)
+
+data OpenSum (f :: k -> Type) (ts :: [k]) where
+  UnsafeOpenSum :: Int -> f t -> OpenSum f ts
+
+type FindElem (key :: k) (ts :: [k]) =
+  FromMaybe Stuck =<< FindIndex (TyEq key) ts
+
+type Member t ts =
+  KnownNat (Eval (FindElem t ts))
+
+findElem :: forall t ts. Member t ts => Int
+findElem = fromIntegral $ natVal $ Proxy @(Eval (FindElem t ts))
+
+inject :: forall f t ts. Member t ts => f t -> OpenSum f ts
+inject = UnsafeOpenSum $ findElem @t @ts
+
+project :: forall f t ts. Member t ts => OpenSum f ts -> Maybe (f t)
+project (UnsafeOpenSum i f) =
+  if i == findElem @t @ts
+    then Just $ unsafeCoerce f
+    else Nothing
+
+decompose :: OpenSum f (t ': ts) -> Either (f t) (OpenSum f ts)
+decompose (UnsafeOpenSum 0 t) = Left $ unsafeCoerce t
+decompose (UnsafeOpenSum n t) = Right $ UnsafeOpenSum (n - 1) t
+
+-- Exercise 11.2-i
+-- Write `weaken :: OpenSum f ts -> OpenSum f (x ': ts)`.
+weaken :: OpenSum f ts -> OpenSum f (x ': ts)
+weaken (UnsafeOpenSum n t) = UnsafeOpenSum (n + 1) t
+
+-- Example usage:
+type SumTypes = '[Bool, Int]
+
+osum1 :: OpenSum Identity SumTypes
+osum1 = inject (Identity True)
+
+projVal :: Maybe (Identity Bool)
+projVal = project osum1
diff --git a/ch11_11.3-i_ii.hs b/ch11_11.3-i_ii.hs
new file mode 100644
index 0000000..20867f9
--- /dev/null
+++ b/ch11_11.3-i_ii.hs
@@ -0,0 +1,123 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+
+import Data.Kind (Type)
+import Data.Proxy (Proxy (Proxy))
+import Data.Vector (Vector, cons, empty, ifilter, unsafeIndex, (//))
+import Fcf qualified as F
+import Fcf.Data.List qualified as F (Cons)
+import Fcf.Data.Nat qualified as F (Nat)
+import GHC.OverloadedLabels (IsLabel, fromLabel)
+import GHC.TypeLits (KnownNat, Symbol, natVal)
+import Unsafe.Coerce (unsafeCoerce)
+
+data Any (f :: k -> Type) where
+  Any :: f t -> Any f
+
+data OpenProduct (f :: k -> Type) (ts :: [(Symbol, k)]) where
+  OpenProduct :: Vector (Any f) -> OpenProduct f ts
+
+type UniqueKey (key :: k) (ts :: [(k, t)]) =
+  F.Null F.=<< F.Filter (F.TyEq key F.<=< F.Fst) ts
+
+type FindIndex (key :: Symbol) (ts :: [(Symbol, k)]) =
+  F.FindIndex (F.TyEq key F.<=< F.Fst) ts
+
+type FindElem (key :: Symbol) (ts :: [(Symbol, k)]) =
+  F.Eval (F.FromMaybe F.Stuck F.=<< FindIndex key ts)
+
+type LookupType (key :: k) (ts :: [(k, t)]) =
+  F.FromMaybe F.Stuck F.=<< F.Lookup key ts
+
+type UpdateElem (key :: Symbol) (t :: k) (ts :: [(Symbol, k)]) =
+  F.SetIndex (FindElem key ts) '(key, t) ts
+
+type DeleteElem (key :: Symbol) (ts :: [(Symbol, k)]) =
+  F.Filter (F.Not F.<=< F.TyEq key F.<=< F.Fst) ts
+
+type UpsertElem (key :: Symbol) (t :: k) (ts :: [(Symbol, k)]) =
+  F.UnMaybe
+    (F.Cons '(key, t) ts)
+    (F.ConstFn (F.Eval (UpdateElem key t ts)))
+    F.=<< FindIndex key ts
+
+data Key (key :: Symbol) = Key
+
+instance key ~ key' => IsLabel key (Key key') where
+  fromLabel = Key
+
+class MaybeIndex (m :: Maybe F.Nat) where
+  maybeIndex :: Maybe Int
+
+instance MaybeIndex 'Nothing where
+  maybeIndex = Nothing
+
+instance KnownNat a => MaybeIndex ('Just a) where
+  maybeIndex = Just $ fromIntegral $ natVal $ Proxy @a
+
+nil :: OpenProduct f '[]
+nil = OpenProduct empty
+
+insert
+  :: F.Eval (UniqueKey key ts) ~ 'True
+  => Key key
+  -> f t
+  -> OpenProduct f ts
+  -> OpenProduct f ('(key, t) ': ts)
+insert _ ft (OpenProduct v) = OpenProduct $ cons (Any ft) v
+
+findElem
+  :: forall key ts
+   . KnownNat (FindElem key ts)
+  => Int
+findElem = fromIntegral $ natVal $ Proxy @(FindElem key ts)
+
+get
+  :: forall key ts f
+   . KnownNat (FindElem key ts)
+  => Key key
+  -> OpenProduct f ts
+  -> f (F.Eval (LookupType key ts))
+get _ (OpenProduct v) = unAny $ unsafeIndex v $ findElem @key @ts
+ where
+  unAny (Any a) = unsafeCoerce a
+
+update
+  :: forall key ts t f
+   . KnownNat (FindElem key ts)
+  => Key key
+  -> f t
+  -> OpenProduct f ts
+  -> OpenProduct f (F.Eval (UpdateElem key t ts))
+update _ ft (OpenProduct v) = OpenProduct $ v // [(findElem @key @ts, Any ft)]
+
+-- Exercise 11.3-i
+-- Implement `delete` for `OpenProduct`s.
+
+-- This one works identically to Sandy's version:
+delete
+  :: forall key ts f
+   . KnownNat (FindElem key ts)
+  => Key key
+  -> OpenProduct f ts
+  -> OpenProduct f (F.Eval (DeleteElem key ts))
+delete _ (OpenProduct v) = OpenProduct $ flip ifilter v $ curry $ (findElem @key @ts ==) . fst
+
+-- Exercise 11.3-ii
+-- Implement `upsert` for `OpenProduct`s.
+
+-- I came up with slightly different (but equivalent) helper data-types and
+-- type families (see above).
+upsert
+  :: forall key ts t f
+   . MaybeIndex (F.Eval (FindIndex key ts))
+  => Key key
+  -> f t
+  -> OpenProduct f ts
+  -> OpenProduct f (F.Eval (UpsertElem key t ts))
+upsert _ ft (OpenProduct v) =
+  case maybeIndex @(F.Eval (FindIndex key ts)) of
+    Nothing -> OpenProduct $ cons (Any ft) v
+    Just i -> OpenProduct $ v // [(i, Any ft)]
diff --git a/ch12_12.i.hs b/ch12_12.i.hs
new file mode 100644
index 0000000..cf3ddcf
--- /dev/null
+++ b/ch12_12.i.hs
@@ -0,0 +1,168 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE TypeFamilies #-}
+
+import Data.Kind (Constraint, Type)
+import Data.Proxy (Proxy (Proxy))
+import Data.Vector (Vector, cons, empty, ifilter, unsafeIndex, (//))
+import Fcf qualified as F
+import Fcf.Data.List qualified as F (Cons)
+import Fcf.Data.Nat qualified as F (Nat)
+import GHC.OverloadedLabels (IsLabel, fromLabel)
+import GHC.TypeLits qualified as T
+import Unsafe.Coerce (unsafeCoerce)
+
+data Any (f :: k -> Type) where
+  Any :: f t -> Any f
+
+data OpenProduct (f :: k -> Type) (ts :: [(T.Symbol, k)]) where
+  OpenProduct :: Vector (Any f) -> OpenProduct f ts
+
+type UniqueKey (key :: k) (ts :: [(k, t)]) =
+  F.Null F.=<< F.Filter (F.TyEq key F.<=< F.Fst) ts
+
+type family
+  RequireUniqueKey
+    (result :: Bool)
+    (key :: T.Symbol)
+    (t :: k)
+    (ts :: [(T.Symbol, k)])
+    :: Constraint
+  where
+  RequireUniqueKey 'True key t ts = ()
+  RequireUniqueKey 'False key t ts =
+    T.TypeError
+      ( 'T.Text "Attempting to add a field named `"
+          'T.:<>: 'T.Text key
+          'T.:<>: 'T.Text "' with type "
+          'T.:<>: 'T.ShowType t
+          'T.:<>: 'T.Text " to an OpenProduct."
+          'T.:$$: 'T.Text "But the OpenProduct already has a field `"
+            'T.:<>: 'T.Text key
+            'T.:<>: 'T.Text "' with type "
+            'T.:<>: 'T.ShowType (F.Eval (LookupType key ts))
+          'T.:$$: 'T.Text "Consider using `update' instead of `insert'."
+      )
+
+type FindIndex (key :: T.Symbol) (ts :: [(T.Symbol, k)]) =
+  F.FindIndex (F.TyEq key F.<=< F.Fst) ts
+
+-- Exercise 12-i
+-- Add helpful type errors to `OpenProduct`'s `update` and `delete` functions.
+
+-- My take is a bit different than Sandy's solution. `FindElemWithBase`
+-- generalizes element finding, so we can re-implement the original `FindElem`
+-- (which gets stuck) plus a new `FindElemDuring` (which provides the helpful
+-- error message) using it.
+type FindElemWithBase (key :: T.Symbol) (ts :: [(T.Symbol, k)]) (base :: T.Nat) =
+  F.Eval (F.FromMaybe base F.=<< FindIndex key ts)
+
+type FindElem (key :: T.Symbol) (ts :: [(T.Symbol, k)]) =
+  FindElemWithBase key ts F.Stuck
+
+type FindElemDuring (action :: T.Symbol) (key :: T.Symbol) (ts :: [(T.Symbol, k)]) =
+  FindElemWithBase
+    key
+    ts
+    ( T.TypeError
+        ( 'T.Text "Attempting to "
+            'T.:<>: 'T.Text action
+            'T.:<>: 'T.Text " a field named `"
+            'T.:<>: 'T.Text key
+            'T.:<>: 'T.Text "' in an OpenProduct."
+            'T.:$$: 'T.Text "But the OpenProduct does not have a field `"
+              'T.:<>: 'T.Text key
+              'T.:<>: 'T.Text "'."
+        )
+    )
+
+type FindableDuring action key ts =
+  ( T.KnownNat (FindElemDuring action key ts)
+  , T.KnownNat (FindElem key ts)
+  )
+
+type LookupType (key :: k) (ts :: [(k, t)]) =
+  F.FromMaybe F.Stuck F.=<< F.Lookup key ts
+
+type UpdateElem (key :: T.Symbol) (t :: k) (ts :: [(T.Symbol, k)]) =
+  F.SetIndex (FindElem key ts) '(key, t) ts
+
+type DeleteElem (key :: T.Symbol) (ts :: [(T.Symbol, k)]) =
+  F.Filter (F.Not F.<=< F.TyEq key F.<=< F.Fst) ts
+
+type UpsertElem (key :: T.Symbol) (t :: k) (ts :: [(T.Symbol, k)]) =
+  F.UnMaybe
+    (F.Cons '(key, t) ts)
+    (F.ConstFn (F.Eval (UpdateElem key t ts)))
+    F.=<< FindIndex key ts
+
+data Key (key :: T.Symbol) = Key
+
+instance key ~ key' => IsLabel key (Key key') where
+  fromLabel = Key
+
+class MaybeIndex (m :: Maybe F.Nat) where
+  maybeIndex :: Maybe Int
+
+instance MaybeIndex 'Nothing where
+  maybeIndex = Nothing
+
+instance T.KnownNat a => MaybeIndex ('Just a) where
+  maybeIndex = Just $ fromIntegral $ T.natVal $ Proxy @a
+
+nil :: OpenProduct f '[]
+nil = OpenProduct empty
+
+insert
+  :: RequireUniqueKey (F.Eval (UniqueKey key ts)) key t ts
+  => Key key
+  -> f t
+  -> OpenProduct f ts
+  -> OpenProduct f ('(key, t) ': ts)
+insert _ ft (OpenProduct v) = OpenProduct $ cons (Any ft) v
+
+findElem
+  :: forall key ts
+   . T.KnownNat (FindElem key ts)
+  => Int
+findElem = fromIntegral $ T.natVal $ Proxy @(FindElem key ts)
+
+get
+  :: forall key ts f
+   . FindableDuring "get" key ts
+  => Key key
+  -> OpenProduct f ts
+  -> f (F.Eval (LookupType key ts))
+get _ (OpenProduct v) = unAny $ unsafeIndex v $ findElem @key @ts
+ where
+  unAny (Any a) = unsafeCoerce a
+
+update
+  :: forall key ts t f
+   . FindableDuring "update" key ts
+  => Key key
+  -> f t
+  -> OpenProduct f ts
+  -> OpenProduct f (F.Eval (UpdateElem key t ts))
+update _ ft (OpenProduct v) = OpenProduct $ v // [(findElem @key @ts, Any ft)]
+
+delete
+  :: forall key ts f
+   . FindableDuring "delete" key ts
+  => Key key
+  -> OpenProduct f ts
+  -> OpenProduct f (F.Eval (DeleteElem key ts))
+delete _ (OpenProduct v) = OpenProduct $ flip ifilter v $ curry $ (findElem @key @ts ==) . fst
+
+upsert
+  :: forall key ts t f
+   . MaybeIndex (F.Eval (FindIndex key ts))
+  => Key key
+  -> f t
+  -> OpenProduct f ts
+  -> OpenProduct f (F.Eval (UpsertElem key t ts))
+upsert _ ft (OpenProduct v) =
+  case maybeIndex @(F.Eval (FindIndex key ts)) of
+    Nothing -> OpenProduct $ cons (Any ft) v
+    Just i -> OpenProduct $ v // [(i, Any ft)]
diff --git a/ch12_12.ii.hs b/ch12_12.ii.hs
new file mode 100644
index 0000000..eb4dd2b
--- /dev/null
+++ b/ch12_12.ii.hs
@@ -0,0 +1,83 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+
+import Data.Functor.Identity (Identity (Identity))
+import Data.Kind (Type)
+import Data.Proxy (Proxy (Proxy))
+import Fcf (Eval, FindIndex, FromMaybe, Stuck, TyEq, type (=<<))
+import GHC.TypeLits (ErrorMessage (ShowType, Text, (:$$:), (:<>:)), KnownNat, TypeError, natVal)
+import Unsafe.Coerce (unsafeCoerce)
+
+data OpenSum (f :: k -> Type) (ts :: [k]) where
+  UnsafeOpenSum :: Int -> f t -> OpenSum f ts
+
+type FindElem (key :: k) (ts :: [k]) =
+  FromMaybe Stuck =<< FindIndex (TyEq key) ts
+
+-- Exercise 12-ii
+-- Write a closed type family of kind `[k] -> ErrorMessage` that pretty prints
+-- a list. Use it to improve the error message from `FriendlyFindElem`.
+
+-- Here Sandy gives an equation for the intermediate pattern `(t ': '[])`. I
+-- don't. Even so, recursion seems to work just fine up to the base case of
+-- the empty list.
+type family PrettyList (ts :: [k]) where
+  PrettyList '[] = 'Text ""
+  PrettyList (t ': ts) = 'Text " :: " ':<>: 'ShowType t ':$$: PrettyList ts
+
+type family FriendlyFindElem (f :: k -> Type) (t :: k) (ts :: [k]) where
+  FriendlyFindElem f t ts =
+    FromMaybe
+      ( TypeError
+          ( 'Text "Attempted to call 'friendlyProject' to produce a `"
+              ':<>: 'ShowType (f t)
+              ':<>: 'Text "'."
+              ':$$: 'Text "But the OpenSum can only contain one of: "
+              ':$$: PrettyList ts
+          )
+      )
+      =<< FindIndex (TyEq t) ts
+
+type Member t ts =
+  KnownNat (Eval (FindElem t ts))
+
+findElem :: forall t ts. Member t ts => Int
+findElem = fromIntegral $ natVal $ Proxy @(Eval (FindElem t ts))
+
+inject :: forall f t ts. Member t ts => f t -> OpenSum f ts
+inject = UnsafeOpenSum $ findElem @t @ts
+
+project :: forall f t ts. Member t ts => OpenSum f ts -> Maybe (f t)
+project (UnsafeOpenSum i f) =
+  if i == findElem @t @ts
+    then Just $ unsafeCoerce f
+    else Nothing
+
+friendlyProject
+  :: forall f t ts
+   . ( KnownNat (Eval (FriendlyFindElem f t ts))
+     , Member t ts
+     )
+  => OpenSum f ts
+  -> Maybe (f t)
+friendlyProject (UnsafeOpenSum i f) =
+  if i == findElem @t @ts
+    then Just $ unsafeCoerce f
+    else Nothing
+
+decompose :: OpenSum f (t ': ts) -> Either (f t) (OpenSum f ts)
+decompose (UnsafeOpenSum 0 t) = Left $ unsafeCoerce t
+decompose (UnsafeOpenSum n t) = Right $ UnsafeOpenSum (n - 1) t
+
+weaken :: OpenSum f ts -> OpenSum f (x ': ts)
+weaken (UnsafeOpenSum n t) = UnsafeOpenSum (n + 1) t
+
+-- usage example
+type SumTypes = '[Bool, Int]
+
+osum1 :: OpenSum Identity SumTypes
+osum1 = inject (Identity True)
+
+projVal :: Maybe (Identity Bool)
+projVal = project osum1
diff --git a/ch13_13.2-i.hs b/ch13_13.2-i.hs
new file mode 100644
index 0000000..acce2b2
--- /dev/null
+++ b/ch13_13.2-i.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE ImportQualifiedPost #-}
+
+-- Exercise 13.2-i
+-- Provide a generic instance for the `Ord` class.
+
+import GHC.Generics qualified as G
+
+class GOrd a where
+  gcompare :: a x -> a x -> Ordering
+
+instance GOrd G.U1 where
+  gcompare G.U1 G.U1 = EQ
+
+instance GOrd G.V1 where
+  gcompare _ _ = EQ
+
+instance Ord a => GOrd (G.K1 _1 a) where
+  gcompare (G.K1 a) (G.K1 b) = compare a b
+
+instance (GOrd a, GOrd b) => GOrd (a G.:+: b) where
+  gcompare (G.L1 a1) (G.L1 a2) = gcompare a1 a2
+  gcompare (G.R1 b1) (G.R1 b2) = gcompare b1 b2
+  gcompare (G.L1 _) (G.R1 _) = LT
+  gcompare (G.R1 _) (G.L1 _) = GT
+
+instance (GOrd a, GOrd b) => GOrd (a G.:*: b) where
+  -- Don't forget `Ord` is a monoid! :)
+  gcompare (a1 G.:*: b1) (a2 G.:*: b2) = gcompare a1 a2 <> gcompare b1 b2
+
+instance GOrd a => GOrd (G.M1 _x _y a) where
+  gcompare (G.M1 a1) (G.M1 a2) = gcompare a1 a2
+
+genericCompare :: (G.Generic a, GOrd (G.Rep a)) => a -> a -> Ordering
+genericCompare a b = gcompare (G.from a) (G.from b)
+
+-- Example usage:
+data Foo a b c = F0 | F1 a | F2 b c deriving (Eq, G.Generic)
+
+instance (Ord a, Ord b, Ord c) => Ord (Foo a b c) where
+  compare = genericCompare
diff --git a/ch13_13.2-ii.hs b/ch13_13.2-ii.hs
new file mode 100644
index 0000000..7f1a494
--- /dev/null
+++ b/ch13_13.2-ii.hs
@@ -0,0 +1,47 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+
+-- Exercise 13.2-ii
+-- Use `GHC.Generics` to implement the function `exNihilo :: Maybe a`.
+
+import GHC.Generics qualified as G
+
+class GExNihilo a where
+  gexNihilo :: Maybe (a x)
+
+instance GExNihilo G.U1 where
+  gexNihilo = Just G.U1
+
+instance GExNihilo G.V1 where
+  gexNihilo = Nothing
+
+instance GExNihilo (G.K1 _1 a) where
+  gexNihilo = Nothing
+
+instance GExNihilo (a G.:+: b) where
+  gexNihilo = Nothing
+
+instance GExNihilo (a G.:*: b) where
+  gexNihilo = Nothing
+
+instance GExNihilo a => GExNihilo (G.M1 _x _y a) where
+  gexNihilo = G.M1 <$> gexNihilo
+
+-- I could not figure this one out so had to look at the solution. I noticed
+-- Sandy missed to provide the actual implementation of `exNihilo` so here is
+-- my version:
+exNihilo :: forall a. (G.Generic a, GExNihilo (G.Rep a)) => Maybe a
+exNihilo = G.to <$> gexNihilo @(G.Rep a)
+
+-- Example usage:
+data MyUnit = MyUnit deriving (G.Generic, Show)
+
+newtype MyType a = MyType a deriving (G.Generic, Show)
+
+data MySum = MySum1 | MySum2 deriving (G.Generic, Show)
+
+t1 = exNihilo @MyUnit -- Just MyUnit
+
+t2 = exNihilo @(MyType ()) -- Nothing
+
+t3 = exNihilo @MySum -- Nothing
diff --git a/ch13_13.3.example.hs b/ch13_13.3.example.hs
new file mode 100644
index 0000000..1c00acc
--- /dev/null
+++ b/ch13_13.3.example.hs
@@ -0,0 +1,136 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+import Control.Monad.Writer (Writer, runWriter, tell)
+import Data.Aeson (Value (Array, Object, String), object, (.=))
+import Data.Aeson.Encode.Pretty (encodePretty)
+import Data.Aeson.Key (fromString)
+import Data.ByteString.Lazy.Char8 qualified as LC8
+import Data.Kind (Type)
+import Data.Proxy (Proxy (Proxy))
+import Data.Text (Text, pack)
+import Data.Vector (fromList)
+import GHC.Generics (C, D, D1, Generic, K1, M1, Meta (MetaData, MetaSel), Rep, S, (:*:), (:+:))
+import GHC.TypeLits (ErrorMessage (Text), KnownSymbol, Symbol, TypeError, symbolVal)
+
+class GSchema (a :: Type -> Type) where
+  gschema :: Writer [Text] Value
+
+mergeObjects :: Value -> Value -> Value
+mergeObjects (Object a) (Object b) = Object $ a <> b
+
+emitRequired :: forall nm. KnownSymbol nm => Writer [Text] ()
+emitRequired = tell . pure . pack . symbolVal $ Proxy @nm
+
+type family RepName (x :: Type -> Type) :: Symbol where
+  RepName (D1 ('MetaData nm _ _ _) _) = nm
+
+type family TypeName (t :: Type) :: Symbol where
+  TypeName t = RepName (Rep t)
+
+type family ToJSONType (a :: Type) :: Symbol where
+  ToJSONType Int = "integer"
+  ToJSONType Integer = "integer"
+  ToJSONType Float = "number"
+  ToJSONType Double = "number"
+  ToJSONType String = "string"
+  ToJSONType Bool = "boolean"
+  ToJSONType [a] = "array"
+  ToJSONType a = TypeName a
+
+makeTypeObj :: forall a. KnownSymbol (ToJSONType a) => Value
+makeTypeObj = object ["type" .= String (pack $ symbolVal $ Proxy @(ToJSONType a))]
+
+makePropertyObj :: forall name. KnownSymbol name => Value -> Value
+makePropertyObj v = object [fromString (symbolVal $ Proxy @name) .= v]
+
+instance
+  ( KnownSymbol nm
+  , KnownSymbol (ToJSONType a)
+  )
+  => GSchema (M1 S ('MetaSel ('Just nm) _1 _2 _3) (K1 _4 a))
+  where
+  gschema = do
+    emitRequired @nm
+    return $ makePropertyObj @nm $ makeTypeObj @a
+  {-# INLINE gschema #-}
+
+instance
+  {-# OVERLAPPING #-}
+  ( KnownSymbol nm
+  , KnownSymbol (ToJSONType a)
+  )
+  => GSchema (M1 S ('MetaSel ('Just nm) _1 _2 _3) (K1 _4 (Maybe a)))
+  where
+  gschema = return $ makePropertyObj @nm $ makeTypeObj @a
+  {-# INLINE gschema #-}
+
+instance
+  {-# OVERLAPPING #-}
+  ( KnownSymbol nm
+  , KnownSymbol (ToJSONType [a])
+  , KnownSymbol (ToJSONType a)
+  )
+  => GSchema (M1 S ('MetaSel ('Just nm) _1 _2 _3) (K1 _4 [a]))
+  where
+  gschema = do
+    emitRequired @nm
+    return $ makePropertyObj @nm $ mergeObjects innerType $ makeTypeObj @[a]
+   where
+    innerType = object ["items" .= makeTypeObj @a]
+  {-# INLINE gschema #-}
+
+instance
+  {-# OVERLAPPING #-}
+  KnownSymbol nm
+  => GSchema (M1 S ('MetaSel ('Just nm) _1 _2 _3) (K1 _4 String))
+  where
+  gschema = do
+    emitRequired @nm
+    return $ makePropertyObj @nm $ makeTypeObj @String
+  {-# INLINE gschema #-}
+
+instance (GSchema f, GSchema g) => GSchema (f :*: g) where
+  gschema = mergeObjects <$> gschema @f <*> gschema @g
+  {-# INLINE gschema #-}
+
+instance
+  TypeError
+    ('Text "JSON Schema does not support sum types")
+  => GSchema (f :+: g)
+  where
+  gschema = error "JSON Schema does not support sum types"
+  {-# INLINE gschema #-}
+
+instance GSchema a => GSchema (M1 C _1 a) where
+  gschema = gschema @a
+  {-# INLINE gschema #-}
+
+instance
+  ( GSchema a
+  , KnownSymbol nm
+  )
+  => GSchema (M1 D ('MetaData nm _1 _2 _3) a)
+  where
+  gschema = do
+    sch <- gschema @a
+    return $
+      object
+        [ "title" .= String (pack $ symbolVal $ Proxy @nm)
+        , "type" .= String "object"
+        , "properties" .= sch
+        ]
+  {-# INLINE gschema #-}
+
+schema :: forall a. (GSchema (Rep a), Generic a) => Value
+schema = mergeObjects v $ object ["required" .= Array (fromList $ String <$> reqs)]
+ where
+  (v, reqs) = runWriter $ gschema @(Rep a)
+{-# INLINE schema #-}
+
+pp :: Value -> IO ()
+pp = LC8.putStrLn . encodePretty
diff --git a/ch14_14.1.example.hs b/ch14_14.1.example.hs
new file mode 100644
index 0000000..91bfcbf
--- /dev/null
+++ b/ch14_14.1.example.hs
@@ -0,0 +1,79 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE RebindableSyntax #-}
+
+import Control.Monad.Indexed qualified as I
+import Data.Coerce (coerce)
+import Fcf (Eval, Filter, Find, IsJust, Not, TyEq, type (<=<), type (=<<))
+import GHC.TypeLits (Nat, type (+))
+import Language.Haskell.DoNotation (Monad, pure, (>>=))
+import System.IO qualified as IO
+import Prelude hiding (Monad, pure, (>>=))
+
+newtype Ix m i j a = Ix
+  { unsafeRunIx :: m a
+  }
+  deriving (Functor, Applicative, Monad)
+
+instance Functor m => I.IxFunctor (Ix m) where
+  imap = fmap
+
+instance (Applicative m, Monad m) => I.IxPointed (Ix m) where
+  ireturn = pure
+
+instance (Applicative m, Monad m) => I.IxApplicative (Ix m) where
+  iap :: forall i j k a b. Ix m i j (a -> b) -> Ix m j k a -> Ix m i k b
+  iap = coerce $ (<*>) @m @a @b
+
+instance Monad m => I.IxMonad (Ix m) where
+  ibind :: forall i j k a b. (a -> Ix m j k b) -> Ix m i j a -> Ix m i k b
+  ibind = coerce $ (=<<) @m @a @b
+
+data LinearState = LinearState
+  { linearNextKey :: Nat
+  , linearOpenKeys :: [Nat]
+  }
+
+newtype Linear s (i :: LinearState) (j :: LinearState) a = Linear
+  { unsafeRunLinear :: Ix IO i j a
+  }
+  deriving (I.IxFunctor, I.IxPointed, I.IxApplicative, I.IxMonad)
+
+newtype Handle s key = Handle
+  { unsafeGetHandle :: IO.Handle
+  }
+
+openFile
+  :: FilePath
+  -> IO.IOMode
+  -> Linear
+      s
+      ('LinearState next open)
+      ('LinearState (next + 1) (next ': open))
+      (Handle s next)
+openFile = coerce IO.openFile
+
+type IsOpen (key :: k) (ts :: [k]) = IsJust =<< Find (TyEq key) ts
+
+type Close (key :: k) (ts :: [k]) = Filter (Not <=< TyEq key) ts
+
+closeFile
+  :: Eval (IsOpen key open) ~ 'True
+  => Handle s key
+  -> Linear
+      s
+      ('LinearState next open)
+      ('LinearState next (Eval (Close key open)))
+      ()
+closeFile = coerce IO.hClose
+
+-- If I try to write this point-free GHC gets angry. Not sure why that is:
+--
+-- • Couldn't match representation of type ‘a0’ with that of ‘IO a’
+--     arising from a use of ‘coerce’
+--
+-- 79 | runLinear = coerce
+--    |             ^^^^^^
+runLinear :: (forall s. Linear s ('LinearState 0 '[]) ('LinearState n '[]) a) -> IO a
+runLinear a = coerce a
diff --git a/ch15_15.0.example.hs b/ch15_15.0.example.hs
new file mode 100644
index 0000000..8d63903
--- /dev/null
+++ b/ch15_15.0.example.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+
+import Control.Monad.Writer (WriterT, runWriterT, tell)
+import Data.Constraint (Dict (Dict))
+import Data.Foldable (for_)
+import Data.Kind (Type)
+
+data SBool (b :: Bool) where
+  STrue :: SBool 'True
+  SFalse :: SBool 'False
+
+data SomeSBool where
+  SomeSBool :: SBool b -> SomeSBool
+
+fromSBool :: SBool b -> Bool
+fromSBool STrue = True
+fromSBool SFalse = False
+
+toSBool :: Bool -> SomeSBool
+toSBool True = SomeSBool STrue
+toSBool False = SomeSBool SFalse
+
+withSomeSBool :: SomeSBool -> (forall (b :: Bool). SBool b -> r) -> r
+withSomeSBool (SomeSBool s) f = f s
+
+class Monad (LoggingMonad b) => MonadLogging (b :: Bool) where
+  type LoggingMonad b = (r :: Type -> Type) | r -> b
+  logMsg :: String -> LoggingMonad b ()
+  runLogging :: LoggingMonad b a -> IO a
+
+instance MonadLogging 'False where
+  type LoggingMonad 'False = IO
+  logMsg _ = pure ()
+  runLogging = id
+
+instance MonadLogging 'True where
+  type LoggingMonad 'True = WriterT [String] IO
+  logMsg s = tell [s]
+  runLogging m = do
+    (a, w) <- runWriterT m
+    for_ w putStrLn
+    pure a
+
+program :: MonadLogging b => LoggingMonad b ()
+program = do
+  logMsg "hello world"
+  pure ()
+
+dict :: (c 'True, c 'False) => SBool b -> Dict (c b)
+dict STrue = Dict
+dict SFalse = Dict
+
+test :: Bool -> IO ()
+test bool =
+  withSomeSBool (toSBool bool) $ \(sb :: SBool b) ->
+    case dict @MonadLogging sb of
+      Dict -> runLogging @b program
diff --git a/ch15_15.3-i.hs b/ch15_15.3-i.hs
new file mode 100644
index 0000000..9a0b2fd
--- /dev/null
+++ b/ch15_15.3-i.hs
@@ -0,0 +1,74 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+
+data family Sing (a :: k)
+
+data SomeSing k where
+  SomeSing :: Sing (a :: k) -> SomeSing k
+
+withSomeSing :: SomeSing k -> (forall (a :: k). Sing a -> r) -> r
+withSomeSing (SomeSing s) f = f s
+
+class SingKind k where
+  type Demote k = r | r -> k
+  toSing :: Demote k -> SomeSing k
+  fromSing :: Sing (a :: k) -> Demote k
+
+data instance Sing (a :: Bool) where
+  STrue :: Sing 'True
+  SFalse :: Sing 'False
+
+instance SingKind Bool where
+  type Demote Bool = Bool
+  toSing True = SomeSing STrue
+  toSing False = SomeSing SFalse
+  fromSing STrue = True
+  fromSing SFalse = False
+
+class SingI (a :: k) where
+  sing :: Sing a
+
+instance SingI 'True where
+  sing = STrue
+
+instance SingI 'False where
+  sing = SFalse
+
+data instance Sing (a :: Maybe k) where
+  SJust :: Sing (a :: k) -> Sing ('Just a)
+  SNothing :: Sing 'Nothing
+
+instance SingI a => SingI ('Just a) where
+  sing = SJust sing
+
+instance SingI 'Nothing where
+  sing = SNothing
+
+instance (k ~ Demote k, SingKind k) => SingKind (Maybe k) where
+  type Demote (Maybe k) = Maybe k
+  toSing (Just a) = withSomeSing (toSing a) $ SomeSing . SJust
+  toSing Nothing = SomeSing SNothing
+  fromSing (SJust a) = Just $ fromSing a
+  fromSing SNothing = Nothing
+
+data instance Sing (a :: [k]) where
+  SNil :: Sing '[]
+  SCons :: Sing (h :: k) -> Sing (t :: [k]) -> Sing (h ': t)
+
+-- Exercise 15.3-i
+-- Provide instances of `SingI` for lists.
+instance (SingI h, SingI t) => SingI (h ': t) where
+  sing = SCons sing sing
+
+instance SingI '[] where
+  sing = SNil
+
+instance (k ~ Demote k, SingKind k) => SingKind [k] where
+  type Demote [k] = [k]
+  toSing [] = SomeSing SNil
+  toSing (h : t) =
+    withSomeSing (toSing h) $ \sh ->
+      withSomeSing (toSing t) $ \st ->
+        SomeSing $ SCons sh st
+  fromSing SNil = []
+  fromSing (SCons h t) = fromSing h : fromSing t
diff --git a/ch15_15.4-i.hs b/ch15_15.4-i.hs
new file mode 100644
index 0000000..273753d
--- /dev/null
+++ b/ch15_15.4-i.hs
@@ -0,0 +1,10 @@
+-- Exercise 15.4-i
+-- Give instances of `SDecide` for `Maybe`.
+
+-- This is slightly different to Sandy's version but I feel it should work the
+-- same. I can't easily test if it compiles though. Importing
+-- `Data.Singletons.Decide` pulls in the already existing instances!
+instance SDecide a => SDecide (Maybe a) where
+  SJust a %~ SJust b = a %~ b
+  SNothing %~ SNothing = Proved Refl
+  _ %~ _ = Disproved $ const undefined
diff --git a/ch15_15.5-i.hs b/ch15_15.5-i.hs
new file mode 100644
index 0000000..ac52df4
--- /dev/null
+++ b/ch15_15.5-i.hs
@@ -0,0 +1,85 @@
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+import Data.Constraint (Dict (Dict))
+import Data.Kind (Type)
+import Data.Singletons (Demote, Sing, SingI, SingKind, fromSing, sing)
+import Data.Singletons.Decide qualified as D
+
+data Sigma (f :: k -> Type) where
+  Sigma :: Sing a -> f a -> Sigma f
+
+withSigma :: (forall (a :: k). Sing a -> f a -> r) -> Sigma f -> r
+withSigma c (Sigma s f) = c s f
+
+toSigma :: SingI a => f a -> Sigma f
+toSigma = Sigma sing
+
+fromSigma
+  :: forall k (a :: k) (f :: k -> Type)
+   . (SingI a, D.SDecide k)
+  => Sigma f
+  -> Maybe (f a)
+fromSigma (Sigma s f) =
+  case s D.%~ sing @a of
+    D.Proved D.Refl -> Just f
+    D.Disproved _ -> Nothing
+
+class Dict1 c (f :: k -> Type) where
+  dict1 :: Sing (a :: k) -> Dict (c (f a))
+
+instance
+  ( Dict1 Eq (f :: k -> Type)
+  , D.SDecide k
+  )
+  => Eq (Sigma f)
+  where
+  Sigma sa fa == Sigma sb fb =
+    case sa D.%~ sb of
+      D.Proved D.Refl ->
+        case dict1 @_ @Eq @f sa of
+          Dict -> fa == fb
+      D.Disproved _ -> False
+
+-- Exercise 15.5-i
+-- Provide an instance of `Ord` for `Sigma` by comparing the `fs` if the
+-- singletons are equal, comparing the singletons at the term-level otherwise.
+instance
+  ( Dict1 Eq (f :: k -> Type)
+  , Dict1 Ord (f :: k -> Type)
+  , D.SDecide k
+  , Ord (Demote k)
+  , SingKind k
+  )
+  => Ord (Sigma f)
+  where
+  compare (Sigma sa fa) (Sigma sb fb) =
+    case sa D.%~ sb of
+      D.Proved D.Refl ->
+        -- Sandy passes `@Ord` as the first type application, however that
+        -- failed to compile on my PC. I had to do `@_ @Ord` instead (same
+        -- with `@Eq` above and `@Show` below). I wonder if newer versions of
+        -- GHC treat the order of type variables differently when used against
+        -- `class` functions, like `dict1` above.
+        case dict1 @_ @Ord @f sa of
+          Dict -> compare fa fb
+      D.Disproved _ -> compare (fromSing sa) (fromSing sb)
+
+instance
+  ( Dict1 Show (f :: k -> Type)
+  , Show (Demote k)
+  , SingKind k
+  )
+  => Show (Sigma f)
+  where
+  show (Sigma sa fa) =
+    case dict1 @_ @Show @f sa of
+      Dict ->
+        mconcat
+          [ "Sigma "
+          , show $ fromSing sa
+          , " ("
+          , show fa
+          , ")"
+          ]
diff --git a/ch15_15.5.1.example.hs b/ch15_15.5.1.example.hs
new file mode 100644
index 0000000..b2daec1
--- /dev/null
+++ b/ch15_15.5.1.example.hs
@@ -0,0 +1,77 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+
+import Data.Aeson (Value, object, (.=))
+import Data.Constraint (Dict (Dict))
+import Data.Kind (Type)
+import Data.Maybe (mapMaybe)
+import Data.Singletons (Sing, SingI, sing)
+import Data.Singletons.Base.TH (genSingletons, singDecideInstance)
+import Data.Singletons.Decide qualified as D
+
+data Sigma (f :: k -> Type) where
+  Sigma :: Sing a -> f a -> Sigma f
+
+withSigma :: (forall (a :: k). Sing a -> f a -> r) -> Sigma f -> r
+withSigma c (Sigma s f) = c s f
+
+toSigma :: SingI a => f a -> Sigma f
+toSigma = Sigma sing
+
+fromSigma
+  :: forall k (a :: k) (f :: k -> Type)
+   . (SingI a, D.SDecide k)
+  => Sigma f
+  -> Maybe (f a)
+fromSigma (Sigma s f) =
+  case s D.%~ sing @a of
+    D.Proved D.Refl -> Just f
+    D.Disproved _ -> Nothing
+
+class Dict1 c (f :: k -> Type) where
+  dict1 :: Sing (a :: k) -> Dict (c (f a))
+
+data LogType = JsonMsg | TextMsg deriving (Eq, Ord, Show)
+
+$(genSingletons [''LogType])
+$(singDecideInstance ''LogType)
+
+data family LogMsg (msg :: LogType)
+
+newtype instance LogMsg 'JsonMsg = Json Value deriving (Eq, Show)
+
+newtype instance LogMsg 'TextMsg = Text String deriving (Eq, Show)
+
+instance
+  ( c (LogMsg 'JsonMsg)
+  , c (LogMsg 'TextMsg)
+  )
+  => Dict1 c LogMsg
+  where
+  dict1 SJsonMsg = Dict
+  dict1 STextMsg = Dict
+
+catSigmas
+  :: forall k (a :: k) f
+   . ( SingI a
+     , D.SDecide k
+     )
+  => [Sigma f]
+  -> [f a]
+catSigmas = mapMaybe fromSigma
+
+logs :: [Sigma LogMsg]
+logs =
+  [ toSigma $ Text "hello"
+  , toSigma $ Json $ object ["world" .= (5 :: Int)]
+  , toSigma $ Text "structured logging"
+  ]
+
+jsonLogs :: [LogMsg 'JsonMsg]
+jsonLogs = catSigmas logs
+
+textLogs :: [LogMsg 'TextMsg]
+textLogs = catSigmas logs
diff --git a/fourmolu.yaml b/fourmolu.yaml
new file mode 100644
index 0000000..86a7343
--- /dev/null
+++ b/fourmolu.yaml
@@ -0,0 +1,54 @@
+# Number of spaces per indentation step
+indentation: 2
+
+# Max line length for automatic line breaking
+column-limit: 100
+
+# Styling of arrows in type signatures (choices: trailing, leading, or leading-args)
+function-arrows: leading
+
+# How to place commas in multi-line lists, records, etc. (choices: leading or trailing)
+comma-style: leading
+
+# Styling of import/export lists (choices: leading, trailing, or diff-friendly)
+import-export-style: leading
+
+# Whether to full-indent or half-indent 'where' bindings past the preceding body
+indent-wheres: false
+
+# Whether to leave a space before an opening record brace
+record-brace-space: true
+
+# Number of spaces between top-level declarations
+newlines-between-decls: 1
+
+# How to print Haddock comments (choices: single-line, multi-line, or multi-line-compact)
+haddock-style: multi-line
+
+# How to print module docstring
+haddock-style-module: null
+
+# Styling of let blocks (choices: auto, inline, newline, or mixed)
+let-style: auto
+
+# How to align the 'in' keyword with respect to the 'let' keyword (choices: left-align, right-align, or no-space)
+in-style: right-align
+
+# Whether to put parentheses around a single constraint (choices: auto, always, or never)
+single-constraint-parens: never
+
+# Whether to put parentheses around a single deriving class (choices: auto, always, or never)
+single-deriving-parens: never
+
+# Output Unicode syntax (choices: detect, always, or never)
+unicode: never
+
+# Give the programmer more choice on where to insert blank lines
+respectful: false
+
+# Fixity information for operators
+fixities: []
+
+# Module reexports Fourmolu should know about
+reexports: []
+
diff --git a/thinking.cabal b/thinking.cabal
new file mode 100644
index 0000000..84c04e5
--- /dev/null
+++ b/thinking.cabal
@@ -0,0 +1,25 @@
+cabal-version: 3.4
+author:        Paul Oliver
+build-type:    Simple
+maintainer:    contact@pauloliver.dev
+name:          thinking
+version:       0.1.0.0
+
+library
+  build-depends:
+    , aeson
+    , aeson-pretty
+    , base
+    , constraints
+    , do-notation
+    , first-class-families
+    , indexed
+    , mtl
+    , singletons
+    , singletons-base
+    , text
+    , vector
+
+  exposed-modules:
+  ghc-options:      -Wall -Wunused-packages
+  default-language: GHC2021