diff --git a/.editorconfig b/.editorconfig
new file mode 100644
--- /dev/null
+++ b/.editorconfig
@@ -0,0 +1,14 @@
+root = true
+
+[*]
+charset = utf-8
+end_of_line = lf
+indent_style = space
+indent_size = 2
+tab_width = 2
+insert_final_newline = true
+max_line_length = 80
+trim_trailing_whitespace = true
+
+[Makefile]
+indent_style = tab
diff --git a/.hlint.yaml b/.hlint.yaml
new file mode 100644
--- /dev/null
+++ b/.hlint.yaml
@@ -0,0 +1,6 @@
+- group: {name: default, enabled: true}
+- group: {name: dollar, enabled: true}
+- group: {name: future, enabled: true}
+- group: {name: generalise, enabled: true}
+
+- ignore: {name: Use fmap, within: Mini.Data.Map}
diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,3 @@
+0.1.0.0 [2024-03-07]
+--------------------
+* Initial upload to Hackage
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,20 @@
+Copyright (c) 2023-2024 Victor Wallsten
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/Mini/Data/Map.hs b/Mini/Data/Map.hs
new file mode 100644
--- /dev/null
+++ b/Mini/Data/Map.hs
@@ -0,0 +1,1067 @@
+{- | Representation of a structure mapping unique keys to values. The internal
+structure is an AVL tree.
+-}
+module Mini.Data.Map (
+  -- * Type
+  Map,
+
+  -- * Combination
+  difference,
+  intersection,
+  union,
+
+  -- * Construction
+  empty,
+  fromList,
+  singleton,
+
+  -- * Conversion
+  toAscList,
+  toDescList,
+
+  -- * Fold
+  foldlWithKey,
+  foldrWithKey,
+
+  -- * Modification
+  adjust,
+  delete,
+  filter,
+  filterWithKey,
+  insert,
+  update,
+
+  -- * Query
+  isSubmapOf,
+  lookup,
+  lookupMax,
+  lookupMin,
+  member,
+  null,
+  size,
+
+  -- * Traversal
+  traverseWithKey,
+
+  -- * Validation
+  valid,
+) where
+
+import Control.Monad (
+  liftM2,
+ )
+import Data.Bool (
+  bool,
+ )
+import Prelude hiding (
+  filter,
+  lookup,
+  map,
+  null,
+ )
+
+{-
+ - Type
+ -}
+
+{- | A map from keys of type /k/ to values of type /a/.
+
+The internal structure is an AVL tree; a tree that is always height-balanced
+(the absolute value of the level difference between the left and right
+subtrees is at most 1).
+-}
+data Map k a
+  = -- | Empty bin
+    E
+  | -- | Left-heavy bin
+    L (Map k a) k a (Map k a)
+  | -- | Balanced bin
+    B (Map k a) k a (Map k a)
+  | -- | Right-heavy bin
+    R (Map k a) k a (Map k a)
+  deriving (Eq, Ord)
+
+instance (Show k, Show a) => Show (Map k a) where
+  show = curl . map [] go go go
+   where
+    go _ k a _ recl recr = recl <> show (k, a) <> "," <> recr
+    curl = wrap "{" "}" . removeTrailingComma
+    wrap open close s = open <> s <> close
+    removeTrailingComma s = case s of
+      [] -> []
+      [_] -> []
+      (c : cs) -> c : removeTrailingComma cs
+
+instance Functor (Map k) where
+  fmap f =
+    map
+      E
+      (\_ k a _ recl recr -> L recl k (f a) recr)
+      (\_ k a _ recl recr -> B recl k (f a) recr)
+      (\_ k a _ recl recr -> R recl k (f a) recr)
+
+instance Foldable (Map k) where
+  foldr f b = map b go go go where go _ _ a r recl _ = foldr f (f a recl) r
+
+instance Traversable (Map k) where
+  traverse = traverseWithKey . const
+
+instance (Ord k) => Semigroup (Map k a) where
+  (<>) = union
+
+instance (Ord k) => Monoid (Map k a) where
+  mempty = empty
+
+{-
+ - Primitive recursion
+ -}
+
+-- | Primitive recursion on maps
+map
+  :: b
+  -- ^ Empty bin
+  -> (Map k a -> k -> a -> Map k a -> b -> b -> b)
+  -- ^ Left-heavy bin: left child, key, value, right child, left recursion,
+  -- right recursion
+  -> (Map k a -> k -> a -> Map k a -> b -> b -> b)
+  -- ^ Balanced bin: left child, key, value, right child, left recursion, right
+  -- recursion
+  -> (Map k a -> k -> a -> Map k a -> b -> b -> b)
+  -- ^ Right-heavy bin: left child, key, value, right child, left recursion,
+  -- right recursion
+  -> Map k a
+  -- ^ Map
+  -> b
+map e _ _ _ E = e
+map e f g h (L l k a r) = f l k a r (map e f g h l) (map e f g h r)
+map e f g h (B l k a r) = g l k a r (map e f g h l) (map e f g h r)
+map e f g h (R l k a r) = h l k a r (map e f g h l) (map e f g h r)
+
+{-
+ - Combination
+ -}
+
+-- | \(O(n \log n)\) Map difference (matching only on keys)
+difference :: (Ord k) => Map k a -> Map k b -> Map k a
+difference = foldrWithKey (\k _ b -> delete k b)
+
+-- | \(O(n \log n)\) Left-biased map intersection (matching only on keys)
+intersection :: (Ord k) => Map k a -> Map k b -> Map k a
+intersection t1 t2 =
+  foldrWithKey
+    (\k a b -> bool b (insert k a b) $ k `member` t2)
+    empty
+    t1
+
+-- | \(O(n \log n)\) Left-biased map union (matching only on keys)
+union :: (Ord k) => Map k a -> Map k a -> Map k a
+union t = foldrWithKey (\k a b -> bool b (insert k a b) . not $ k `member` t) t
+
+{-
+ - Construction
+ -}
+
+-- | \(O(1)\) The empty map
+empty :: Map k a
+empty = E
+
+{- | \(O(n \log n)\) From a tail-biased list of @(key, value)@ pairs to a map
+with bins containing the keys and values
+-}
+fromList :: (Ord k) => [(k, a)] -> Map k a
+fromList = foldl (flip $ uncurry insert) empty
+
+-- | \(O(1)\) From a key and a value to a map with a single bin
+singleton :: k -> a -> Map k a
+singleton k a = B E k a E
+
+{-
+ - Conversion
+ -}
+
+{- | \(O(n)\) From a map to a list of @(key, value)@ pairs in key-ascending
+order
+-}
+toAscList :: Map k a -> [(k, a)]
+toAscList = foldlWithKey (\b k a -> (k, a) : b) []
+
+{- | \(O(n)\) From a map to a list of @(key, value)@ pairs in key-descending
+order
+-}
+toDescList :: Map k a -> [(k, a)]
+toDescList = foldrWithKey (\k a b -> (k, a) : b) []
+
+{-
+ - Fold
+ -}
+
+{- | \(O(n)\) From a left-associative operation on keys and values, a starting
+accumulator and a map to a thing
+-}
+foldlWithKey :: (b -> k -> a -> b) -> b -> Map k a -> b
+foldlWithKey f b = map b go go go
+ where
+  go l k a _ _ recr = foldlWithKey f (f recr k a) l
+
+{- | \(O(n)\) From a right-associative operation on keys and values, a starting
+accumulator and a map to a thing
+-}
+foldrWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b
+foldrWithKey f b = map b go go go
+ where
+  go _ k a r recl _ = foldrWithKey f (f k a recl) r
+
+{-
+ - Modification
+ -}
+
+{- | \(O(\log n)\) From an operation, a key and a map to the map adjusted by
+applying the operation to the value associated with the key
+-}
+adjust :: (Ord k) => (a -> a) -> k -> Map k a -> Map k a
+adjust f k0 =
+  map
+    E
+    ( \l k a r recl recr ->
+        case compare k0 k of
+          LT -> L recl k a r
+          EQ -> L l k (f a) r
+          GT -> L l k a recr
+    )
+    ( \l k a r recl recr ->
+        case compare k0 k of
+          LT -> B recl k a r
+          EQ -> B l k (f a) r
+          GT -> B l k a recr
+    )
+    ( \l k a r recl recr ->
+        case compare k0 k of
+          LT -> R recl k a r
+          EQ -> R l k (f a) r
+          GT -> R l k a recr
+    )
+
+-- | \(O(\log n)\) From a key and a map to the map without the key
+delete :: (Ord k) => k -> Map k a -> Map k a
+delete k0 t = bool t (go t) (k0 `member` t)
+ where
+  go =
+    map
+      (error "Map.delete: L0")
+      ( \l k a r _ _ ->
+          case compare k0 k of
+            LT -> deleteLl l k a r
+            EQ -> substituteL l r
+            GT -> deleteLr l k a r
+      )
+      ( \l k a r _ _ ->
+          case compare k0 k of
+            LT -> deleteBl l k a r
+            EQ -> substituteBr l r
+            GT -> deleteBr l k a r
+      )
+      ( \l k a r _ _ ->
+          case compare k0 k of
+            LT -> deleteRl l k a r
+            EQ -> substituteR l r
+            GT -> deleteRr l k a r
+      )
+  deleteRl l k a r =
+    map
+      (error "Map.delete: L1")
+      ( \ll lk la lr _ _ ->
+          case compare k0 lk of
+            LT -> checkLeftR (deleteLl ll lk la lr) k a r
+            EQ -> checkLeftR (substituteL ll lr) k a r
+            GT -> checkLeftR (deleteLr ll lk la lr) k a r
+      )
+      ( \ll lk la lr _ _ ->
+          case compare k0 lk of
+            LT -> R (deleteBl ll lk la lr) k a r
+            EQ -> checkLeftR' (substituteBr ll lr) k a r
+            GT -> R (deleteBr ll lk la lr) k a r
+      )
+      ( \ll lk la lr _ _ ->
+          case compare k0 lk of
+            LT -> checkLeftR (deleteRl ll lk la lr) k a r
+            EQ -> checkLeftR (substituteR ll lr) k a r
+            GT -> checkLeftR (deleteRr ll lk la lr) k a r
+      )
+      l
+  deleteRr l k a =
+    map
+      (error "Map.delete: L2")
+      ( \rl rk ra rr _ _ ->
+          case compare k0 rk of
+            LT -> checkRightR l k a (deleteLl rl rk ra rr)
+            EQ -> checkRightR l k a (substituteL rl rr)
+            GT -> checkRightR l k a (deleteLr rl rk ra rr)
+      )
+      ( \rl rk ra rr _ _ ->
+          case compare k0 rk of
+            LT -> R l k a (deleteBl rl rk ra rr)
+            EQ -> checkRightR' l k a (substituteBl rl rr)
+            GT -> R l k a (deleteBr rl rk ra rr)
+      )
+      ( \rl rk ra rr _ _ ->
+          case compare k0 rk of
+            LT -> checkRightR l k a (deleteRl rl rk ra rr)
+            EQ -> checkRightR l k a (substituteR rl rr)
+            GT -> checkRightR l k a (deleteRr rl rk ra rr)
+      )
+  deleteBl l k a r =
+    map
+      (error "Map.delete: L3")
+      ( \ll lk la lr _ _ ->
+          case compare k0 lk of
+            LT -> checkLeftB (deleteLl ll lk la lr) k a r
+            EQ -> checkLeftB (substituteL ll lr) k a r
+            GT -> checkLeftB (deleteLr ll lk la lr) k a r
+      )
+      ( \ll lk la lr _ _ ->
+          case compare k0 lk of
+            LT -> B (deleteBl ll lk la lr) k a r
+            EQ -> checkLeftB' (substituteBr ll lr) k a r
+            GT -> B (deleteBr ll lk la lr) k a r
+      )
+      ( \ll lk la lr _ _ ->
+          case compare k0 lk of
+            LT -> checkLeftB (deleteRl ll lk la lr) k a r
+            EQ -> checkLeftB (substituteR ll lr) k a r
+            GT -> checkLeftB (deleteRr ll lk la lr) k a r
+      )
+      l
+  deleteBr l k a =
+    map
+      (error "Map.delete: L4")
+      ( \rl rk ra rr _ _ ->
+          case compare k0 rk of
+            LT -> checkRightB l k a (deleteLl rl rk ra rr)
+            EQ -> checkRightB l k a (substituteL rl rr)
+            GT -> checkRightB l k a (deleteLr rl rk ra rr)
+      )
+      ( \rl rk ra rr _ _ ->
+          case compare k0 rk of
+            LT -> B l k a (deleteBl rl rk ra rr)
+            EQ -> checkRightB' l k a (substituteBl rl rr)
+            GT -> B l k a (deleteBr rl rk ra rr)
+      )
+      ( \rl rk ra rr _ _ ->
+          case compare k0 rk of
+            LT -> checkRightB l k a (deleteRl rl rk ra rr)
+            EQ -> checkRightB l k a (substituteR rl rr)
+            GT -> checkRightB l k a (deleteRr rl rk ra rr)
+      )
+  deleteLl l k a r =
+    map
+      (error "Map.delete: L5")
+      ( \ll lk la lr _ _ ->
+          case compare k0 lk of
+            LT -> checkLeftL (deleteLl ll lk la lr) k a r
+            EQ -> checkLeftL (substituteL ll lr) k a r
+            GT -> checkLeftL (deleteLr ll lk la lr) k a r
+      )
+      ( \ll lk la lr _ _ ->
+          case compare k0 lk of
+            LT -> L (deleteBl ll lk la lr) k a r
+            EQ -> checkLeftL' (substituteBr ll lr) k a r
+            GT -> L (deleteBr ll lk la lr) k a r
+      )
+      ( \ll lk la lr _ _ ->
+          case compare k0 lk of
+            LT -> checkLeftL (deleteRl ll lk la lr) k a r
+            EQ -> checkLeftL (substituteR ll lr) k a r
+            GT -> checkLeftL (deleteRr ll lk la lr) k a r
+      )
+      l
+  deleteLr l k a =
+    map
+      (error "Map.delete: L6")
+      ( \rl rk ra rr _ _ ->
+          case compare k0 rk of
+            LT -> checkRightL l k a (deleteLl rl rk ra rr)
+            EQ -> checkRightL l k a (substituteL rl rr)
+            GT -> checkRightL l k a (deleteLr rl rk ra rr)
+      )
+      ( \rl rk ra rr _ _ ->
+          case compare k0 rk of
+            LT -> L l k a (deleteBl rl rk ra rr)
+            EQ -> checkRightL' l k a (substituteBl rl rr)
+            GT -> L l k a (deleteBr rl rk ra rr)
+      )
+      ( \rl rk ra rr _ _ ->
+          case compare k0 rk of
+            LT -> checkRightL l k a (deleteRl rl rk ra rr)
+            EQ -> checkRightL l k a (substituteR rl rr)
+            GT -> checkRightL l k a (deleteRr rl rk ra rr)
+      )
+  rebalanceR l k a =
+    map
+      (error "Map.delete: L7")
+      ( \rl rk ra rr _ _ ->
+          map
+            (error "Map.delete: L8")
+            (\rll rlk rla rlr _ _ -> B (B l k a rll) rlk rla (R rlr rk ra rr))
+            (\rll rlk rla rlr _ _ -> B (B l k a rll) rlk rla (B rlr rk ra rr))
+            (\rll rlk rla rlr _ _ -> B (L l k a rll) rlk rla (B rlr rk ra rr))
+            rl
+      )
+      (\rl rk ra rr _ _ -> L (R l k a rl) rk ra rr)
+      (\rl rk ra rr _ _ -> B (B l k a rl) rk ra rr)
+  rebalanceL l k a r =
+    map
+      (error "Map.delete: L9")
+      (\ll lk la lr _ _ -> B ll lk la (B lr k a r))
+      (\ll lk la lr _ _ -> R ll lk la (L lr k a r))
+      ( \ll lk la lr _ _ ->
+          map
+            (error "Map.delete: L10")
+            (\lrl lrk lra lrr _ _ -> B (B ll lk la lrl) lrk lra (R lrr k a r))
+            (\lrl lrk lra lrr _ _ -> B (B ll lk la lrl) lrk lra (B lrr k a r))
+            (\lrl lrk lra lrr _ _ -> B (L ll lk la lrl) lrk lra (B lrr k a r))
+            lr
+      )
+      l
+  checkLeftR l k a r =
+    map
+      (error "Map.delete: L11")
+      (\_ _ _ _ _ _ -> R l k a r)
+      (\_ _ _ _ _ _ -> rebalanceR l k a r)
+      (\_ _ _ _ _ _ -> R l k a r)
+      l
+  checkLeftB l k a r =
+    map
+      (error "Map.delete: L12")
+      (\_ _ _ _ _ _ -> B l k a r)
+      (\_ _ _ _ _ _ -> R l k a r)
+      (\_ _ _ _ _ _ -> B l k a r)
+      l
+  checkLeftL l k a r =
+    map
+      (error "Map.delete: L13")
+      (\_ _ _ _ _ _ -> L l k a r)
+      (\_ _ _ _ _ _ -> B l k a r)
+      (\_ _ _ _ _ _ -> L l k a r)
+      l
+  checkRightR l k a r =
+    map
+      (error "Map.delete: L14")
+      (\_ _ _ _ _ _ -> R l k a r)
+      (\_ _ _ _ _ _ -> B l k a r)
+      (\_ _ _ _ _ _ -> R l k a r)
+      r
+  checkRightB l k a r =
+    map
+      (error "Map.delete: L15")
+      (\_ _ _ _ _ _ -> B l k a r)
+      (\_ _ _ _ _ _ -> L l k a r)
+      (\_ _ _ _ _ _ -> B l k a r)
+      r
+  checkRightL l k a r =
+    map
+      (error "Map.delete: L16")
+      (\_ _ _ _ _ _ -> L l k a r)
+      (\_ _ _ _ _ _ -> rebalanceL l k a r)
+      (\_ _ _ _ _ _ -> L l k a r)
+      r
+  substituteR l =
+    map
+      (error "Map.delete: L17")
+      ( \rl rk ra rr _ _ ->
+          (\(k, a, r) -> checkRightR l k a r) $
+            popLeftL rl rk ra rr
+      )
+      ( \rl rk ra rr _ _ ->
+          (\(k, a, r) -> checkRightR' l k a r) $
+            popLeftB rl rk ra rr
+      )
+      ( \rl rk ra rr _ _ ->
+          (\(k, a, r) -> checkRightR l k a r) $
+            popLeftR rl rk ra rr
+      )
+  substituteBr l =
+    map
+      E
+      ( \rl rk ra rr _ _ ->
+          (\(k, a, r) -> checkRightB l k a r) $
+            popLeftL rl rk ra rr
+      )
+      ( \rl rk ra rr _ _ ->
+          (\(k, a, r) -> checkRightB' l k a r) $
+            popLeftB rl rk ra rr
+      )
+      ( \rl rk ra rr _ _ ->
+          (\(k, a, r) -> checkRightB l k a r) $
+            popLeftR rl rk ra rr
+      )
+  substituteBl l r =
+    map
+      E
+      ( \ll lk la lr _ _ ->
+          (\(l', k, a) -> checkLeftB l' k a r) $
+            popRightL ll lk la lr
+      )
+      ( \ll lk la lr _ _ ->
+          (\(l', k, a) -> checkLeftB' l' k a r) $
+            popRightB ll lk la lr
+      )
+      ( \ll lk la lr _ _ ->
+          (\(l', k, a) -> checkLeftB l' k a r) $
+            popRightR ll lk la lr
+      )
+      l
+  substituteL l r =
+    map
+      (error "Map.delete: L18")
+      ( \ll lk la lr _ _ ->
+          (\(l', k, a) -> checkLeftL l' k a r) $
+            popRightL ll lk la lr
+      )
+      ( \ll lk la lr _ _ ->
+          (\(l', k, a) -> checkLeftL' l' k a r) $
+            popRightB ll lk la lr
+      )
+      ( \ll lk la lr _ _ ->
+          (\(l', k, a) -> checkLeftL l' k a r) $
+            popRightR ll lk la lr
+      )
+      l
+  checkLeftR' l k a r =
+    map
+      (rebalanceR l k a r)
+      (\_ _ _ _ _ _ -> R l k a r)
+      (\_ _ _ _ _ _ -> R l k a r)
+      (\_ _ _ _ _ _ -> R l k a r)
+      l
+  checkLeftB' l k a r =
+    map
+      (R l k a r)
+      (\_ _ _ _ _ _ -> B l k a r)
+      (\_ _ _ _ _ _ -> B l k a r)
+      (\_ _ _ _ _ _ -> B l k a r)
+      l
+  checkLeftL' l k a r =
+    map
+      (B l k a r)
+      (\_ _ _ _ _ _ -> L l k a r)
+      (\_ _ _ _ _ _ -> L l k a r)
+      (\_ _ _ _ _ _ -> L l k a r)
+      l
+  checkRightR' l k a r =
+    map
+      (B l k a r)
+      (\_ _ _ _ _ _ -> R l k a r)
+      (\_ _ _ _ _ _ -> R l k a r)
+      (\_ _ _ _ _ _ -> R l k a r)
+      r
+  checkRightB' l k a r =
+    map
+      (L l k a r)
+      (\_ _ _ _ _ _ -> B l k a r)
+      (\_ _ _ _ _ _ -> B l k a r)
+      (\_ _ _ _ _ _ -> B l k a r)
+      r
+  checkRightL' l k a r =
+    map
+      (rebalanceL l k a r)
+      (\_ _ _ _ _ _ -> L l k a r)
+      (\_ _ _ _ _ _ -> L l k a r)
+      (\_ _ _ _ _ _ -> L l k a r)
+      r
+  popLeftR l k a r =
+    map
+      (k, a, r)
+      ( \ll lk la lr _ _ ->
+          (\(k', a', l') -> (k', a', checkLeftR l' k a r)) $
+            popLeftL ll lk la lr
+      )
+      (\ll lk la lr _ _ -> popLeftRB ll lk la lr k a r)
+      ( \ll lk la lr _ _ ->
+          (\(k', a', l') -> (k', a', checkLeftR l' k a r)) $
+            popLeftR ll lk la lr
+      )
+      l
+  popLeftB l k a r =
+    map
+      (k, a, E)
+      (\ll lk la lr _ _ -> popLeftBL ll lk la lr k a r)
+      (\ll lk la lr _ _ -> popLeftBB ll lk la lr k a r)
+      (\ll lk la lr _ _ -> popLeftBR ll lk la lr k a r)
+      l
+  popLeftL l k a r =
+    map
+      (error "Map.delete: L19")
+      ( \ll lk la lr _ _ ->
+          (\(k', a', l') -> (k', a', checkLeftL l' k a r)) $
+            popLeftL ll lk la lr
+      )
+      (\ll lk la lr _ _ -> popLeftLB ll lk la lr k a r)
+      ( \ll lk la lr _ _ ->
+          (\(k', a', l') -> (k', a', checkLeftL l' k a r)) $
+            popLeftR ll lk la lr
+      )
+      l
+  popLeftRB ll lk la lr k a r =
+    map
+      (lk, la, rebalanceR E k a r)
+      ( \lll llk lla llr _ _ ->
+          (\(k', a', l) -> (k', a', R l k a r)) $
+            popLeftBL lll llk lla llr lk la lr
+      )
+      ( \lll llk lla llr _ _ ->
+          (\(k', a', l) -> (k', a', R l k a r)) $
+            popLeftBB lll llk lla llr lk la lr
+      )
+      ( \lll llk lla llr _ _ ->
+          (\(k', a', l) -> (k', a', R l k a r)) $
+            popLeftBR lll llk lla llr lk la lr
+      )
+      ll
+  popLeftBB ll lk la lr k a r =
+    map
+      (lk, la, R E k a r)
+      ( \lll llk lla llr _ _ ->
+          (\(k', a', l) -> (k', a', B l k a r)) $
+            popLeftBL lll llk lla llr lk la lr
+      )
+      ( \lll llk lla llr _ _ ->
+          (\(k', a', l) -> (k', a', B l k a r)) $
+            popLeftBB lll llk lla llr lk la lr
+      )
+      ( \lll llk lla llr _ _ ->
+          (\(k', a', l) -> (k', a', B l k a r)) $
+            popLeftBR lll llk lla llr lk la lr
+      )
+      ll
+  popLeftLB ll lk la lr k a r =
+    map
+      (lk, la, B E k a E)
+      ( \lll llk lla llr _ _ ->
+          (\(k', a', l) -> (k', a', L l k a r)) $
+            popLeftBL lll llk lla llr lk la lr
+      )
+      ( \lll llk lla llr _ _ ->
+          (\(k', a', l) -> (k', a', L l k a r)) $
+            popLeftBB lll llk lla llr lk la lr
+      )
+      ( \lll llk lla llr _ _ ->
+          (\(k', a', l) -> (k', a', L l k a r)) $
+            popLeftBR lll llk lla llr lk la lr
+      )
+      ll
+  popLeftBR ll lk la lr k a r =
+    (\(k', a', l) -> (k', a', checkLeftB l k a r)) $
+      popLeftR ll lk la lr
+  popLeftBL ll lk la lr k a r =
+    (\(k', a', l) -> (k', a', checkLeftB l k a r)) $
+      popLeftL ll lk la lr
+  popRightR l k a =
+    map
+      (error "Map.delete: L20")
+      ( \rl rk ra rr _ _ ->
+          (\(r, k', a') -> (checkRightR l k a r, k', a')) $
+            popRightL rl rk ra rr
+      )
+      (\rl rk ra rr _ _ -> popRightRB l k a rl rk ra rr)
+      ( \rl rk ra rr _ _ ->
+          (\(r, k', a') -> (checkRightR l k a r, k', a')) $
+            popRightR rl rk ra rr
+      )
+  popRightB l k a =
+    map
+      (E, k, a)
+      (\rl rk ra rr _ _ -> popRightBL l k a rl rk ra rr)
+      (\rl rk ra rr _ _ -> popRightBB l k a rl rk ra rr)
+      (\rl rk ra rr _ _ -> popRightBR l k a rl rk ra rr)
+  popRightL l k a =
+    map
+      (l, k, a)
+      ( \rl rk ra rr _ _ ->
+          (\(r, k', a') -> (checkRightL l k a r, k', a')) $
+            popRightL rl rk ra rr
+      )
+      (\rl rk ra rr _ _ -> popRightLB l k a rl rk ra rr)
+      ( \rl rk ra rr _ _ ->
+          (\(r, k', a') -> (checkRightL l k a r, k', a')) $
+            popRightR rl rk ra rr
+      )
+  popRightRB l k a rl rk ra =
+    map
+      (B E k a E, rk, ra)
+      ( \rrl rrk rra rrr _ _ ->
+          (\(r, k', a') -> (R l k a r, k', a')) $
+            popRightBL rl rk ra rrl rrk rra rrr
+      )
+      ( \rrl rrk rra rrr _ _ ->
+          (\(r, k', a') -> (R l k a r, k', a')) $
+            popRightBB rl rk ra rrl rrk rra rrr
+      )
+      ( \rrl rrk rra rrr _ _ ->
+          (\(r, k', a') -> (R l k a r, k', a')) $
+            popRightBR rl rk ra rrl rrk rra rrr
+      )
+  popRightBB l k a rl rk ra =
+    map
+      (L l k a E, rk, ra)
+      ( \rrl rrk rra rrr _ _ ->
+          (\(r, k', a') -> (B l k a r, k', a')) $
+            popRightBL rl rk ra rrl rrk rra rrr
+      )
+      ( \rrl rrk rra rrr _ _ ->
+          (\(r, k', a') -> (B l k a r, k', a')) $
+            popRightBB rl rk ra rrl rrk rra rrr
+      )
+      ( \rrl rrk rra rrr _ _ ->
+          (\(r, k', a') -> (B l k a r, k', a')) $
+            popRightBR rl rk ra rrl rrk rra rrr
+      )
+  popRightLB l k a rl rk ra =
+    map
+      (rebalanceL l k a E, rk, ra)
+      ( \rrl rrk rra rrr _ _ ->
+          (\(r, k', a') -> (L l k a r, k', a')) $
+            popRightBL rl rk ra rrl rrk rra rrr
+      )
+      ( \rrl rrk rra rrr _ _ ->
+          (\(r, k', a') -> (L l k a r, k', a')) $
+            popRightBB rl rk ra rrl rrk rra rrr
+      )
+      ( \rrl rrk rra rrr _ _ ->
+          (\(r, k', a') -> (L l k a r, k', a')) $
+            popRightBR rl rk ra rrl rrk rra rrr
+      )
+  popRightBR l k a rl rk ra rr =
+    (\(r, k', a') -> (checkRightB l k a r, k', a')) $
+      popRightR rl rk ra rr
+  popRightBL l k a rl rk ra rr =
+    (\(r, k', a') -> (checkRightB l k a r, k', a')) $
+      popRightL rl rk ra rr
+
+{- | \(O(n)\) From a predicate and a map to the map with values satisfying the
+predicate
+-}
+filter :: (Ord k) => (a -> Bool) -> Map k a -> Map k a
+filter p = foldrWithKey (\k a b -> bool b (insert k a b) $ p a) empty
+
+{- | \(O(n)\) From a predicate and a map to the map with keys and values
+satisfying the predicate
+-}
+filterWithKey :: (Ord k) => (k -> a -> Bool) -> Map k a -> Map k a
+filterWithKey p = foldrWithKey (\k a b -> bool b (insert k a b) $ p k a) empty
+
+{- | \(O(\log n)\) From a key, a value and a map to the map including a bin
+containing the key and the value
+-}
+insert :: (Ord k) => k -> a -> Map k a -> Map k a
+insert k0 a0 =
+  map
+    (B E k0 a0 E)
+    (\l k a r _ _ -> insertL l k a r)
+    (\l k a r _ _ -> insertB l k a r)
+    (\l k a r _ _ -> insertR l k a r)
+ where
+  insertR l k a r =
+    case compare k0 k of
+      LT -> insertRl l k a r
+      EQ -> R l k a r
+      GT -> insertRr l k a r
+  insertB l k a r =
+    case compare k0 k of
+      LT -> insertBl l k a r
+      EQ -> B l k a r
+      GT -> insertBr l k a r
+  insertL l k a r =
+    case compare k0 k of
+      LT -> insertLl l k a r
+      EQ -> L l k a r
+      GT -> insertLr l k a r
+  insertRl l k a r =
+    map
+      (B (B E k0 a0 E) k a r)
+      (\ll lk la lr _ _ -> R (insertL ll lk la lr) k a r)
+      ( \ll lk la lr _ _ ->
+          let l' = insertB ll lk la lr
+           in map
+                (error "Map.insert: L0")
+                (\_ _ _ _ _ _ -> B l' k a r)
+                (\_ _ _ _ _ _ -> R l' k a r)
+                (\_ _ _ _ _ _ -> B l' k a r)
+                l'
+      )
+      (\ll lk la lr _ _ -> R (insertR ll lk la lr) k a r)
+      l
+  insertBl l k a r =
+    map
+      (L (B E k0 a0 E) k a r)
+      (\ll lk la lr _ _ -> B (insertL ll lk la lr) k a r)
+      ( \ll lk la lr _ _ ->
+          let l' = insertB ll lk la lr
+           in map
+                (error "Map.insert: L1")
+                (\_ _ _ _ _ _ -> L l' k a r)
+                (\_ _ _ _ _ _ -> B l' k a r)
+                (\_ _ _ _ _ _ -> L l' k a r)
+                l'
+      )
+      (\ll lk la lr _ _ -> B (insertR ll lk la lr) k a r)
+      l
+  insertBr l k a =
+    map
+      (R l k a (B E k0 a0 E))
+      (\rl rk ra rr _ _ -> B l k a (insertL rl rk ra rr))
+      ( \rl rk ra rr _ _ ->
+          let r = insertB rl rk ra rr
+           in map
+                (error "Map.insert: L2")
+                (\_ _ _ _ _ _ -> R l k a r)
+                (\_ _ _ _ _ _ -> B l k a r)
+                (\_ _ _ _ _ _ -> R l k a r)
+                r
+      )
+      (\rl rk ra rr _ _ -> B l k a (insertR rl rk ra rr))
+  insertLr l k a =
+    map
+      (B l k a (B E k0 a0 E))
+      (\rl rk ra rr _ _ -> L l k a (insertL rl rk ra rr))
+      ( \rl rk ra rr _ _ ->
+          let r = insertB rl rk ra rr
+           in map
+                (error "Map.insert: L3")
+                (\_ _ _ _ _ _ -> B l k a r)
+                (\_ _ _ _ _ _ -> L l k a r)
+                (\_ _ _ _ _ _ -> B l k a r)
+                r
+      )
+      (\rl rk ra rr _ _ -> L l k a (insertR rl rk ra rr))
+  insertRr l k a =
+    map
+      (error "Map.insert: L4")
+      (\rl rk ra rr _ _ -> R l k a (insertL rl rk ra rr))
+      ( \rl rk ra rr _ _ ->
+          case compare k0 rk of
+            LT -> insertRrl l k a rl rk ra rr
+            EQ -> R l k a (B rl rk ra rr)
+            GT -> insertRrr l k a rl rk ra rr
+      )
+      (\rl rk ra rr _ _ -> R l k a (insertR rl rk ra rr))
+  insertLl l k a r =
+    map
+      (error "Map.insert: L5")
+      (\ll lk la lr _ _ -> L (insertL ll lk la lr) k a r)
+      ( \ll lk la lr _ _ ->
+          case compare k0 lk of
+            LT -> insertLll ll lk la lr k a r
+            EQ -> L (B ll lk la lr) k a r
+            GT -> insertLlr ll lk la lr k a r
+      )
+      (\ll lk la lr _ _ -> L (insertR ll lk la lr) k a r)
+      l
+  insertRrr l k a rl rk ra =
+    map
+      (B (B l k a rl) rk ra (B E k0 a0 E))
+      (\rrl rrk rra rrr _ _ -> R l k a (B rl rk ra (insertL rrl rrk rra rrr)))
+      ( \rrl rrk rra rrr _ _ ->
+          let rr = insertB rrl rrk rra rrr
+           in map
+                (error "Map.insert: L6")
+                (\_ _ _ _ _ _ -> B (B l k a rl) rk ra rr)
+                (\_ _ _ _ _ _ -> R l k a (B rl rk ra rr))
+                (\_ _ _ _ _ _ -> B (B l k a rl) rk ra rr)
+                rr
+      )
+      (\rrl rrk rra rrr _ _ -> R l k a (B rl rk ra (insertR rrl rrk rra rrr)))
+  insertLll ll lk la lr k a r =
+    map
+      (B (B E k0 a0 E) lk la (B lr k a r))
+      (\lll llk lla llr _ _ -> L (B (insertL lll llk lla llr) lk la lr) k a r)
+      ( \lll llk lla llr _ _ ->
+          let ll' = insertB lll llk lla llr
+           in map
+                (error "Map.insert: L7")
+                (\_ _ _ _ _ _ -> B ll' lk la (B lr k a r))
+                (\_ _ _ _ _ _ -> L (B ll' lk la lr) k a r)
+                (\_ _ _ _ _ _ -> B ll' lk la (B lr k a r))
+                ll'
+      )
+      (\lll llk lla llr _ _ -> L (B (insertR lll llk lla llr) lk la lr) k a r)
+      ll
+  insertRrl l k a rl rk ra rr =
+    map
+      (B (B l k a E) k0 a0 (B E rk ra rr))
+      (\rll rlk rla rlr _ _ -> R l k a (B (insertL rll rlk rla rlr) rk ra rr))
+      ( \rll rlk rla rlr _ _ ->
+          let rl' = insertB rll rlk rla rlr
+           in map
+                (error "Map.insert: L8")
+                ( \rll' rlk' rla' rlr' _ _ ->
+                    B
+                      (B l k a rll')
+                      rlk'
+                      rla'
+                      (R rlr' rk ra rr)
+                )
+                (\_ _ _ _ _ _ -> R l k a (B rl' rk ra rr))
+                ( \rll' rlk' rla' rlr' _ _ ->
+                    B
+                      (L l k a rll')
+                      rlk'
+                      rla'
+                      (B rlr' rk ra rr)
+                )
+                rl'
+      )
+      (\rll rlk rla rlr _ _ -> R l k a (B (insertR rll rlk rla rlr) rk ra rr))
+      rl
+  insertLlr ll lk la lr k a r =
+    map
+      (B (B ll lk la E) k0 a0 (B E k a r))
+      (\lrl lrk lra lrr _ _ -> L (B ll lk la (insertL lrl lrk lra lrr)) k a r)
+      ( \lrl lrk lra lrr _ _ ->
+          let lr' = insertB lrl lrk lra lrr
+           in map
+                (error "Map.insert: L9")
+                ( \lrl' lrk' lra' lrr' _ _ ->
+                    B
+                      (B ll lk la lrl')
+                      lrk'
+                      lra'
+                      (R lrr' k a r)
+                )
+                (\_ _ _ _ _ _ -> L (B ll lk la lr') k a r)
+                ( \lrl' lrk' lra' lrr' _ _ ->
+                    B
+                      (L ll lk la lrl')
+                      lrk'
+                      lra'
+                      (B lrr' k a r)
+                )
+                lr'
+      )
+      (\lrl lrk lra lrr _ _ -> L (B ll lk la (insertR lrl lrk lra lrr)) k a r)
+      lr
+
+{- | \(O(\log n)\) From an operation, a key and a map to the map updated by
+applying the operation to the value associated with the key (setting if
+'Just', deleting if 'Nothing')
+-}
+update :: (Ord k) => (a -> Maybe a) -> k -> Map k a -> Map k a
+update f k t =
+  maybe
+    t
+    ( maybe
+        (delete k t)
+        (\a -> insert k a t)
+        . f
+    )
+    $ lookup k t
+
+{-
+ - Query
+ -}
+
+{- | \(O(n \log n)\) From a map and another map to whether the former is a
+submap of the latter (matching on keys and values)
+-}
+isSubmapOf :: (Ord k, Eq a) => Map k a -> Map k a -> Bool
+isSubmapOf p q =
+  foldrWithKey
+    (\k a b -> maybe False ((&& b) . (== a)) $ lookup k q)
+    True
+    p
+
+{- | \(O(\log n)\) From a key and a map to the value associated with the key in
+the map
+-}
+lookup :: (Ord k) => k -> Map k a -> Maybe a
+lookup k = map Nothing go go go
+ where
+  go _ k' a _ recl recr = case compare k k' of
+    LT -> recl
+    EQ -> Just a
+    GT -> recr
+
+{- | \(O(\log n)\) From a map to the value associated with the maximum key in
+the map
+-}
+lookupMax :: Map k a -> Maybe a
+lookupMax = map Nothing go go go
+ where
+  go _ _ a r _ recr = map (Just a) go' go' go' r where go' _ _ _ _ _ _ = recr
+
+{- | \(O(\log n)\) From a map to the value associated with the minimum key in
+the map
+-}
+lookupMin :: Map k a -> Maybe a
+lookupMin = map Nothing go go go
+ where
+  go l _ a _ recl _ = map (Just a) go' go' go' l where go' _ _ _ _ _ _ = recl
+
+-- | \(O(\log n)\) From a key and a map to whether the key is in the map
+member :: (Ord k) => k -> Map k a -> Bool
+member k = map False go go go
+ where
+  go _ k' _ _ recl recr = case compare k k' of
+    LT -> recl
+    EQ -> True
+    GT -> recr
+
+-- | \(O(1)\) From a map to whether the map is empty
+null :: Map k a -> Bool
+null = map True go go go where go _ _ _ _ _ _ = False
+
+-- | \(O(n)\) From a map to the size of the map
+size :: Map k a -> Int
+size =
+  map
+    0
+    (\_ _ _ _ recl recr -> 1 + recl + recr)
+    (\_ _ _ _ recl recr -> 1 + recl + recr)
+    (\_ _ _ _ recl recr -> 1 + recl + recr)
+
+{-
+ - Traversal
+ -}
+
+{- | \(O(n)\) From a lifting operation on keys and values and a map to a lifted
+map
+-}
+traverseWithKey :: (Applicative f) => (k -> a -> f b) -> Map k a -> f (Map k b)
+traverseWithKey f =
+  map
+    (pure E)
+    (\_ k a _ recl recr -> L <$> recl <*> pure k <*> f k a <*> recr)
+    (\_ k a _ recl recr -> B <$> recl <*> pure k <*> f k a <*> recr)
+    (\_ k a _ recl recr -> R <$> recl <*> pure k <*> f k a <*> recr)
+
+{-
+ - Validation
+ -}
+
+{- | \(O(n)\) From a map to whether its internal structure is valid, i.e.
+height-balanced and ordered
+-}
+valid :: (Ord k) => Map k a -> Bool
+valid = liftM2 (&&) balanced ordered
+ where
+  balanced =
+    map
+      True
+      (\l _ _ r recl recr -> levels l - levels r == 1 && recl && recr)
+      (\l _ _ r recl recr -> levels l - levels r == 0 && recl && recr)
+      (\l _ _ r recl recr -> levels r - levels l == 1 && recl && recr)
+  levels = map 0 go go go where go _ _ _ _ recl recr = 1 + max recl recr :: Int
+  ordered = map True go go go
+   where
+    go l k _ r recl recr =
+      map
+        True
+        (\_ lk _ _ _ _ -> lk < k && recl && recr)
+        (\_ lk _ _ _ _ -> lk < k && recl && recr)
+        (\_ lk _ _ _ _ -> lk < k && recl && recr)
+        l
+        && map
+          True
+          (\_ rk _ _ _ _ -> rk > k && recl && recr)
+          (\_ rk _ _ _ _ -> rk > k && recl && recr)
+          (\_ rk _ _ _ _ -> rk > k && recl && recr)
+          r
diff --git a/Mini/Data/Set.hs b/Mini/Data/Set.hs
new file mode 100644
--- /dev/null
+++ b/Mini/Data/Set.hs
@@ -0,0 +1,830 @@
+{-# LANGUAGE LambdaCase #-}
+
+{- | Representation of a structure containing unique elements. The internal
+structure is an AVL tree.
+-}
+module Mini.Data.Set (
+  -- * Type
+  Set,
+
+  -- * Combination
+  difference,
+  intersection,
+  union,
+
+  -- * Construction
+  empty,
+  fromList,
+  singleton,
+
+  -- * Conversion
+  toAscList,
+  toDescList,
+
+  -- * Modification
+  delete,
+  filter,
+  insert,
+
+  -- * Query
+  isSubsetOf,
+  lookupMax,
+  lookupMin,
+  member,
+  null,
+  size,
+
+  -- * Validation
+  valid,
+) where
+
+import Control.Monad (
+  liftM2,
+ )
+import Data.Bifunctor (
+  first,
+ )
+import Data.Bool (
+  bool,
+ )
+import Prelude hiding (
+  filter,
+  null,
+ )
+
+{-
+ - Type
+ -}
+
+{- | A set containing elements of type /a/.
+
+The internal structure is an AVL tree; a tree that is always height-balanced
+(the absolute value of the level difference between the left and right
+subtrees is at most 1).
+-}
+data Set a
+  = -- | Empty node
+    E
+  | -- | Left-heavy node
+    L (Set a) a (Set a)
+  | -- | Balanced node
+    B (Set a) a (Set a)
+  | -- | Right-heavy node
+    R (Set a) a (Set a)
+  deriving (Eq, Ord)
+
+instance (Show a) => Show (Set a) where
+  show = curl . set [] go go go
+   where
+    go _ a _ recl recr = recl <> show a <> "," <> recr
+    curl = wrap "{" "}" . removeTrailingComma
+    wrap open close s = open <> s <> close
+    removeTrailingComma = \case
+      [] -> []
+      [_] -> []
+      (c : cs) -> c : removeTrailingComma cs
+
+instance Foldable Set where
+  foldr f b = set b go go go where go _ a r recl _ = foldr f (f a recl) r
+
+{-
+ - Primitive recursion
+ -}
+
+-- | Primitive recursion on sets
+set
+  :: b
+  -- ^ Empty node
+  -> (Set a -> a -> Set a -> b -> b -> b)
+  -- ^ Left-heavy node: left child, element, right child, left recursion, right
+  -- recursion
+  -> (Set a -> a -> Set a -> b -> b -> b)
+  -- ^ Balanced node: left child, element, right child, left recursion, right
+  -- recursion
+  -> (Set a -> a -> Set a -> b -> b -> b)
+  -- ^ Right-heavy node: left child, element, right child, left recursion, right
+  -- recursion
+  -> Set a
+  -- ^ Set
+  -> b
+set e _ _ _ E = e
+set e f g h (L l a r) = f l a r (set e f g h l) (set e f g h r)
+set e f g h (B l a r) = g l a r (set e f g h l) (set e f g h r)
+set e f g h (R l a r) = h l a r (set e f g h l) (set e f g h r)
+
+{-
+ - Combination
+ -}
+
+-- | \(O(n \log n)\) Set difference
+difference :: (Ord a) => Set a -> Set a -> Set a
+difference = foldr delete
+
+-- | \(O(n \log n)\) Set intersection
+intersection :: (Ord a) => Set a -> Set a -> Set a
+intersection t = foldr (\a b -> bool b (insert a b) (a `member` t)) empty
+
+-- | \(O(n \log n)\) Set union
+union :: (Ord a) => Set a -> Set a -> Set a
+union = foldr insert
+
+{-
+ - Construction
+ -}
+
+-- | \(O(1)\) The empty set
+empty :: Set a
+empty = E
+
+{- | \(O(n \log n)\) From a tail-biased list of elements to a set containing the
+elements
+-}
+fromList :: (Ord a) => [a] -> Set a
+fromList = foldl (flip insert) empty
+
+-- | \(O(1)\) From an element to a set with a single element
+singleton :: a -> Set a
+singleton a = B E a E
+
+{-
+ - Conversion
+ -}
+
+-- | \(O(n)\) From a set to a list of elements in ascending order
+toAscList :: Set a -> [a]
+toAscList = foldl (flip (:)) []
+
+-- | \(O(n)\) From a set to a list of elements in descending order
+toDescList :: Set a -> [a]
+toDescList = foldr (:) []
+
+{-
+ - Modification
+ -}
+
+-- | \(O(\log n)\) From an element and a set to the set without the element
+delete :: (Ord a) => a -> Set a -> Set a
+delete a0 t = bool t (go t) (a0 `member` t)
+ where
+  go =
+    set
+      (error "Set.delete: L0")
+      ( \l a r _ _ ->
+          case compare a0 a of
+            LT -> deleteLl l a r
+            EQ -> substituteL l r
+            GT -> deleteLr l a r
+      )
+      ( \l a r _ _ ->
+          case compare a0 a of
+            LT -> deleteBl l a r
+            EQ -> substituteBr l r
+            GT -> deleteBr l a r
+      )
+      ( \l a r _ _ ->
+          case compare a0 a of
+            LT -> deleteRl l a r
+            EQ -> substituteR l r
+            GT -> deleteRr l a r
+      )
+  deleteRl l a r =
+    set
+      (error "Set.delete: L1")
+      ( \ll la lr _ _ ->
+          case compare a0 la of
+            LT -> checkLeftR (deleteLl ll la lr) a r
+            EQ -> checkLeftR (substituteL ll lr) a r
+            GT -> checkLeftR (deleteLr ll la lr) a r
+      )
+      ( \ll la lr _ _ ->
+          case compare a0 la of
+            LT -> R (deleteBl ll la lr) a r
+            EQ -> checkLeftR' (substituteBr ll lr) a r
+            GT -> R (deleteBr ll la lr) a r
+      )
+      ( \ll la lr _ _ ->
+          case compare a0 la of
+            LT -> checkLeftR (deleteRl ll la lr) a r
+            EQ -> checkLeftR (substituteR ll lr) a r
+            GT -> checkLeftR (deleteRr ll la lr) a r
+      )
+      l
+  deleteRr l a =
+    set
+      (error "Set.delete: L2")
+      ( \rl ra rr _ _ ->
+          case compare a0 ra of
+            LT -> checkRightR l a (deleteLl rl ra rr)
+            EQ -> checkRightR l a (substituteL rl rr)
+            GT -> checkRightR l a (deleteLr rl ra rr)
+      )
+      ( \rl ra rr _ _ ->
+          case compare a0 ra of
+            LT -> R l a (deleteBl rl ra rr)
+            EQ -> checkRightR' l a (substituteBl rl rr)
+            GT -> R l a (deleteBr rl ra rr)
+      )
+      ( \rl ra rr _ _ ->
+          case compare a0 ra of
+            LT -> checkRightR l a (deleteRl rl ra rr)
+            EQ -> checkRightR l a (substituteR rl rr)
+            GT -> checkRightR l a (deleteRr rl ra rr)
+      )
+  deleteBl l a r =
+    set
+      (error "Set.delete: L3")
+      ( \ll la lr _ _ ->
+          case compare a0 la of
+            LT -> checkLeftB (deleteLl ll la lr) a r
+            EQ -> checkLeftB (substituteL ll lr) a r
+            GT -> checkLeftB (deleteLr ll la lr) a r
+      )
+      ( \ll la lr _ _ ->
+          case compare a0 la of
+            LT -> B (deleteBl ll la lr) a r
+            EQ -> checkLeftB' (substituteBr ll lr) a r
+            GT -> B (deleteBr ll la lr) a r
+      )
+      ( \ll la lr _ _ ->
+          case compare a0 la of
+            LT -> checkLeftB (deleteRl ll la lr) a r
+            EQ -> checkLeftB (substituteR ll lr) a r
+            GT -> checkLeftB (deleteRr ll la lr) a r
+      )
+      l
+  deleteBr l a =
+    set
+      (error "Set.delete: L4")
+      ( \rl ra rr _ _ ->
+          case compare a0 ra of
+            LT -> checkRightB l a (deleteLl rl ra rr)
+            EQ -> checkRightB l a (substituteL rl rr)
+            GT -> checkRightB l a (deleteLr rl ra rr)
+      )
+      ( \rl ra rr _ _ ->
+          case compare a0 ra of
+            LT -> B l a (deleteBl rl ra rr)
+            EQ -> checkRightB' l a (substituteBl rl rr)
+            GT -> B l a (deleteBr rl ra rr)
+      )
+      ( \rl ra rr _ _ ->
+          case compare a0 ra of
+            LT -> checkRightB l a (deleteRl rl ra rr)
+            EQ -> checkRightB l a (substituteR rl rr)
+            GT -> checkRightB l a (deleteRr rl ra rr)
+      )
+  deleteLl l a r =
+    set
+      (error "Set.delete: L5")
+      ( \ll la lr _ _ ->
+          case compare a0 la of
+            LT -> checkLeftL (deleteLl ll la lr) a r
+            EQ -> checkLeftL (substituteL ll lr) a r
+            GT -> checkLeftL (deleteLr ll la lr) a r
+      )
+      ( \ll la lr _ _ ->
+          case compare a0 la of
+            LT -> L (deleteBl ll la lr) a r
+            EQ -> checkLeftL' (substituteBr ll lr) a r
+            GT -> L (deleteBr ll la lr) a r
+      )
+      ( \ll la lr _ _ ->
+          case compare a0 la of
+            LT -> checkLeftL (deleteRl ll la lr) a r
+            EQ -> checkLeftL (substituteR ll lr) a r
+            GT -> checkLeftL (deleteRr ll la lr) a r
+      )
+      l
+  deleteLr l a =
+    set
+      (error "Set.delete: L6")
+      ( \rl ra rr _ _ ->
+          case compare a0 ra of
+            LT -> checkRightL l a (deleteLl rl ra rr)
+            EQ -> checkRightL l a (substituteL rl rr)
+            GT -> checkRightL l a (deleteLr rl ra rr)
+      )
+      ( \rl ra rr _ _ ->
+          case compare a0 ra of
+            LT -> L l a (deleteBl rl ra rr)
+            EQ -> checkRightL' l a (substituteBl rl rr)
+            GT -> L l a (deleteBr rl ra rr)
+      )
+      ( \rl ra rr _ _ ->
+          case compare a0 ra of
+            LT -> checkRightL l a (deleteRl rl ra rr)
+            EQ -> checkRightL l a (substituteR rl rr)
+            GT -> checkRightL l a (deleteRr rl ra rr)
+      )
+  rebalanceR l a =
+    set
+      (error "Set.delete: L7")
+      ( \rl ra rr _ _ ->
+          set
+            (error "Set.delete: L8")
+            (\rll rla rlr _ _ -> B (B l a rll) rla (R rlr ra rr))
+            (\rll rla rlr _ _ -> B (B l a rll) rla (B rlr ra rr))
+            (\rll rla rlr _ _ -> B (L l a rll) rla (B rlr ra rr))
+            rl
+      )
+      (\rl ra rr _ _ -> L (R l a rl) ra rr)
+      (\rl ra rr _ _ -> B (B l a rl) ra rr)
+  rebalanceL l a r =
+    set
+      (error "Set.delete: L9")
+      (\ll la lr _ _ -> B ll la (B lr a r))
+      (\ll la lr _ _ -> R ll la (L lr a r))
+      ( \ll la lr _ _ ->
+          set
+            (error "Set.delete: L10")
+            (\lrl lra lrr _ _ -> B (B ll la lrl) lra (R lrr a r))
+            (\lrl lra lrr _ _ -> B (B ll la lrl) lra (B lrr a r))
+            (\lrl lra lrr _ _ -> B (L ll la lrl) lra (B lrr a r))
+            lr
+      )
+      l
+  checkLeftR l a r =
+    set
+      (error "Set.delete: L11")
+      (\_ _ _ _ _ -> R l a r)
+      (\_ _ _ _ _ -> rebalanceR l a r)
+      (\_ _ _ _ _ -> R l a r)
+      l
+  checkLeftB l a r =
+    set
+      (error "Set.delete: L12")
+      (\_ _ _ _ _ -> B l a r)
+      (\_ _ _ _ _ -> R l a r)
+      (\_ _ _ _ _ -> B l a r)
+      l
+  checkLeftL l a r =
+    set
+      (error "Set.delete: L13")
+      (\_ _ _ _ _ -> L l a r)
+      (\_ _ _ _ _ -> B l a r)
+      (\_ _ _ _ _ -> L l a r)
+      l
+  checkRightR l a r =
+    set
+      (error "Set.delete: L14")
+      (\_ _ _ _ _ -> R l a r)
+      (\_ _ _ _ _ -> B l a r)
+      (\_ _ _ _ _ -> R l a r)
+      r
+  checkRightB l a r =
+    set
+      (error "Set.delete: L15")
+      (\_ _ _ _ _ -> B l a r)
+      (\_ _ _ _ _ -> L l a r)
+      (\_ _ _ _ _ -> B l a r)
+      r
+  checkRightL l a r =
+    set
+      (error "Set.delete: L16")
+      (\_ _ _ _ _ -> L l a r)
+      (\_ _ _ _ _ -> rebalanceL l a r)
+      (\_ _ _ _ _ -> L l a r)
+      r
+  substituteR l =
+    set
+      (error "Set.delete: L17")
+      (\rl ra rr _ _ -> uncurry (checkRightR l) $ popLeftL rl ra rr)
+      (\rl ra rr _ _ -> uncurry (checkRightR' l) $ popLeftB rl ra rr)
+      (\rl ra rr _ _ -> uncurry (checkRightR l) $ popLeftR rl ra rr)
+  substituteBr l =
+    set
+      E
+      (\rl ra rr _ _ -> uncurry (checkRightB l) $ popLeftL rl ra rr)
+      (\rl ra rr _ _ -> uncurry (checkRightB' l) $ popLeftB rl ra rr)
+      (\rl ra rr _ _ -> uncurry (checkRightB l) $ popLeftR rl ra rr)
+  substituteBl l r =
+    set
+      E
+      (\ll la lr _ _ -> (\(l', a) -> checkLeftB l' a r) $ popRightL ll la lr)
+      (\ll la lr _ _ -> (\(l', a) -> checkLeftB' l' a r) $ popRightB ll la lr)
+      (\ll la lr _ _ -> (\(l', a) -> checkLeftB l' a r) $ popRightR ll la lr)
+      l
+  substituteL l r =
+    set
+      (error "Set.delete: L18")
+      (\ll la lr _ _ -> (\(l', a) -> checkLeftL l' a r) $ popRightL ll la lr)
+      (\ll la lr _ _ -> (\(l', a) -> checkLeftL' l' a r) $ popRightB ll la lr)
+      (\ll la lr _ _ -> (\(l', a) -> checkLeftL l' a r) $ popRightR ll la lr)
+      l
+  checkLeftR' l a r =
+    set
+      (rebalanceR l a r)
+      (\_ _ _ _ _ -> R l a r)
+      (\_ _ _ _ _ -> R l a r)
+      (\_ _ _ _ _ -> R l a r)
+      l
+  checkLeftB' l a r =
+    set
+      (R l a r)
+      (\_ _ _ _ _ -> B l a r)
+      (\_ _ _ _ _ -> B l a r)
+      (\_ _ _ _ _ -> B l a r)
+      l
+  checkLeftL' l a r =
+    set
+      (B l a r)
+      (\_ _ _ _ _ -> L l a r)
+      (\_ _ _ _ _ -> L l a r)
+      (\_ _ _ _ _ -> L l a r)
+      l
+  checkRightR' l a r =
+    set
+      (B l a r)
+      (\_ _ _ _ _ -> R l a r)
+      (\_ _ _ _ _ -> R l a r)
+      (\_ _ _ _ _ -> R l a r)
+      r
+  checkRightB' l a r =
+    set
+      (L l a r)
+      (\_ _ _ _ _ -> B l a r)
+      (\_ _ _ _ _ -> B l a r)
+      (\_ _ _ _ _ -> B l a r)
+      r
+  checkRightL' l a r =
+    set
+      (rebalanceL l a r)
+      (\_ _ _ _ _ -> L l a r)
+      (\_ _ _ _ _ -> L l a r)
+      (\_ _ _ _ _ -> L l a r)
+      r
+  popLeftR l a r =
+    set
+      (a, r)
+      ( \ll la lr _ _ ->
+          (\(a', l') -> (a', checkLeftR l' a r)) $
+            popLeftL ll la lr
+      )
+      (\ll la lr _ _ -> popLeftRB ll la lr a r)
+      ( \ll la lr _ _ ->
+          (\(a', l') -> (a', checkLeftR l' a r)) $
+            popLeftR ll la lr
+      )
+      l
+  popLeftB l a r =
+    set
+      (a, E)
+      (\ll la lr _ _ -> popLeftBL ll la lr a r)
+      (\ll la lr _ _ -> popLeftBB ll la lr a r)
+      (\ll la lr _ _ -> popLeftBR ll la lr a r)
+      l
+  popLeftL l a r =
+    set
+      (error "Set.delete: L19")
+      ( \ll la lr _ _ ->
+          (\(a', l') -> (a', checkLeftL l' a r)) $
+            popLeftL ll la lr
+      )
+      (\ll la lr _ _ -> popLeftLB ll la lr a r)
+      ( \ll la lr _ _ ->
+          (\(a', l') -> (a', checkLeftL l' a r)) $
+            popLeftR ll la lr
+      )
+      l
+  popLeftRB ll la lr a r =
+    set
+      (la, rebalanceR E a r)
+      ( \lll lla llr _ _ ->
+          (\(a', l) -> (a', R l a r)) $
+            popLeftBL lll lla llr la lr
+      )
+      ( \lll lla llr _ _ ->
+          (\(a', l) -> (a', R l a r)) $
+            popLeftBB lll lla llr la lr
+      )
+      ( \lll lla llr _ _ ->
+          (\(a', l) -> (a', R l a r)) $
+            popLeftBR lll lla llr la lr
+      )
+      ll
+  popLeftBB ll la lr a r =
+    set
+      (la, R E a r)
+      ( \lll lla llr _ _ ->
+          (\(a', l) -> (a', B l a r)) $
+            popLeftBL lll lla llr la lr
+      )
+      ( \lll lla llr _ _ ->
+          (\(a', l) -> (a', B l a r)) $
+            popLeftBB lll lla llr la lr
+      )
+      ( \lll lla llr _ _ ->
+          (\(a', l) -> (a', B l a r)) $
+            popLeftBR lll lla llr la lr
+      )
+      ll
+  popLeftLB ll la lr a r =
+    set
+      (la, B E a E)
+      ( \lll lla llr _ _ ->
+          (\(a', l) -> (a', L l a r)) $
+            popLeftBL lll lla llr la lr
+      )
+      ( \lll lla llr _ _ ->
+          (\(a', l) -> (a', L l a r)) $
+            popLeftBB lll lla llr la lr
+      )
+      ( \lll lla llr _ _ ->
+          (\(a', l) -> (a', L l a r)) $
+            popLeftBR lll lla llr la lr
+      )
+      ll
+  popLeftBR ll la lr a r =
+    (\(a', l) -> (a', checkLeftB l a r)) $
+      popLeftR ll la lr
+  popLeftBL ll la lr a r =
+    (\(a', l) -> (a', checkLeftB l a r)) $
+      popLeftL ll la lr
+  popRightR l a =
+    set
+      (error "Set.delete: L20")
+      (\rl ra rr _ _ -> first (checkRightR l a) $ popRightL rl ra rr)
+      (\rl ra rr _ _ -> popRightRB l a rl ra rr)
+      (\rl ra rr _ _ -> first (checkRightR l a) $ popRightR rl ra rr)
+  popRightB l a =
+    set
+      (E, a)
+      (\rl ra rr _ _ -> popRightBL l a rl ra rr)
+      (\rl ra rr _ _ -> popRightBB l a rl ra rr)
+      (\rl ra rr _ _ -> popRightBR l a rl ra rr)
+  popRightL l a =
+    set
+      (l, a)
+      (\rl ra rr _ _ -> first (checkRightL l a) $ popRightL rl ra rr)
+      (\rl ra rr _ _ -> popRightLB l a rl ra rr)
+      (\rl ra rr _ _ -> first (checkRightL l a) $ popRightR rl ra rr)
+  popRightRB l a rl ra =
+    set
+      (B E a E, ra)
+      (\rrl rra rrr _ _ -> first (R l a) $ popRightBL rl ra rrl rra rrr)
+      (\rrl rra rrr _ _ -> first (R l a) $ popRightBB rl ra rrl rra rrr)
+      (\rrl rra rrr _ _ -> first (R l a) $ popRightBR rl ra rrl rra rrr)
+  popRightBB l a rl ra =
+    set
+      (L l a E, ra)
+      (\rrl rra rrr _ _ -> first (B l a) $ popRightBL rl ra rrl rra rrr)
+      (\rrl rra rrr _ _ -> first (B l a) $ popRightBB rl ra rrl rra rrr)
+      (\rrl rra rrr _ _ -> first (B l a) $ popRightBR rl ra rrl rra rrr)
+  popRightLB l a rl ra =
+    set
+      (rebalanceL l a E, ra)
+      (\rrl rra rrr _ _ -> first (L l a) $ popRightBL rl ra rrl rra rrr)
+      (\rrl rra rrr _ _ -> first (L l a) $ popRightBB rl ra rrl rra rrr)
+      (\rrl rra rrr _ _ -> first (L l a) $ popRightBR rl ra rrl rra rrr)
+  popRightBR l a rl ra rr = first (checkRightB l a) $ popRightR rl ra rr
+  popRightBL l a rl ra rr = first (checkRightB l a) $ popRightL rl ra rr
+
+{- | \(O(n)\) From a predicate and a set to the set with elements satisfying the
+predicate
+-}
+filter :: (Ord a) => (a -> Bool) -> Set a -> Set a
+filter p = foldr (\a b -> bool b (insert a b) (p a)) empty
+
+-- | \(O(\log n)\) From an element and a set to the set including the element
+insert :: (Ord a) => a -> Set a -> Set a
+insert a0 =
+  set
+    (B E a0 E)
+    (\l a r _ _ -> insertL l a r)
+    (\l a r _ _ -> insertB l a r)
+    (\l a r _ _ -> insertR l a r)
+ where
+  insertR l a r =
+    case compare a0 a of
+      LT -> insertRl l a r
+      EQ -> R l a r
+      GT -> insertRr l a r
+  insertB l a r =
+    case compare a0 a of
+      LT -> insertBl l a r
+      EQ -> B l a r
+      GT -> insertBr l a r
+  insertL l a r =
+    case compare a0 a of
+      LT -> insertLl l a r
+      EQ -> L l a r
+      GT -> insertLr l a r
+  insertRl l a r =
+    set
+      (B (B E a0 E) a r)
+      (\ll la lr _ _ -> R (insertL ll la lr) a r)
+      ( \ll la lr _ _ ->
+          let l' = insertB ll la lr
+           in set
+                (error "Set.insert: L0")
+                (\_ _ _ _ _ -> B l' a r)
+                (\_ _ _ _ _ -> R l' a r)
+                (\_ _ _ _ _ -> B l' a r)
+                l'
+      )
+      (\ll la lr _ _ -> R (insertR ll la lr) a r)
+      l
+  insertBl l a r =
+    set
+      (L (B E a0 E) a r)
+      (\ll la lr _ _ -> B (insertL ll la lr) a r)
+      ( \ll la lr _ _ ->
+          let l' = insertB ll la lr
+           in set
+                (error "Set.insert: L1")
+                (\_ _ _ _ _ -> L l' a r)
+                (\_ _ _ _ _ -> B l' a r)
+                (\_ _ _ _ _ -> L l' a r)
+                l'
+      )
+      (\ll la lr _ _ -> B (insertR ll la lr) a r)
+      l
+  insertBr l a =
+    set
+      (R l a (B E a0 E))
+      (\rl ra rr _ _ -> B l a (insertL rl ra rr))
+      ( \rl ra rr _ _ ->
+          let r = insertB rl ra rr
+           in set
+                (error "Set.insert: L2")
+                (\_ _ _ _ _ -> R l a r)
+                (\_ _ _ _ _ -> B l a r)
+                (\_ _ _ _ _ -> R l a r)
+                r
+      )
+      (\rl ra rr _ _ -> B l a (insertR rl ra rr))
+  insertLr l a =
+    set
+      (B l a (B E a0 E))
+      (\rl ra rr _ _ -> L l a (insertL rl ra rr))
+      ( \rl ra rr _ _ ->
+          let r = insertB rl ra rr
+           in set
+                (error "Set.insert: L3")
+                (\_ _ _ _ _ -> B l a r)
+                (\_ _ _ _ _ -> L l a r)
+                (\_ _ _ _ _ -> B l a r)
+                r
+      )
+      (\rl ra rr _ _ -> L l a (insertR rl ra rr))
+  insertRr l a =
+    set
+      (error "Set.insert: L4")
+      (\rl ra rr _ _ -> R l a (insertL rl ra rr))
+      ( \rl ra rr _ _ ->
+          case compare a0 ra of
+            LT -> insertRrl l a rl ra rr
+            EQ -> R l a (B rl ra rr)
+            GT -> insertRrr l a rl ra rr
+      )
+      (\rl ra rr _ _ -> R l a (insertR rl ra rr))
+  insertLl l a r =
+    set
+      (error "Set.insert: L5")
+      (\ll la lr _ _ -> L (insertL ll la lr) a r)
+      ( \ll la lr _ _ ->
+          case compare a0 la of
+            LT -> insertLll ll la lr a r
+            EQ -> L (B ll la lr) a r
+            GT -> insertLlr ll la lr a r
+      )
+      (\ll la lr _ _ -> L (insertR ll la lr) a r)
+      l
+  insertRrr l a rl ra =
+    set
+      (B (B l a rl) ra (B E a0 E))
+      (\rrl rra rrr _ _ -> R l a (B rl ra (insertL rrl rra rrr)))
+      ( \rrl rra rrr _ _ ->
+          let rr = insertB rrl rra rrr
+           in set
+                (error "Set.insert: L6")
+                (\_ _ _ _ _ -> B (B l a rl) ra rr)
+                (\_ _ _ _ _ -> R l a (B rl ra rr))
+                (\_ _ _ _ _ -> B (B l a rl) ra rr)
+                rr
+      )
+      (\rrl rra rrr _ _ -> R l a (B rl ra (insertR rrl rra rrr)))
+  insertLll ll la lr a r =
+    set
+      (B (B E a0 E) la (B lr a r))
+      (\lll lla llr _ _ -> L (B (insertL lll lla llr) la lr) a r)
+      ( \lll lla llr _ _ ->
+          let ll' = insertB lll lla llr
+           in set
+                (error "Set.insert: L7")
+                (\_ _ _ _ _ -> B ll' la (B lr a r))
+                (\_ _ _ _ _ -> L (B ll' la lr) a r)
+                (\_ _ _ _ _ -> B ll' la (B lr a r))
+                ll'
+      )
+      (\lll lla llr _ _ -> L (B (insertR lll lla llr) la lr) a r)
+      ll
+  insertRrl l a rl ra rr =
+    set
+      (B (B l a E) a0 (B E ra rr))
+      (\rll rla rlr _ _ -> R l a (B (insertL rll rla rlr) ra rr))
+      ( \rll rla rlr _ _ ->
+          let rl' = insertB rll rla rlr
+           in set
+                (error "Set.insert: L8")
+                (\rll' rla' rlr' _ _ -> B (B l a rll') rla' (R rlr' ra rr))
+                (\_ _ _ _ _ -> R l a (B rl' ra rr))
+                (\rll' rla' rlr' _ _ -> B (L l a rll') rla' (B rlr' ra rr))
+                rl'
+      )
+      (\rll rla rlr _ _ -> R l a (B (insertR rll rla rlr) ra rr))
+      rl
+  insertLlr ll la lr a r =
+    set
+      (B (B ll la E) a0 (B E a r))
+      (\lrl lra lrr _ _ -> L (B ll la (insertL lrl lra lrr)) a r)
+      ( \lrl lra lrr _ _ ->
+          let lr' = insertB lrl lra lrr
+           in set
+                (error "Set.insert: L9")
+                (\lrl' lra' lrr' _ _ -> B (B ll la lrl') lra' (R lrr' a r))
+                (\_ _ _ _ _ -> L (B ll la lr') a r)
+                (\lrl' lra' lrr' _ _ -> B (L ll la lrl') lra' (B lrr' a r))
+                lr'
+      )
+      (\lrl lra lrr _ _ -> L (B ll la (insertR lrl lra lrr)) a r)
+      lr
+
+{-
+ - Query
+ -}
+
+{- | \(O(n \log n)\) From a set and another set to whether the former is a
+subset of the latter
+-}
+isSubsetOf :: (Ord a) => Set a -> Set a -> Bool
+isSubsetOf p q = foldr (\a b -> a `member` q && b) True p
+
+-- | \(O(\log n)\) From a set to the maximum element of the set
+lookupMax :: Set a -> Maybe a
+lookupMax = set Nothing go go go
+ where
+  go _ a r _ recr = set (Just a) go' go' go' r where go' _ _ _ _ _ = recr
+
+-- | \(O(\log n)\) From a set to the minimum element of the set
+lookupMin :: Set a -> Maybe a
+lookupMin = set Nothing go go go
+ where
+  go l a _ recl _ = set (Just a) go' go' go' l where go' _ _ _ _ _ = recl
+
+{- | \(O(\log n)\) From an element and a set to whether the element is in the
+set
+-}
+member :: (Ord a) => a -> Set a -> Bool
+member a = set False go go go
+ where
+  go _ a' _ recl recr = case compare a a' of
+    LT -> recl
+    EQ -> True
+    GT -> recr
+
+-- | \(O(1)\) From a set to whether the set is empty
+null :: Set a -> Bool
+null = set True go go go where go _ _ _ _ _ = False
+
+-- | \(O(n)\) From a set to the size of the set
+size :: Set a -> Int
+size =
+  set
+    0
+    (\_ _ _ recl recr -> 1 + recl + recr)
+    (\_ _ _ recl recr -> 1 + recl + recr)
+    (\_ _ _ recl recr -> 1 + recl + recr)
+
+{-
+ - Validation
+ -}
+
+{- | \(O(n)\) From a set to whether its internal structure is valid, i.e.
+height-balanced and ordered
+-}
+valid :: (Ord a) => Set a -> Bool
+valid = liftM2 (&&) balanced ordered
+ where
+  balanced =
+    set
+      True
+      (\l _ r recl recr -> levels l - levels r == 1 && recl && recr)
+      (\l _ r recl recr -> levels l - levels r == 0 && recl && recr)
+      (\l _ r recl recr -> levels r - levels l == 1 && recl && recr)
+  levels = set 0 go go go where go _ _ _ recl recr = 1 + max recl recr :: Int
+  ordered = set True go go go
+   where
+    go l a r recl recr =
+      set
+        True
+        (\_ la _ _ _ -> la < a && recl && recr)
+        (\_ la _ _ _ -> la < a && recl && recr)
+        (\_ la _ _ _ -> la < a && recl && recr)
+        l
+        && set
+          True
+          (\_ ra _ _ _ -> ra > a && recl && recr)
+          (\_ ra _ _ _ -> ra > a && recl && recr)
+          (\_ ra _ _ _ -> ra > a && recl && recr)
+          r
diff --git a/Mini/Lens.hs b/Mini/Lens.hs
new file mode 100644
--- /dev/null
+++ b/Mini/Lens.hs
@@ -0,0 +1,100 @@
+{-# LANGUAGE RankNTypes #-}
+
+{- | Minimal library of /van Laarhoven/ lenses: composable polymorphic record
+updates
+-}
+module Mini.Lens (
+  -- * Types
+  Lens,
+
+  -- * Construction
+  lens,
+
+  -- * Reading
+  view,
+
+  -- * Modifying
+  over,
+
+  -- * Writing
+  set,
+) where
+
+import Control.Applicative (
+  Const (
+    Const,
+    getConst
+  ),
+ )
+import Data.Functor.Identity (
+  Identity (
+    Identity,
+    runIdentity
+  ),
+ )
+
+{-
+ - Types
+ -}
+
+{- | A purely functional reference for updating structures of type /s/ with
+fields of type /a/ to structures of type /t/ with fields of type /b/
+-}
+type Lens s t a b = forall f. (Functor f) => (a -> f b) -> (s -> f t)
+
+{-
+ - Construction
+ -}
+
+{- | From a getter and a setter to a lens
+
+> data Foo = Foo { _bar :: Bar } deriving Show
+> data Bar = Bar { _baz :: Int } deriving Show
+>
+> bar :: Lens Foo Foo Bar Bar
+> bar = lens _bar $ \s b -> s { _bar = b }
+>
+> baz :: Lens Bar Bar Int Int
+> baz = lens _baz $ \s b -> s { _baz = b }
+-}
+lens :: (s -> a) -> (s -> b -> t) -> Lens s t a b
+lens sa sbt ab s = sbt s <$> ab (sa s)
+
+{-
+ - Reading
+ -}
+
+{- | From a lens and a structure to the value of the field of the structure
+referenced by the lens
+
+> ghci> view (bar . baz) $ Foo (Bar 73)
+> 73
+-}
+view :: Lens s t a b -> s -> a
+view o = getConst . o Const
+
+{-
+ - Modifying
+ -}
+
+{- | From a lens, an operation and a structure to the structure updated by
+applying the operation to the value of the field referenced by the lens
+
+> ghci> over (bar . baz) (+ 1) $ Foo (Bar 73)
+> Foo {_bar = Bar {_baz = 74}}
+-}
+over :: Lens s t a b -> (a -> b) -> s -> t
+over o ab = runIdentity . o (Identity . ab)
+
+{-
+ - Writing
+ -}
+
+{- | From a lens, a value and a structure to the structure updated by setting
+the field referenced by the lens to the value
+
+> ghci> set (bar . baz) 21 $ Foo (Bar 73)
+> Foo {_bar = Bar {_baz = 21}}
+-}
+set :: Lens s t a b -> b -> s -> t
+set o b = runIdentity . o (const $ Identity b)
diff --git a/Mini/Transformers/Class.hs b/Mini/Transformers/Class.hs
new file mode 100644
--- /dev/null
+++ b/Mini/Transformers/Class.hs
@@ -0,0 +1,21 @@
+-- | The class of monad transformers
+module Mini.Transformers.Class (
+  -- * Class
+  MonadTrans (
+    lift
+  ),
+) where
+
+{-
+ - Class
+ -}
+
+{- | Instances should satisfy the following laws:
+
+> lift . pure = pure
+
+> lift (m >>= f) = lift m >>= (lift . f)
+-}
+class MonadTrans t where
+  -- | Lift a computation from the inner monad to the transformer monad
+  lift :: (Monad m) => m a -> t m a
diff --git a/Mini/Transformers/EitherT.hs b/Mini/Transformers/EitherT.hs
new file mode 100644
--- /dev/null
+++ b/Mini/Transformers/EitherT.hs
@@ -0,0 +1,91 @@
+{- | Extension of a monad with the 'Either' ability to interrupt a sequence of
+actions and terminate with a value
+-}
+module Mini.Transformers.EitherT (
+  -- * Type
+  EitherT,
+
+  -- * Termination
+  left,
+
+  -- * Anticipation
+  anticipate,
+
+  -- * Runners
+  runEitherT,
+) where
+
+import Control.Applicative (
+  Alternative (
+    empty,
+    (<|>)
+  ),
+ )
+import Control.Monad (
+  ap,
+  liftM,
+  (>=>),
+ )
+import Mini.Transformers.Class (
+  MonadTrans (
+    lift
+  ),
+ )
+
+{-
+ - Type
+ -}
+
+{- | A monad with early termination type /e/, inner monad /m/, and return type
+/a/
+-}
+newtype EitherT e m a = EitherT
+  { runEitherT :: m (Either e a)
+  -- ^ Unwrap an 'EitherT'
+  }
+
+instance (Monad m) => Functor (EitherT e m) where
+  fmap = liftM
+
+instance (Monad m) => Applicative (EitherT e m) where
+  pure = EitherT . pure . Right
+  (<*>) = ap
+
+instance (Monad m, Monoid e) => Alternative (EitherT e m) where
+  empty = EitherT . pure $ Left mempty
+  m <|> n =
+    EitherT $
+      runEitherT m
+        >>= either
+          (\e -> either (Left . mappend e) Right <$> runEitherT n)
+          (pure . Right)
+
+instance (Monad m) => Monad (EitherT e m) where
+  m >>= k =
+    EitherT $
+      runEitherT m
+        >>= either
+          (pure . Left)
+          (runEitherT . k)
+
+instance MonadTrans (EitherT e) where
+  lift = EitherT . fmap Right
+
+{-
+ - Termination
+ -}
+
+-- | Terminate an action sequence with the given value
+left :: (Monad m) => e -> EitherT e m a
+left = EitherT . pure . Left
+
+{-
+ - Anticipation
+ -}
+
+{- | Run the given action and decide what to do depending on the return type
+
+> anticipate foo >>= either bar baz
+-}
+anticipate :: (Monad m) => EitherT e m a -> EitherT e m (Either e a)
+anticipate = lift . runEitherT . (Right <$>) >=> either (pure . Left) pure
diff --git a/Mini/Transformers/ParserT.hs b/Mini/Transformers/ParserT.hs
new file mode 100644
--- /dev/null
+++ b/Mini/Transformers/ParserT.hs
@@ -0,0 +1,192 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE TupleSections #-}
+
+-- | Turning strings into things
+module Mini.Transformers.ParserT (
+  -- * Types
+  ParserT,
+  ParseError,
+
+  -- * Runners
+  runParserT,
+
+  -- * Parsers
+  sat,
+  item,
+  symbol,
+  string,
+  oneOf,
+  noneOf,
+
+  -- * Combinators
+  sepBy,
+  sepBy1,
+  endBy,
+  endBy1,
+  between,
+  option,
+) where
+
+import Control.Applicative (
+  Alternative (
+    empty,
+    many,
+    (<|>)
+  ),
+ )
+import Control.Monad (
+  ap,
+  liftM,
+  (>=>),
+ )
+import Data.Bool (
+  bool,
+ )
+import Data.Functor (
+  (<&>),
+ )
+import Mini.Transformers.Class (
+  MonadTrans (
+    lift
+  ),
+ )
+
+{-
+ - Types
+ -}
+
+{- | A monad for parsing symbols of type /s/ with inner monad /m/ and return
+type /a/
+-}
+newtype ParserT s m a = ParserT
+  { runParserT :: [s] -> m (Either [ParseError s] (a, [s]))
+  -- ^ Unwrap a 'ParserT' given a string of symbols
+  }
+
+instance (Monad m) => Functor (ParserT s m) where
+  fmap = liftM
+
+instance (Monad m) => Applicative (ParserT s m) where
+  pure a = ParserT $ pure . Right . (a,)
+  (<*>) = ap
+
+instance (Monad m, Eq s) => Alternative (ParserT s m) where
+  empty = ParserT . const . pure $ Left [EmptyError]
+  m <|> n = ParserT $ \ss ->
+    runParserT m ss
+      >>= either
+        ( \e1 ->
+            runParserT n ss
+              <&> either
+                (Left . mappend e1)
+                Right
+        )
+        (pure . Right)
+
+instance (Monad m) => Monad (ParserT s m) where
+  m >>= k =
+    ParserT $
+      runParserT m
+        >=> either
+          (pure . Left)
+          (\(a, ss') -> runParserT (k a) ss')
+
+instance MonadTrans (ParserT s) where
+  lift m = ParserT $ \ss -> m <&> Right . (,ss)
+
+-- | Abstract representation of a parse error for symbols of type /s/
+data ParseError s
+  = EndOfInput
+  | Unexpected s
+  | EmptyError
+
+instance (Show s) => Show (ParseError s) where
+  show = \case
+    EndOfInput -> "unexpected EOF"
+    Unexpected s -> "unexpected " <> show s
+    EmptyError -> "empty"
+
+{-
+ - Common Parsers
+ -}
+
+{- | From a predicate to a parser for symbols satisfying the predicate
+
+> digit = sat Data.Char.isDigit
+>
+> spaces = Control.Applicative.many $ sat Data.Char.isSpace
+-}
+sat :: (Applicative m) => (s -> Bool) -> ParserT s m s
+sat p =
+  ParserT $ \case
+    [] -> pure $ Left [EndOfInput]
+    (s : ss) ->
+      bool
+        (pure $ Left [Unexpected s])
+        (pure $ Right (s, ss))
+        $ p s
+
+-- | A parser for any symbol
+item :: (Applicative m) => ParserT s m s
+item = sat $ const True
+
+-- | A parser for the given symbol
+symbol :: (Applicative m, Eq s) => s -> ParserT s m s
+symbol = sat . (==)
+
+-- | A parser for the given string of symbols
+string :: (Monad m, Traversable t, Eq s) => t s -> ParserT s m (t s)
+string = traverse symbol
+
+-- | A parser for any of the given symbols
+oneOf :: (Applicative m, Foldable t, Eq s) => t s -> ParserT s m s
+oneOf = sat . flip elem
+
+-- | A parser for any symbol excluding the given symbols
+noneOf :: (Applicative m, Foldable t, Eq s) => t s -> ParserT s m s
+noneOf = sat . flip notElem
+
+{-
+ - Combinators
+ -}
+
+{- | Turn a parser and another parser into a parser for zero or more of the
+former separated by the latter
+-}
+sepBy :: (Monad m, Eq s) => ParserT s m a -> ParserT s m b -> ParserT s m [a]
+sepBy p = option [] . sepBy1 p
+
+{- | Turn a parser and another parser into a parser for one or more of the
+former separated by the latter
+-}
+sepBy1 :: (Monad m, Eq s) => ParserT s m a -> ParserT s m b -> ParserT s m [a]
+sepBy1 p sep = (:) <$> p <*> many (sep *> p)
+
+{- | Turn a parser and another parser into a parser for zero or more of the
+former separated and ended by the latter
+-}
+endBy :: (Monad m, Eq s) => ParserT s m a -> ParserT s m b -> ParserT s m [a]
+endBy p = option [] . endBy1 p
+
+{- | Turn a parser and another parser into a parser for one or more of the
+former separated and ended by the latter
+-}
+endBy1 :: (Monad m, Eq s) => ParserT s m a -> ParserT s m b -> ParserT s m [a]
+endBy1 p sep = sepBy1 p sep <* sep
+
+{- | Turn a first, second and third parser into a parser for the third enclosed
+between the first and the second, returning the result of the third
+-}
+between
+  :: (Monad m)
+  => ParserT s m open
+  -> ParserT s m close
+  -> ParserT s m a
+  -> ParserT s m a
+between open close p = open *> p <* close
+
+{- | From a default value and a parser to the parser returning the default value
+in case of failure
+-}
+option :: (Monad m, Eq s) => a -> ParserT s m a -> ParserT s m a
+option a p = p <|> pure a
diff --git a/Mini/Transformers/ReaderT.hs b/Mini/Transformers/ReaderT.hs
new file mode 100644
--- /dev/null
+++ b/Mini/Transformers/ReaderT.hs
@@ -0,0 +1,67 @@
+-- | Extension of a monad with a read-only environment
+module Mini.Transformers.ReaderT (
+  -- * Type
+  ReaderT,
+
+  -- * Reading
+  ask,
+
+  -- * Runners
+  runReaderT,
+) where
+
+import Control.Applicative (
+  Alternative (
+    empty,
+    (<|>)
+  ),
+ )
+import Control.Monad (
+  ap,
+  liftM,
+ )
+import Mini.Transformers.Class (
+  MonadTrans (
+    lift
+  ),
+ )
+
+{-
+ - Type
+ -}
+
+-- | A monad with read-only type /r/, inner monad /m/, and return type /a/
+newtype ReaderT r m a = ReaderT
+  { runReaderT :: r -> m a
+  -- ^ Unwrap a 'ReaderT' given a read-only value
+  }
+
+instance (Monad m) => Functor (ReaderT r m) where
+  fmap = liftM
+
+instance (Monad m) => Applicative (ReaderT r m) where
+  pure = ReaderT . const . pure
+  (<*>) = ap
+
+instance (Monad m, Alternative m) => Alternative (ReaderT r m) where
+  empty = ReaderT . const $ empty
+  m <|> n = ReaderT $ \r -> runReaderT m r <|> runReaderT n r
+
+instance (Monad m) => Monad (ReaderT r m) where
+  m >>= k = ReaderT $ \r -> runReaderT m r >>= (`runReaderT` r) . k
+
+instance MonadTrans (ReaderT r) where
+  lift = ReaderT . const
+
+{-
+ - Reading
+ -}
+
+{- | Fetch the read-only value
+
+> foo = do
+>   r <- ask
+>   bar r
+-}
+ask :: (Monad m) => ReaderT r m r
+ask = ReaderT pure
diff --git a/Mini/Transformers/StateT.hs b/Mini/Transformers/StateT.hs
new file mode 100644
--- /dev/null
+++ b/Mini/Transformers/StateT.hs
@@ -0,0 +1,98 @@
+{-# LANGUAGE TupleSections #-}
+
+-- | Extension of a monad with a modifiable environment
+module Mini.Transformers.StateT (
+  -- * Type
+  StateT,
+
+  -- * Reading
+  get,
+
+  -- * Modifying
+  modify,
+
+  -- * Writing
+  put,
+
+  -- * Runners
+  runStateT,
+) where
+
+import Control.Applicative (
+  Alternative (
+    empty,
+    (<|>)
+  ),
+ )
+import Control.Monad (
+  ap,
+  liftM,
+  (>=>),
+ )
+import Data.Functor (
+  (<&>),
+ )
+import Mini.Transformers.Class (
+  MonadTrans (
+    lift
+  ),
+ )
+
+{-
+ - Type
+ -}
+
+-- | A monad with modifiable type /s/, inner monad /m/, and return type /a/
+newtype StateT s m a = StateT
+  { runStateT :: s -> m (a, s)
+  -- ^ Unwrap a 'StateT' given a starting state
+  }
+
+instance (Monad m) => Functor (StateT s m) where
+  fmap = liftM
+
+instance (Monad m) => Applicative (StateT s m) where
+  pure a = StateT $ \s -> pure (a, s)
+  (<*>) = ap
+
+instance (Monad m, Alternative m) => Alternative (StateT s m) where
+  empty = StateT $ const empty
+  m <|> n = StateT $ \s -> runStateT m s <|> runStateT n s
+
+instance (Monad m) => Monad (StateT s m) where
+  m >>= k = StateT $ runStateT m >=> (\(a, s) -> runStateT (k a) s)
+
+instance MonadTrans (StateT s) where
+  lift m = StateT $ \s -> m <&> (,s)
+
+{-
+ - Reading
+ -}
+
+{- | Fetch the current value of the state
+
+> foo = do
+>   s <- get
+>   bar s
+-}
+get :: (Monad m) => StateT s m s
+get = StateT $ \s -> pure (s, s)
+
+{-
+ - Modifying
+ -}
+
+{- | Update the current value of the state with the given operation
+
+> foo = modify $ \s -> bar s
+-}
+modify :: (Monad m) => (s -> s) -> StateT s m ()
+modify f = StateT $ pure . ((),) . f
+
+{-
+ - Writing
+ -}
+
+-- | Set the state to the given value
+put :: (Monad m) => s -> StateT s m ()
+put = StateT . const . pure . ((),)
diff --git a/Mini/Transformers/WriterT.hs b/Mini/Transformers/WriterT.hs
new file mode 100644
--- /dev/null
+++ b/Mini/Transformers/WriterT.hs
@@ -0,0 +1,72 @@
+{-# LANGUAGE TupleSections #-}
+
+-- | Extension of a monad with a write-only environment
+module Mini.Transformers.WriterT (
+  -- * Type
+  WriterT,
+
+  -- * Writing
+  tell,
+
+  -- * Runners
+  runWriterT,
+) where
+
+import Control.Applicative (
+  Alternative (
+    empty,
+    (<|>)
+  ),
+ )
+import Control.Monad (
+  ap,
+  liftM,
+ )
+import Data.Functor (
+  (<&>),
+ )
+import Mini.Transformers.Class (
+  MonadTrans (
+    lift
+  ),
+ )
+
+{-
+ - Type
+ -}
+
+{- | A monad with monoidal write-only type /w/, inner monad /m/, and return type
+/a/
+-}
+newtype WriterT w m a = WriterT
+  { runWriterT :: m (a, w)
+  -- ^ Unwrap a 'WriterT'
+  }
+
+instance (Monad m, Monoid w) => Functor (WriterT w m) where
+  fmap = liftM
+
+instance (Monad m, Monoid w) => Applicative (WriterT w m) where
+  pure = WriterT . pure . (,mempty)
+  (<*>) = ap
+
+instance (Monad m, Alternative m, Monoid w) => Alternative (WriterT w m) where
+  empty = WriterT empty
+  m <|> n = WriterT $ runWriterT m <|> runWriterT n
+
+instance (Monad m, Monoid w) => Monad (WriterT w m) where
+  m >>= k = WriterT $ do
+    (a, w) <- runWriterT m
+    (b, w') <- runWriterT (k a)
+    pure (b, w <> w')
+
+instance (Monoid w) => MonadTrans (WriterT w) where
+  lift m = WriterT $ m <&> (,mempty)
+
+{-
+ - Writing
+ -}
+
+-- | Append the given value to the output
+tell :: (Monad m) => w -> WriterT w m ()
+tell = WriterT . pure . ((),)
diff --git a/fourmolu.yaml b/fourmolu.yaml
new file mode 100644
--- /dev/null
+++ b/fourmolu.yaml
@@ -0,0 +1,17 @@
+indentation: 2
+column-limit: none
+function-arrows: leading
+comma-style: leading
+import-export-style: diff-friendly
+indent-wheres: false
+record-brace-space: false
+newlines-between-decls: 1
+haddock-style: multi-line
+haddock-style-module: null
+let-style: inline
+in-style: right-align
+single-constraint-parens: always
+unicode: never
+respectful: false
+fixities: []
+reexports: []
diff --git a/mini.cabal b/mini.cabal
new file mode 100644
--- /dev/null
+++ b/mini.cabal
@@ -0,0 +1,49 @@
+cabal-version:      2.4
+name:               mini
+version:            0.1.0.0
+license:            MIT
+license-file:       LICENSE
+copyright:          (c) 2023-2024 Victor Wallsten
+author:             Victor Wallsten
+maintainer:         victor.wallsten@protonmail.com
+homepage:           https://gitlab.com/vicwall/mini
+bug-reports:        https://gitlab.com/vicwall/mini/issues
+synopsis:           Minimal essentials
+description:        A minimal yet powerful library of essentials, only depending on
+                    @base@.
+category:           library
+tested-with:        GHC == 9.4.8
+extra-doc-files:    CHANGELOG.md
+extra-source-files: .editorconfig
+                    .hlint.yaml
+                    fourmolu.yaml
+
+source-repository head
+  type:     git
+  location: https://gitlab.com/vicwall/mini.git
+
+library
+  exposed-modules:
+    Mini.Data.Map
+    Mini.Data.Set
+    Mini.Lens
+    Mini.Transformers.Class
+    Mini.Transformers.EitherT
+    Mini.Transformers.ReaderT
+    Mini.Transformers.WriterT
+    Mini.Transformers.StateT
+    Mini.Transformers.ParserT
+  build-depends:
+    base == 4.*
+  default-language:
+    Haskell2010
+  ghc-options:
+    -Wall
+    -Wcompat
+    -Widentities
+    -Wincomplete-record-updates
+    -Wincomplete-uni-patterns
+    -Wmissing-export-lists
+    -Wmissing-home-modules
+    -Wpartial-fields
+    -Wredundant-constraints