diff --git a/_freeze/posts/type-algebra/1/index/execute-results/html.json b/_freeze/posts/type-algebra/1/index/execute-results/html.json
new file mode 100644
index 0000000..64f7fe1
--- /dev/null
+++ b/_freeze/posts/type-algebra/1/index/execute-results/html.json
@@ -0,0 +1,12 @@
+{
+  "hash": "1721d4196271f3da8cf4efc33a68dcc1",
+  "result": {
+    "engine": "jupyter",
+    "markdown": "---\ntitle: \"Type Algebra and You, Part 1: Basics\"\ndescription: |\n  Counting and arithmetic on finite types.\nformat:\n  html:\n    html-math-method: katex\ndate: \"2022-07-06\"\ndate-modified: \"2025-08-06\"\ncategories:\n  - haskell\n  - hyperoperations\n  - type theory\n---\n\n\n\nWhen learning a new programming language, its type system can be a point of contention.\nDynamic systems are fairly common in scripting languages like Python and JavaScript,\n  which makes them great for beginners.\nHowever, it appears to be a general principle that imposing type-strictness (staticness, strength, ...)\n  will generally allow errors to be caught before someone discovers them.\nTo the computer, types are illusory, but they are not to the human.\n\nBeyond their use in programming languages, mathematicians also work with types in a purely abstract way\n  (putting aside the fact that \"type\" is already an abstract concept).\nTypes bear some resemblance to sets, yet in other ways resemble numbers and can be manipulated via algebra.\nIn the following couple of posts, I would like to investigate these resemblances.\n\nThis post will primarily focus on making the numerical resemblance clear,\n  since it is more fundamental and everyone tends to agree on\n  [how to define arithmetic](https://en.wikipedia.org/wiki/Peano_axioms).\nSince it can be difficult to appreciate relatively simple expressions without retreating\n  back to a programming language, I will use Haskell to demonstrate some interesting consequences\n  of this higher-kinded world.\n\n\nStarting from Square Zero\n-------------------------\n\nIf we can treat types as numbers, then we best start with 0.\nWe interpret this as the number of possible values which populate the type.\nThere are exactly zero possible values of type **0**, i.e., there is no way to construct\n  a value with this type.\n\nIn Haskell, this type is referred to as `Void`.\nHere is a paraphrased definition from (an earlier version of)\n  [`Data.Void`](https://hackage.haskell.org/package/void-0.7/docs/src/Data-Void.html):\n\n::: {#badc6fe1 .cell execution_count=3}\n``` {.haskell .cell-code}\nnewtype Void = V Void\n```\n:::\n\n\nIn other words, `V`, the only constructor of `Void`, requires already having a `Void`.\nThis requires infinite regress, so it is logically impossible.\n\n\n### Wait a minute, \"only constructor\"?\n\nNotice that `Void`'s constructor, `V`, has type `Void -> Void`.\nThis type, unlike `Void`, is definitely populated.\nIt resembles the [empty function](https://en.wikipedia.org/wiki/Function_%28mathematics%29#empty_function)\n  from set theory, of which there is only one for the empty set.\nThis means that by constructing an empty type, we've also constructed a singleton.\n\nHaskell already has a type with only one possible value: `()`[^1],\n  with its only value written identically.\nCan we prove that this is somehow the \"same\" type as `Void -> Void`?\nOf course!\nRemember, Haskell is a functional language.\nTherefore, we should focus on writing functions between the two types.\n\n[^1]: Pronounced as \"unit\"\n\n::: {#fd2372db .cell execution_count=4}\n``` {.haskell .cell-code}\n-- Haskell actually complains that you're trying to pattern-match\n--   based on the constructor if you specify `V` on the LHS.\ntoUnit :: (Void -> Void) -> ()\ntoUnit _ = ()\n\nfromUnit :: () -> (Void -> Void)\nfromUnit () = V\n```\n:::\n\n\nThe \"to\" and \"from\" in the names suggests that if we do one followed by the other,\n  we should end up where we started.\nOr, in the language of functions, the composition of the functions is the identity.\n\n```haskell\nfromUnit . toUnit == (id :: (Void -> Void) -> (Void -> Void))\ntoUnit . fromUnit == (id :: () -> ())\n```\n\nIn other words, we can reversibly map values from one type to the other (and vice versa).\nIf such functions (also known as bijections) exist, then the types are *isomorphic*.\n\n\n### Poly-iso-morphisms\n\nWe can assemble pairs of functions resembling this structure into a *typeclass* in Haskell:\n\n::: {#d80a0123 .cell execution_count=5}\n``` {.haskell .cell-code}\nclass Isomorphism a b where\n  -- Isomorphisms must define these two polymorphic functions\n  toA :: (b -> a)\n  toB :: (a -> b)\n\n  -- And these functions, which *could* be derived automatically\n  --   from the prior two, if the compiler didn't complain about ambiguity\n  identityA :: (a -> a)\n  -- aIdentity = toA . toB\n  identityB :: (b -> b)\n  -- bIdentity = toB . toA\n```\n:::\n\n\nSpecifically, the isomorphism between `Void -> Void` and `()` looks like:\n\n::: {#f71ae8c6 .cell execution_count=6}\n``` {.haskell .cell-code}\ninstance Isomorphism (Void -> Void) () where\n  toA = fromUnit\n  toB = toUnit\n\n  identityA = fromUnit . toUnit\n  identityB = toUnit . fromUnit\n```\n:::\n\n\nIn future examples, I'll use this typeclass to demonstrate isomorphisms between types.\n\n\nHyperoperative (Multi)functors\n------------------------------\n\nAnother way to go from 0 to 1 is to just add one,\n  an operation also called the [successor function](https://en.wikipedia.org/wiki/Successor_function).\n\n[Kinds](https://wiki.haskell.org/Kind) live one step up from types,\n  and we can conjecture the kind a successor \"function\" on types would have.\n\n```haskell\n-- The successor function constructs an integer from an integer\nsucc :: Int -> Int\n-- So we need to be able to construct a \"bigger\" type from a type\nSucc :: * -> *\n```\n\n\"Function\" is the wrong word for this, since it is evocative of a mapping between values,\n  rather than a mapping between types.\nThe word with the closest meaning is [*functor*](https://wiki.haskell.org/Functor),\n  which Haskell already uses to refer to types with a manipulable \"inside\" that can be mapped over.\nFortunately, the kind of `Succ` matches what Haskell expects `Functor`s to look like[^2].\n\n[^2]: In fact, since GHC 6.12.1, the compiler is smart enough to derive definitions in many cases.\n\nThe functor in Haskell which most closely resembles the successor function is `Maybe`.\n\n```haskell\ndata Maybe a = Nothing | Just a\ntype One = Maybe Void\n```\n\n<!-- Evaluate the above cell -->\n\n\n\n$$\n\\begin{matrix}\n  \\scriptsize \\text{A Maybe $X$ is either}\n  & \\scriptsize \\text{Nothing}\n  & \\scriptsize \\text{or}\n  & \\scriptsize \\text{a value of $X$}\n  \\\\\n  S(X) := & 1 & + & X\n  \\\\\n  \\scriptsize \\text{The 1-valued type is}\n  & \\scriptsize \\text{Nothing}\n  & \\scriptsize \\text{or}\n  & \\scriptsize \\text{logically impossible}\n  \\\\\n  \\bold{1}  =& 1 & + & 0\n\\end{matrix}\n$$\n\nSince `Void` is has zero possible values, we should expect `Maybe Void` to have exactly one possible value.\nConstructing a `Just Void` would require that we already had a Void value, which is impossible.\nTherefore, `Nothing` is the only possible value of `Maybe Void`.\n\n::: {#c9ca06b4 .cell execution_count=8}\n``` {.haskell .cell-code}\ntoUnitM :: Maybe Void -> ()\ntoUnitM Nothing = ()\n\nfromUnitM :: () -> Maybe Void\nfromUnitM () = Nothing\n\ninstance Isomorphism (Maybe Void) () where\n  toA = fromUnitM\n  toB = toUnitM\n\n  identityA = fromUnitM . toUnitM\n  identityB = toUnitM . fromUnitM\n```\n:::\n\n\n### Sums and Products\n\nIf there's a functor which resembles the successor, then are there ones which also resemble addition and multiplication?\nNot exactly.\nFunctors are strictly a single-argument kind, and luckily the successor is a unary function.\nAddition and multiplication are binary, so they require a slightly more complicated kind:\n\n```haskell\n(+)      :: Int -> Int -> Int   -- we can add two things together\nPlus a b :: * -> * -> *         -- so we want to be able to add two types together\n\n(*)      :: Int -> Int -> Int   -- likewise, we can multiply two things\nMult a b :: * -> * -> *         -- and we want to be able to multiply two types\n```\n\nThese kinds match what Haskell expects `Bifunctor`s to look like.\nTypes get complicated when more than one parameter is involved, so GHC cannot derive `Bifunctor`.\nAlternatively, we can just consider bifunctors as they appear here: a functor with an arity of 2.\n\nPutting aside semantics, Haskell indeed has two types resembling type addition and type multiplication.\nRespectively, they are `Either` and `(,)` (i.e., a 2-tuple):\n\n```haskell\ndata Either a b = Left a | Right b\ndata (,) a b = (,) a b\n```\n\n$$\n\\begin{matrix}\n  \\scriptsize \\text{Either $X$ or $Y$ is}\n  & \\scriptsize \\text{a value of $X$}\n  & \\scriptsize \\text{or}\n  & \\scriptsize \\text{a value of $Y$}\n  \\\\\n  E(X,Y) := & X & + & Y\n  \\\\\n  \\scriptsize \\text{A tuple of $X$ and $Y$ is}\n  & \\scriptsize \\text{a value of $X$}\n  & \\scriptsize \\text{and}\n  & \\scriptsize \\text{a value of $Y$}\n  \\\\\n  P(X,Y) := & X & \\times & Y\n\\end{matrix}\n$$\n\nProduct types are common (consider any `struct` or tuple in a more common language,\n  but sum types are less so.\n`union`s in C get close, but they are bound too memory for our purposes.\nUsing addition, we can actually reconstruct the successor from **1**:\n\n::: {#478dfc1e .cell execution_count=9}\n``` {.haskell .cell-code code-fold=\"true\" code-summary=\"Isomorphism instance for `Maybe a` and `((), a)`\"}\ntype MaybeE a = Either () a\n\ntoMaybeE :: Maybe a -> MaybeE a\ntoMaybeE Nothing  = Left ()\ntoMaybeE (Just x) = Right x\n\nfromMaybeE :: MaybeE a -> Maybe a\nfromMaybeE (Left ()) = Nothing\nfromMaybeE (Right x) = Just x\n\ninstance Isomorphism (Maybe a) (MaybeE a) where\n  toA = fromMaybeE\n  toB = toMaybeE\n\n  identityA = fromMaybeE . toMaybeE\n  identityB = toMaybeE . fromMaybeE\n```\n:::\n\n\n`Left ()` now takes on the role of `Nothing`, while all the `Right`s come from the type parameter `a`.\n\n\n### Rearranging and Rebracketing\n\nWithin the world of numbers, addition and multiplication are commutative and associative.\nIs the same true for types?\n\nCommutativity is obvious, since we can construct functions which switch *X* and *Y* around.\nHaskell already provides these functions, whose definitions I have copied here\n\n::: {#3d962ec6 .cell execution_count=10}\n``` {.haskell .cell-code code-fold=\"true\" code-summary=\"Isomorphism instance for `Either a b` and `Either b a`\"}\n-- From https://hackage.haskell.org/package/either-5.0.2/docs/Data-Either-Combinators.html#v:swapEither\nswapEither :: Either a b -> Either b a\nswapEither (Left x)  = Right x\nswapEither (Right x) = Left x\n\ninstance Isomorphism (Either x y) (Either y x) where\n  toA = swapEither\n  toB = swapEither\n\n  identityA = swapEither . swapEither\n  identityB = swapEither . swapEither\n```\n:::\n\n\n::: {#25e35e89 .cell execution_count=11}\n``` {.haskell .cell-code code-fold=\"true\" code-summary=\"Isomorphism instance for `(a,b)` and `(b,a)`\"}\n-- From https://hackage.haskell.org/package/base-4.16.1.0/docs/Data-Tuple.html#v:swap\nswap :: (a, b) -> (b, a)\nswap (x, y) = (y, x)\n\ninstance Isomorphism (x, y) (y, x) where\n  toA = swap\n  toB = swap\n\n  identityA = swap . swap\n  identityB = swap . swap\n```\n:::\n\n\nAssociativity is a bit trickier, since it deals with triples rather than pairs.\n\n::: {#660420ee .cell execution_count=12}\n``` {.haskell .cell-code code-fold=\"true\" code-summary=\"Isomorphism instance for `Either a (Either b c)` and `Either (Either a b) c`\"}\nassocRightSum :: Either a (Either b c) -> Either (Either a b) c\nassocRightSum (Left x)          = Left (Left x)\nassocRightSum (Right (Left y))  = Left (Right y)\nassocRightSum (Right (Right z)) = Right z\n\nassocLeftSum :: Either (Either a b) c -> Either a (Either b c)\nassocLeftSum (Left (Left x))  = Left x\nassocLeftSum (Left (Right y)) = Right (Left y)\nassocLeftSum (Right z)        = Right (Right z)\n\ninstance Isomorphism (Either a (Either b c)) (Either (Either a b) c) where\n  toA = assocLeftSum\n  toB = assocRightSum\n\n  identityA = assocLeftSum . assocRightSum\n  identityB = assocRightSum . assocLeftSum\n```\n:::\n\n\n::: {#cd6b5d07 .cell execution_count=13}\n``` {.haskell .cell-code code-fold=\"true\" code-summary=\"Isomorphism instance for `(a,(b,c))` and `((a,b),c)`\"}\nassocRightProd :: (a, (b, c)) -> ((a, b), c)\nassocRightProd (x, (y, z)) = ((x, y), z)\n\nassocLeftProd :: ((a, b), c) -> (a, (b, c))\nassocLeftProd ((x, y), z) = (x, (y, z))\n\ninstance Isomorphism (a, (b, c)) ((a, b), c) where\n  toA = assocLeftProd\n  toB = assocRightProd\n\n  identityA = assocLeftProd . assocRightProd\n  identityB = assocRightProd . assocLeftProd\n```\n:::\n\n\nIn fact, since we don't care about order or grouping, we can forget both entirely\n  and map them instead into 3-tuples and a triple-sum type:\n\n```haskell\ndata Either3 a b c = Left3 a | Center3 b | Right3 c\ndata (,,) a b c = (,,) a b c\n```\n\n\n\n::: {#39eeb1e0 .cell execution_count=15}\n``` {.haskell .cell-code code-fold=\"true\" code-summary=\"Isomorphism instance for `Either3 a b c` and `Either (Either a b) c`\"}\ntoLeftSum :: Either3 a b c -> Either (Either a b) c -- x+y+z = (x+y)+z\ntoLeftSum (Left3 x)   = Left (Left x)\ntoLeftSum (Center3 y) = Left (Right y)\ntoLeftSum (Right3 z)  = Right z\n\nfromLeftSum :: Either (Either a b) c -> Either3 a b c\nfromLeftSum (Left (Left x))  = Left3 x\nfromLeftSum (Left (Right y)) = Center3 y\nfromLeftSum (Right z)        = Right3 z\n\ninstance Isomorphism (Either3 a b c) (Either (Either a b) c) where\n  toA = fromLeftSum\n  toB = toLeftSum\n\n  identityA = fromLeftSum . toLeftSum\n  identityB = toLeftSum . fromLeftSum\n```\n:::\n\n\n::: {#9d579a86 .cell execution_count=16}\n``` {.haskell .cell-code code-fold=\"true\" code-summary=\"Isomorphism instance for `(a,b,c)` and `((a,b),c)`\"}\ntoLeftProd :: (a,b,c) -> ((a,b),c)\ntoLeftProd (x,y,z) = ((x,y),z)\n\nfromLeftProd :: ((a,b),c) -> (a,b,c)\nfromLeftProd ((x,y),z) = (x,y,z)\n\ninstance Isomorphism (a, b, c) ((a,b), c) where\n  toA = fromLeftProd\n  toB = toLeftProd\n\n  identityA = fromLeftProd . toLeftProd\n  identityB = toLeftProd . fromLeftProd\n```\n:::\n\n\nThere's still a bit of work to prove associativity *in general* from these local rules.\nBut that's fine, since we're still primarily concerned with the equivalent functors\n  `Either` and `(,)` (which are local anyway).\n\n\n### Other Arithmetic Properties\n\nNaturally, **0** and **1** satisfy their typical properties. There are additional interpretations, however:\n\n\n#### Additive identity\n\n::: {layout=\"[[1,5,6]]\" layout-valign=\"center\"}\n$$\n0 + X \\cong X\n$$\n\n`Isomorphism (Either Void a) a`\n\nSince **0** is unoccupied, its sum with any other type can only ever contain values from that other type\n  (i.e., only `Right` values).\n:::\n\n\n#### Multiplicative Identity\n\n::: {layout=\"[[1,5,6]]\" layout-valign=\"center\"}\n$$\n1 \\cdot X \\cong X\n$$\n\n`Isomorphism ((), a) a`\n\nSince **1** has exactly one possible value, its product with any other type is this value\n  and any value from the other type (i.e., tuples of the form `((), x)`).\n:::\n\n\n#### Multiplicative Annihilator\n\n::: {layout=\"[[1,5,6]]\" layout-valign=\"center\"}\n$$\n0 \\cdot X \\cong 0\n$$\n\n`Isomorphism (Void, a) Void`\n\nSince **0** is unoccupied, we cannot construct a type which requires a value from it\n  (i.e., writing a tuple of the form `(Void, x)` requires having a `Void` value).\n:::\n\n\n### Distributivity\n\nFinally, to hammer home the resemblance to normal arithmetic, we should consider the\n  distribution of multiplication over addition.\nFirst, notice that type multiplication does distribute over the successor:\n\n::: {#d2d379c9 .cell execution_count=17}\n``` {.haskell .cell-code}\ntype SuccDist a b = (Maybe a, Maybe b)\ndata SumProd a b = Nada | LProd a | RProd b | BothProd a b\n```\n:::\n\n\n$$\n\\begin{matrix}\n  \\scriptsize \\text{Maybe $X$ and Maybe $Y$} & \\scriptsize \\text{is equivalent to}\n  \\\\\n  (1 + X) \\cdot (1 + Y) \\cong\n  \\\\\n  1 & \\scriptsize \\text{Both Nothing}\n  \\\\\n    + X \\phantom{\\cdot Y}\n  & \\scriptsize \\text{or Just $x$, Nothing}\n  \\\\\n    + \\phantom{X \\cdot} Y & \\scriptsize \\text{or Nothing, Just $y$}\n  \\\\\n    + X \\cdot Y & \\scriptsize \\text{or Just $x$, Just $y$}\n\\end{matrix}\n$$\n\nIf we forbade the first and last cases (in other words, if we \"subtract\" them out),\n  then the type would be equivalent to the sum of *X* and *Y*.\n\n::: {#cd999825 .cell execution_count=18}\n``` {.haskell .cell-code code-fold=\"true\" code-summary=\"Isomorphism instance for `SuccDist a b` and `SumProd a b`\"}\neitherToSuccDist :: Either a b -> SuccDist a b\neitherToSuccDist (Left x) = (Just x, Nothing)\neitherToSuccDist (Right y) = (Nothing, Just y)\n\nsuccDistToEither :: SuccDist a b -> Either a b\nsuccDistToEither (Just x, Nothing) = Left x\nsuccDistToEither (Nothing, Just y) = Right y\nsuccDistToEither _                 = undefined -- non-exhaustive!\n\n-- succDistToEither . eitherToSuccDist == (id :: Either a b -> Either a b)\n-- eitherToSuccDist . succDistToEither /= id (because of extra values)\n\ntoSumProd :: SuccDist a b -> SumProd a b\ntoSumProd (Nothing, Nothing) = Nada\ntoSumProd (Just x, Nothing)  = LProd x\ntoSumProd (Nothing, Just y)  = RProd y\ntoSumProd (Just x, Just y)   = BothProd x y\n\ntoSuccDist :: SumProd a b -> SuccDist a b\ntoSuccDist Nada           = (Nothing, Nothing)\ntoSuccDist (LProd x)      = (Just x, Nothing)\ntoSuccDist (RProd y)      = (Nothing, Just y)\ntoSuccDist (BothProd x y) = (Just x, Just y)\n\ninstance Isomorphism (SuccDist a b) (SumProd a b) where\n  toA = toSuccDist\n  toB = toSumProd\n\n  identityA = toSuccDist . toSumProd\n  identityB = toSumProd . toSuccDist\n```\n:::\n\n\nFortunately, general distributivity is also relatively simple.\nWe do as grade schoolers do and FOIL out the results.\n\n::: {#8ea8c475 .cell execution_count=19}\n``` {.haskell .cell-code}\ntype PreDist a b c d  = (Either a b, Either c d)\n-- first, outer, inner, last\ndata PostDist a b c d = F a c | O a d | I b c | L b d\n```\n:::\n\n\n$$\n\\begin{matrix}\n  \\scriptsize \\text{Either $X$ $Y$ and Either $Z$ $W$} & \\scriptsize \\text{is equivalent to}\n  \\\\\n  (X + Y) \\cdot (Z + W) \\cong\n  \\\\\n  \\phantom{+} X \\cdot Z\n  & \\scriptsize \\text{Firsts,}\n  \\\\\n  \\vphantom{} + X \\cdot W\n  & \\scriptsize \\text{Outers,}\n  \\\\\n  \\vphantom{} + Y \\cdot Z\n  & \\scriptsize \\text{Inners,}\n  \\\\\n  \\vphantom{} + Y \\cdot W\n  & \\scriptsize \\text{or Lasts}\n\\end{matrix}\n$$\n\n...then construct our bijections:\n\n::: {#b40947f2 .cell execution_count=20}\n``` {.haskell .cell-code code-fold=\"true\" code-summary=\"Isomorphism instance for `PreDist a b` and `PostDist a b`\"}\ndistribute :: PreDist a b c d -> PostDist a b c d\ndistribute (Left x, Left z)   = F x z\ndistribute (Left x, Right w)  = O x w\ndistribute (Right y, Left z)  = I y z\ndistribute (Right y, Right w) = L y w\n\nundistribute :: PostDist a b c d -> PreDist a b c d\nundistribute (F x z) = (Left x, Left z)\nundistribute (O x w) = (Left x, Right w)\nundistribute (I y z) = (Right y, Left z)\nundistribute (L y w) = (Right y, Right w)\n\ninstance Isomorphism (PreDist a b c d) (PostDist a b c d) where\n  toA = undistribute\n  toB = distribute\n\n  identityA = undistribute . distribute\n  identityB = distribute . undistribute\n```\n:::\n\n\nThis works primarily because without further information about any of the types `a`, `b`, `c`, `d`,\n  we can only rearrange values of them.\n\n\nBools, Bools, and more Bools\n----------------------------\n\nWhile it's all well and good that these operations appear to mirror familiar arithmetic,\n  we haven't counted farther than **0** and **1**.\nEveryone past the age of two recognizes that **2** comes next.\n\nFortunately, this corresponds to a much better-known type: booleans.\nRather than defining them as numbers like in lower-level languages (as a computer would understand),\n  we can construct them directly as abstract values in Haskell\n\n```haskell\ndata Bool = True | False\n```\n\n$$\n\\begin{matrix}\n  \\scriptsize \\text{A bool is either}\n  & \\scriptsize \\text{True}\n  & \\scriptsize \\text{or}\n  & \\scriptsize \\text{False}\n  \\\\\n  \\text{Bool} := & 1 & + & 1 &= \\bold{2}\n\\end{matrix}\n$$\n\nBools may also be defined using the above functors, either by two successors or by addition:\n\n::: {#dd127a83 .cell execution_count=21}\n``` {.haskell .cell-code}\ntype BoolSucc = Maybe (Maybe Void) -- succ (succ 0)\ntype BoolEither = Either () () -- 1 + 1\n```\n:::\n\n\n::: {#c17491e6 .cell execution_count=22}\n``` {.haskell .cell-code code-fold=\"true\" code-summary=\"Isomorphism instance for `Bool` and `BoolSucc`\"}\ntoBoolSucc :: Bool -> BoolSucc\ntoBoolSucc False = Nothing\ntoBoolSucc True  = Just Nothing\n\nfromBoolSucc :: BoolSucc -> Bool\nfromBoolSucc Nothing        = False\nfromBoolSucc (Just Nothing) = True\n\ninstance Isomorphism Bool BoolSucc where\n  toA = fromBoolSucc\n  toB = toBoolSucc\n\n  identityA = fromBoolSucc . toBoolSucc\n  identityB = toBoolSucc . fromBoolSucc\n```\n:::\n\n\n::: {#77b940c7 .cell execution_count=23}\n``` {.haskell .cell-code code-fold=\"true\" code-summary=\"Isomorphism instance for `Bool` and `BoolEither`\"}\ntoBoolEither :: Bool -> BoolEither\ntoBoolEither False = Left ()\ntoBoolEither True  = Right ()\n\nfromBoolEither :: BoolEither -> Bool\nfromBoolEither (Left ())  = False\nfromBoolEither (Right ()) = True\n\ninstance Isomorphism Bool BoolEither where\n  toA = fromBoolEither\n  toB = toBoolEither\n\n  identityA = fromBoolEither . toBoolEither\n  identityB = toBoolEither . fromBoolEither\n```\n:::\n\n\n### Four Great Justice\n\nRather than progressing to **3**, let's jump to **4**.\nThe number 2 has an interesting property: its sum with itself is its product with itself\n  (is its exponent with itself...) is 4.\nThus, the following types all encode a four-valued type:\n\n::: {#05170448 .cell execution_count=24}\n``` {.haskell .cell-code}\ndata Four     = Zero | One | Two | Three\ntype FourSucc = Maybe (Maybe Bool)\ntype FourSum  = Either Bool Bool\ntype FourProd = (Bool, Bool)\n```\n:::\n\n\n$$\n\\begin{align*}\n  4 &:= 1+1+1+1\n  \\\\\n  & \\phantom{:}\\cong  S(S(2))\n  \\\\\n  & \\phantom{:}\\cong  E(2,2) = 2 + 2\n  \\\\\n  & \\phantom{:}\\cong  P(2,2) = 2 \\cdot 2 \\\\\n\\end{align*}\n$$\n\nShowing isomorphism here can get a bit tricky, but there are natural bijections for `FourSum` and `FourProd` obtained by examining the binary expansions of 0, 1, 2, and 3.\n\n::: {#1319626e .cell execution_count=25}\n``` {.haskell .cell-code code-fold=\"true\" code-summary=\"Isomorphism instance for `Four` and `FourSucc`\"}\ntoFourSucc :: Four -> FourSucc\ntoFourSucc Zero  = Nothing\ntoFourSucc One   = Just Nothing\ntoFourSucc Two   = Just (Just False)\ntoFourSucc Three = Just (Just True)\n\nfromFourSucc :: FourSucc -> Four\nfromFourSucc Nothing             = Zero\nfromFourSucc (Just Nothing)      = One\nfromFourSucc (Just (Just False)) = Two\nfromFourSucc (Just (Just True))  = Three\n\ninstance Isomorphism Four FourSucc where\n  toA = fromFourSucc\n  toB = toFourSucc\n\n  identityA = fromFourSucc . toFourSucc\n  identityB = toFourSucc . fromFourSucc\n```\n:::\n\n\n::: {#9a84d053 .cell execution_count=26}\n``` {.haskell .cell-code code-fold=\"true\" code-summary=\"Isomorphism instance for `Four` and `FourSum`\"}\ntoFourSum :: Four -> FourSum\ntoFourSum Zero  = Left False   -- 00\ntoFourSum One   = Left True    -- 01\ntoFourSum Two   = Right False  -- 10\ntoFourSum Three = Right True   -- 11\n\nfromFourSum :: FourSum -> Four\nfromFourSum (Left False)  = Zero\nfromFourSum (Left True)   = One\nfromFourSum (Right False) = Two\nfromFourSum (Right True)  = Three\n\ninstance Isomorphism Four FourSum where\n  toA = fromFourSum\n  toB = toFourSum\n\n  identityA = fromFourSum . toFourSum\n  identityB = toFourSum . fromFourSum\n```\n:::\n\n\n::: {#e57cb529 .cell execution_count=27}\n``` {.haskell .cell-code code-fold=\"true\" code-summary=\"Isomorphism instance for `Four` and `FourProd`\"}\ntoFourProd :: Four -> FourProd\ntoFourProd Zero  = (False, False)  -- 00\ntoFourProd One   = (False, True)   -- 01\ntoFourProd Two   = (True, False)   -- 10\ntoFourProd Three = (True, True)    -- 11\n\nfromFourProd :: FourProd -> Four\nfromFourProd (False, False) = Zero\nfromFourProd (False, True)  = One\nfromFourProd (True, False)  = Two\nfromFourProd (True, True)   = Three\n\ninstance Isomorphism Four FourProd where\n  toA = fromFourProd\n  toB = toFourProd\n\n  identityA = fromFourProd . toFourProd\n  identityB = toFourProd . fromFourProd\n```\n:::\n\n\n### Hiding in the Clouds\n\nThough I mentioned exponentiation earlier, I did not show the equivalent for types.\nSet theorists sometimes write\n  [the set of functions from one set *A* to another set *B*](https://en.wikipedia.org/wiki/Function_type)\n  as $B^A$ because the number of possible functions comes from the cardinalities of the sets:\n  $|B|^{|A|}$.\nWe previously examined how the constructor for Void is a singleton, which satisfies the equation $0^0 = 1$.\nAt least in the finite world, sets and types are not so different, and indeed, we can write:\n\n::: {#ae11e257 .cell execution_count=28}\n``` {.haskell .cell-code}\ntype FourFunc = Bool -> Bool\n\n-- There are exactly four functions:\ntaut x = True   -- tautology\ncont x = False  -- contradiction\nid'  x = x      -- identity\nnot'   = not    -- negation\n```\n:::\n\n\n$$\n\\textcolor{red}{2} \\rightarrow \\textcolor{blue}{2}\n  = \\textcolor{blue}{2}^{\\textcolor{red}{2}} \\cong \\bold 4\n$$\n\nIf we want to map these functions onto our `Four` type, we can again examine\n  the binary expansion of the numbers 0-3.\nThis time, the rightmost place value encodes the value of the function on `False`,\n  and the leftmost value the same on `True`.\n\n::: {#aac4a396 .cell execution_count=29}\n``` {.haskell .cell-code code-fold=\"true\" code-summary=\"Isomorphism instance for `Four` and `FourFunc`\"}\ntoFourFunc :: Four -> FourFunc\n--                       -- f(1) f(0)\ntoFourFunc Zero  = cont  --   0    0\ntoFourFunc One   = not'  --   0    1\ntoFourFunc Two   = id'   --   1    0\ntoFourFunc Three = taut  --   1    1\n\nfromFourFunc :: FourFunc -> Four\nfromFourFunc cont = Zero\nfromFourFunc not' = One\nfromFourFunc id'  = Two\nfromFourFunc taut = Three\n\ninstance Isomorphism Four FourFunc where\n  toA = fromFourFunc\n  toB = toFourFunc\n\n  identityA = fromFourFunc . toFourFunc\n  identityB = toFourFunc . fromFourFunc\n```\n:::\n\n\nFor larger functions, we can see a more generalizable mapping from looking at a truth table, shown here for AND:\n\n| Column Number | Binary | Input (x) | Input (y) | x AND y |\n|---------------|--------|-----------|-----------|---------|\n| 0             | 00     | False     | False     | False   |\n| 1             | 01     | False     | True      | False   |\n| 2             | 10     | True      | False     | False   |\n| 3             | 11     | True      | True      | True    |\n\nGoing up the final column and converting to binary digits, we can read \"1000\",\n  which is the binary expansion of 8.\nThe other numbers from 0 to $(2^2)^2 - 1$ can similarly be associated to\n  boolean functions `Bool -> (Bool -> Bool)`[^3].\n\n[^3]: Note that function arrows are assumed to be right-associative, but this is opposite\n      the typical application order of exponentiation.\n    I'll dive deeper into why this needs to be the case later.\n\n\nClosing\n-------\n\nIf you know your Haskell, especially the difference between `data` and `newtype`,\n  then you know about the way I have slightly stretched the truth.\nIt is true that types defined with `data` implicitly add a possible\n  `undefined` value which can tell the runtime to error out.\nEveryone who knows Haskell better than me says\n  [not to worry about it in most cases](https://wiki.haskell.org/Newtype).\nAt worst, using `data` would make some of the pretty arithmetic above be less pretty.\n\nOther fascinating concepts live in this world, such as the\n  [Curry-Howard correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence).\nRather than discussing them, in [the next post](../2/) I would like to press onward with the algebra.\nI have spent this post laying the groundwork for arithmetic on types,\n  so it will focus more upon recursion and fixed points.\n\n\n### Additional Links\n\n- [Algebraic Data Types](https://en.wikipedia.org/wiki/Algebraic_data_type)\n  (Wikipedia)\n- [Generically Deriving Bifunctor](https://blog.csongor.co.uk/generic-deriving-bifunctor/)\n  (Blogpost by Csongor Kiss)\n\n",
+    "supporting": [
+      "index_files"
+    ],
+    "filters": [],
+    "includes": {}
+  }
+}
\ No newline at end of file
diff --git a/_freeze/posts/type-algebra/2/index/execute-results/html.json b/_freeze/posts/type-algebra/2/index/execute-results/html.json
new file mode 100644
index 0000000..e1ef032
--- /dev/null
+++ b/_freeze/posts/type-algebra/2/index/execute-results/html.json
@@ -0,0 +1,12 @@
+{
+  "hash": "8237c79583c607ab70a8880afd77b989",
+  "result": {
+    "engine": "jupyter",
+    "markdown": "---\ntitle: \"Type Algebra and You, Part 2: A Fixer-upper\"\ndescription: |\n  Broadening arithmetic to exponentials and adding in fixed points.\nformat:\n  html:\n    html-math-method: katex\ndate: \"2022-07-24\"\ndate-modified: \"2025-08-06\"\ncategories:\n  - haskell\n  - type theory\n---\n\n\n\nIn the [previous post](../1/), I wrote mostly about finite types,\n  as well as type addition (`Either`) and multiplication (`(,)`) between them.\n\nI mentioned at the end of the previous post that exponents correspond to functions.\nThis post will focus on this operation before moving on to recursively-defined types.\n\n\nExponent Laws\n-------------\n\nIt's not a stretch to say that without them, nothing would get done in a program.\nThey are denoted as:\n\n::: {#60e44c72 .cell execution_count=3}\n``` {.haskell .cell-code}\n-- Equivalent to `a -> b`\ntype Exponent a b = (->) a b\n```\n:::\n\n\n$$\n\\text{Exp}(X,Y) := Y^X = X \\rightarrow Y\n$$\n\nThe arrow constructor (typically infixed) appears everywhere in Haskell types.\nBut is the corresponding notation $Y^X$ fitting or merely illusory?\n\n\n### Exponentiation Distributes over Multiplication\n\nOne law of exponents states that if we have a product raise it to an exponent,\n  then the exponent should distribute to both terms.\nIn types, this is:\n\n$$\n\\stackrel{\n  \\text{A function to a product}\n}{Z \\rightarrow (X \\times Y)} = (X\\times Y)^{Z}\n%\n\\stackrel{?}{\\cong}  X^Z \\times Y^Z = \\stackrel{\n  \\text{A pair of functions with a common input}\n}{(Z \\rightarrow X) \\times (Z \\rightarrow Y)}\n$$\n\nThis says that a function `f` returning a pair can be decomposed as a pair of functions\n  `g` and `h` returning each component.\nIf we wish to convert form the former to the latter, we can call `f`,\n  then use the functions that give either element of the tuple (`fst` and `snd`).\nConversely, if we instead have a pair of functions from the same type,\n  then we can just send the same value to both and put it in a pair.\n\n::: {#6268cd1b .cell execution_count=4}\n``` {.haskell .cell-code}\nundistExp :: (a -> b, a -> c) -> (a -> (b, c))\nundistExp (g, h) x = (g x, h x)\n-- undistExp (g, h) = \\x -> (g x, h x)\n\ndistExp :: (a -> (b, c)) -> (a -> b, a -> c)\ndistExp f = (fst . f, snd . f)\n-- distExp f = (\\x -> fst (f x), \\x -> snd (f x))\n\ninstance Isomorphism (Exponent a b, Exponent a c) (Exponent a (b, c)) where\n  toA = distExp\n  toB = undistExp\n\n  identityA = distExp . undistExp\n  identityB = undistExp . distExp\n```\n:::\n\n\nUnlike with the sum and product, the identities here exist on functions themselves.\nFortunately, Haskell is\n  [referentially transparent](https://en.wikipedia.org/wiki/Referential_transparency),\n  so we could deepen the proof by composing the functions and using lambda calculus rules\n  until the expression is clearly an identity.\nIf we wanted to, it would be possible to do the same for the identities on the previous post.\nIn the interest of being concise, I won't be doing so.\n\n\n### Product of Exponents is an Exponent of a Sum\n\nWe also know that if two expressions with same base are multiplied, their exponents should add.\nSo at the type level, we must check the equivalence of the following:\n\n$$\n\\stackrel{\n  \\text{A pair of functions with a common return}\n}{(X \\rightarrow Z) \\times (Y \\rightarrow Z)}\n= Z^{X} \\times Z^Y\n%\n\\stackrel{?}{\\cong}  Z^{X + Y}\n= \\stackrel{\n  \\text{A function on a sum}\n}{(X + Y) \\rightarrow Z}\n$$\n\nThis says that a pair of functions `g` and `h` with the same return type can be composed\n  into a function `f`.\nIf we start with the former, we must create a function `f` on `Either` which decides\n  which function to use.\nIf we have this function already, we can get back to where we started by putting our values\n  into `Either` with `Left` or `Right` before using `f`.\nThe bijections look like:\n\n::: {#5891082e .cell execution_count=5}\n``` {.haskell .cell-code}\ntoExpSum :: (a -> c, b -> c) -> (Either a b -> c)\ntoExpSum (g, h) w = case w of\n  Left x  -> g x\n  Right y -> h y\n-- toExpSum (g, h) = \\w -> case w of ...\n\nfromExpSum :: (Either a b -> c) -> (a -> c, b -> c)\nfromExpSum f = (f . Left, f . Right)\n-- fromExpSum f = (\\x -> f (Left x), \\y -> f (Right y))\n\ninstance Isomorphism (Exponent a c, Exponent b c) (Exponent (Either a b) c) where\n   toA = fromExpSum\n   toB = toExpSum\n\n   identityA = fromExpSum . toExpSum\n   identityB = toExpSum . fromExpSum\n```\n:::\n\n\nThis identity actually tells us something very important regarding the definition\n  of functions on sum types: they must have as many definitions (i.e., a *product* of definitions)\n  as there are types in the sum.\nThis has been an implicit part of all bijections involving `Either`, since they have a path for\n  both `Left` and `Right`.\n\n\n### Exponent of an Exponent is an Exponent of a Product\n\nFinally (arguably as consequence of the first law), if we raise a term with an exponent\n  to another exponent, the exponents should multiply.\n\n$$\n\\stackrel{\n  \\text{A function returning a function}\n}{X \\rightarrow (Y \\rightarrow Z)} = (Z^{Y})^X\n%\n\\stackrel{?}{\\cong}\nZ^{X \\times Y}  = \\stackrel{\n  \\text{A function on a product}\n}{(X \\times Y) \\rightarrow Z}\n$$\n\nWe start with a function which returns a function and end up with a function from a product.\nThe equivalence of these two types is [currying](https://en.wikipedia.org/wiki/Currying),\n  an important concept in computer science.\nHaskell treats it so importantly that the bijections are almost trivial\n\n::: {#915facd6 .cell execution_count=6}\n``` {.haskell .cell-code}\ncurry' :: (a -> (b -> c)) -> ((a, b) -> c)\ncurry' f (x, y) = f x y\n-- curry' f = \\(x, y) -> (f x) y\n\nuncurry' :: ((a, b) -> c) -> (a -> b -> c)\nuncurry' f x y = f (x, y)\n-- uncurry' f = \\x -> \\y -> f (x, y)\n\ninstance Isomorphism (Exponent a (Exponent b c)) (Exponent (a,b) c) where\n  toA = uncurry'\n  toB = curry'\n\n  identityA = uncurry' . curry'\n  identityB = curry' . uncurry'\n```\n:::\n\n\nThese come pre-implemented in Haskell since tuples are harder to define than a chain of arrows.\n\n\nDouble-Checking for Algebra\n---------------------------\n\nEven though we've established that sums, products, and exponents obey\n  their normal arithmetical rules, we've yet to lay the groundwork for algebra.\nIn algebra, we start by introducing a symbol called *x* and allow it to interacting with numbers.\nThis means that it obeys the arithmetical laws that have been established.\n\nFunctors allow us to parametrize a type in a similar way to this.\nWe already know how to add and multiply finite types, for a \"variable\" type *X*,\n  it bears checking that it can add and multiply with itself.\n\n\n### Coefficients\n\nIs it truly the case that an object's sum with itself is its product with a 2-valued type?\nIt should follow from addition laws, but it might behoove us to check\n\n::: {#2f4a735c .cell execution_count=7}\n``` {.haskell .cell-code}\ntype LeftRight a = Either a a\n-- Alternatively:\n-- type LeftRight a ≅ (Bool, a)\n```\n:::\n\n\n$$\nX + X \\stackrel{?}\\cong 2 \\times X\n$$\n\nIt's actually quite simple if we look back at the implementation of `Bool` as `Either () ()`.\n`False` values go on the `Left`, and `True` values go on the `Right`:\n\n::: {#5036e8bb .cell execution_count=8}\n``` {.haskell .cell-code}\nto2Coeff :: LeftRight a -> (Bool, a)\nto2Coeff (Left x)  = (False, x)\nto2Coeff (Right x) = (True, x)\n\nfrom2Coeff :: (Bool, a) -> LeftRight a\nfrom2Coeff (False, x) = Left x\nfrom2Coeff (True, x)  = Right x\n\ninstance Isomorphism (LeftRight a) (Bool, a) where\n  toA = from2Coeff\n  toB = to2Coeff\n\n  identityA = from2Coeff . to2Coeff\n  identityB = to2Coeff . from2Coeff\n```\n:::\n\n\nWe can continue adding *X* to itself using `Either` to obtain arbitrarily high coefficients.\nThis is simplest as  `Either a (Either a (... (Either a a)))`, where values are a chain of\n  `Right`s ending in a `Left`.\nThen, the maximum number of `Right`s allowed is *n* - 1.\nCounting zero, there are *n* values, demonstrating the type *n*.\n\n\n### Exponents\n\nMultiplying *X* by a finite type is all well and good, but we should also check\n  that it can multiply like itself.\nIf all is well, then this should be equivalent to raising *X* to an exponent.\nWe've already discussed those laws, but just in case, we should check\n\n::: {#8c1173d4 .cell execution_count=9}\n``` {.haskell .cell-code}\ntype Pair a = (a, a)\n-- Pair a ≅ (Bool -> a)\n```\n:::\n\n\n$$\nX \\times X  \\stackrel{?}{\\cong}\nX^2 = 2 \\rightarrow X\n$$\n\nTo wit, we express the pair as a function from the finite type `Bool`.\nIf we have our pair of *X*, then we know our output is one of the two,\n  and return a function that decides to return.\nOn the other hand, we need only apply a function from `Bool` to every possible value in `Bool`\n  as many times as it appears (twice) and collect it in a product to get back to where we started.\nThe bijections to and from this type look like this\n\n::: {#bd6a45a7 .cell execution_count=10}\n``` {.haskell .cell-code}\nto2Exp :: (a, a) -> (Bool -> a)\nto2Exp (x, y) False = x\nto2Exp (x, y) True = y\n-- to2Exp (x, y) = \\p -> case p of ...\n\nfrom2Exp :: (Bool -> a) -> (a, a)\nfrom2Exp f = (f False, f True)\n\ninstance Isomorphism (a, a) (Bool -> a) where\n  toA = from2Exp\n  toB = to2Exp\n\n  identityA = from2Exp . to2Exp\n  identityB = to2Exp . from2Exp\n```\n:::\n\n\nThis a special case of what are called *representable functors*.\nThe functor in question is `Pair`, represented by functions from `Bool`.\nA similar argument can be shown for any *n* that\n  $\\overbrace{X \\times X \\times ... \\times X}^n$ can be represented functions from *n*.\n\nTogether, these two isomorphisms mean that any polynomial whose coefficients are positive integers\n  can be interpreted as a functor in *X*.\n\n\nFixing What Ain't Broke\n-----------------------\n\nExponents, finite types and polynomials are wonderful, but we need to go further.\nEven though we have access to types for any natural number, we can only define\n  finite arithmetic within them.\nWe could inflate the number of possible values in a naive way...\n\n\n```haskell\ndata Nat = Zero | One | Two | Three | Four | Five | ...\n```\n\n$$\n\\begin{matrix} &\n\\scriptsize \\text{Zero} & \\scriptsize \\text{or} &\n\\scriptsize \\text{One} & \\scriptsize \\text{or} &\n\\scriptsize \\text{Two} & \\scriptsize \\text{or}\n\\\\\nX =& 1 &+& 1 &+& 1 &+& ...\n\\end{matrix}\n$$\n\n...but this is akin to programming without knowing how to use loops.\nIn Haskell, we approach (potentially infinite) loops recursively.\nOne of the simplest ways we can recurse is by using a\n  [fixed-point combinator](https://en.wikipedia.org/wiki/Fixed-point_combinator).\nWhile typically discussed at the value level as a higher-order function,\n  there also exists a similar object at the type level which operates on functors.\nHaskell implements this type in\n  [`Data.Fix`](https://hackage.haskell.org/package/data-fix-0.3.2/docs/Data-Fix.html),\n  from which I have copied the definition below\n\n::: {#2cd7fdda .cell execution_count=11}\n``` {.haskell .cell-code}\n-- Fix :: (* -> *) -> *\nnewtype Fix f = In { out :: f (Fix f) }\n\n-- Compare with the functional fixed-point\nfix :: (a -> a) -> a\nfix f = let x = f x in x\n```\n:::\n\n\n$$\n\\mathcal{Y}(F(X)) := F(\\mathcal Y (F))\n$$\n\n(\"Y\" here comes from the Y-combinator, which isn't entirely accurate, but is fitting enough)\n\nIf we `Fix` a functor `f` Values of this type are the functor `f` containing a `Fix f`.\nIn other words, it produces a new type containing itself.\n\n\nAu Naturale\n-----------\n\nTo demonstrate how this extends what the kinds of types we can define, let's work out the natural numbers.\n[Peano arithmetic](https://en.wikipedia.org/wiki/Peano_axioms) gives them a recursive definition:\n  they are either 0 or the successor of another natural number.\nThe \"naive\" definition in Haskell is very simple. Arithmetically, though, things seem to go wrong.\n\n::: {#2e2e813a .cell execution_count=12}\n``` {.haskell .cell-code}\ndata Nat' = Zero | Succ Nat'\n\nzero' = Zero\none'  = Succ Zero\ntwo'  = Succ one'\n-- ...\n```\n:::\n\n\nValues in `Nat'` are a string of `Succ`s which terminate in a `Zero`.\nOf course, we also could define this in terms of `Fix`.\nFirst, we need to define a type to fix, then apply the operator\n\n::: {#a21806d6 .cell execution_count=13}\n``` {.haskell .cell-code}\ndata NatU a = ZeroU | SuccU a\n\n-- Possible values are \"In ZeroU\" or \"In (SuccU (x :: Fix NatU))\"\ntype NatF = Fix NatU\n```\n:::\n\n\nIf we look at things a little closer, we realize that `NatU` has the exact same form\n  as the successor functor, `Maybe`.\n\n::: {#af103cad .cell execution_count=14}\n``` {.haskell .cell-code}\ntype Nat = Fix Maybe\n\nzero = In Nothing\none  = In (Just zero)\ntwo  = In (Just one)\n-- ...\n```\n:::\n\n\n$$\n\\text{Nat} \\text{ or } \\omega := \\mathcal Y(S)\n$$\n\nLooking back, the statement $X = 1 + X$ is identical to the statement\n  \"*X* is the fixed point of the successor\", as its definition implies.\nUsing the latter form, we can define a bijection to and from `Int`\n  (which I'm regarding as only containing positive integers) as\n\n::: {#f0d1ca22 .cell execution_count=15}\n``` {.haskell .cell-code}\ntoNat :: Int -> Nat\ntoNat 0 = In Nothing\ntoNat x = In $ Just $ toNat $ x - 1 -- the successor Nat of the predecessor of x\n\nfromNat :: Nat -> Int\nfromNat (In Nothing)  = 0\nfromNat (In (Just x)) = 1 + fromNat x -- ...of the predecessor of In (Just x)\n\ninstance Isomorphism Int Nat where\n  toA = fromNat\n  toB = toNat\n\n  identityA = fromNat . toNat   -- Valid for positive integers only!\n  identityB = toNat . fromNat\n```\n:::\n\n\nThese bijections are different from the ones we have seen thus far.\nBoth of them are defined recursively, just like our functorial `Fix`.\nConsequently, rather than exhausting the possible cases,\n  it relies on deconstructing `Nat`s and arithmetic on `Int`s.\n\n::: {#b0c2c967 .cell execution_count=16}\n``` {.haskell .cell-code}\nsuccNat :: Nat -> Nat\nsuccNat x = In (Just x)\n-- succNat x = In . Just\n\nsuccInt :: Int -> Int\nsuccInt x = x + 1\n```\n:::\n\n\nThere's actually no way to know whether the functions above do the same thing,\n  at least without knowing more about `Int`.\nAt best, they afford us a way to bootstrap a way to display numbers that isn't iterated `Just`s.\n\n\nFunctors from Bifunctors\n------------------------\n\nIf the first argument of a bifunctor is fixed, then what remains is a functor.\nFor example, with `Either`:\n\n```haskell\nforall a. Either a :: * -> *\n```\n\nSince this type is functor-like, we can apply `Fix` to it.\n\n::: {#df31c5bb .cell execution_count=17}\n``` {.haskell .cell-code}\ntype Any a = Fix (Either a)\n-- Any' a ~ (Either a (Any' a))\n\nleftmost x = In (Left x)\noneRight x = In (Right (leftmost x))\ntwoRight x = In (Right (oneRight x))\n```\n:::\n\n\n$$\n\\text{Any}(X) := \\mathcal Y(E(X,-))\n= \\mathcal Y(X +)\n$$\n\nRemember what was said earlier about types which look like nested `Either a`?\nThis type encompasses all of those (granted, interspersed with the `Fix` constructor).\n\nI used the names \"one\" and \"two\" in the above example functions to suggest similarity to Nat above.\nIn fact, if `a ~ ()`, then because we already our functor `Either ()` is isomorphic to `Maybe`,\n  we know that `Any ()` is isomorphic to `Nat`.\nIf the type was `Any Bool`, We could terminate the chains in either `Left True` or `Left False`;\n  it is isomorphic to `(Nat, Bool)`.\nIn general, `Any a` is isomorphic to `(Nat, a)`.\n\n::: {#a13e7372 .cell execution_count=18}\n``` {.haskell .cell-code}\ntoAny :: (Nat, a) -> Any a\ntoAny (In Nothing,  x) = In (Left x)\ntoAny (In (Just n), x) = In (Right (toAny (n, x)))\n\nfromAny :: Any a -> (Nat, a)\nfromAny = fromAny' (In Nothing) where\n  fromAny' x (In (Left y))  = (x,  y)\n  fromAny' x (In (Right y)) = fromAny' (In (Just x)) y\n\ninstance Isomorphism (Nat, a) (Any a) where\n  toA = fromAny\n  toB = toAny\n\n  identityA = fromAny . toAny\n  identityB = toAny . fromAny\n```\n:::\n\n\nNote how fixing a sum-like object gives a product-like object.\n\n\n### What about Products?\n\nIf we can do it for sums, we should be able to do it for products.\nHowever, unlike sums, products don't have a builtin exit point.\nFor `Either`, all we need to do is turn `Left` and be done, but fixing a product goes on endlessly.\n\n::: {#3c697f4c .cell execution_count=19}\n``` {.haskell .cell-code}\ntype Stream a = Fix ((,) a)\n-- Stream a ~ (a, Stream a)\n\nrepeatS x = In (x, repeatS x)\n       -- = In (x, In (x, ...\n```\n:::\n\n\n$$\n\\text{Stream}(X) := \\mathcal Y(P(X,-)) =\n\\mathcal Y(X \\times)\n$$\n\nUnlike `Void`, whose \"definition\" would require an infinite chain of constructors,\n  we can actually create values of this type, as seen above with the definition of `repeatS.\n` Fortunately, Haskell is lazy and doesn't actually try to evaluate the entire result.\n\nIf fixing a sum produced a product object with a natural number, then it stands to reason that\n  fixing a product will produce an exponential object with a natural number.\nBy this token, we should try to verify that\n  $\\text{Stream}(X) \\cong X^{\\omega} = \\text{Nat} \\rightarrow X$.\nIntuitively, we have an value of type *X* at every position of a stream defined\n  by a natural number (the input type).\nThis specifies every possible position.\n\n::: {#4e1a2fab .cell execution_count=20}\n``` {.haskell .cell-code}\ntoStream :: (Nat -> a) -> Stream a\ntoStream f = toStream' (In Nothing) where\n  toStream' n = In (f n, toStream' (In (Just n)))\n\nfromStream :: Stream a -> (Nat -> a)\nfromStream (In (x,y)) (In Nothing)  = x\nfromStream (In (x,y)) (In (Just m)) = fromStream y m\n-- fromStream (In (x,y)) = \\n -> case n of ...\n\ninstance Isomorphism (Nat -> a) (Stream a) where\n  toA = fromStream\n  toB = toStream\n\n  identityA = fromStream . toStream\n  identityB = toStream . fromStream\n```\n:::\n\n\nNotice that in `toStream`, an equal number of \"layers\" are added\n  to `Nat` and `Stream` with the `In` constructor,\n  and in `fromStream`, an equal number of layers are peeled away.\n\nAs you might be able to guess, analogously to `Bool` functions representing `Pair`s,\n  this means that `Stream`s are represented by functions from `Nat`.\n\n\n### And Exponents?\n\nFixing exponents is a bad idea.\nFor one, we'd need to pick a direction to fix since exponentiation, even on types,\n  is obviously non-commutative.\nLet's choose to fix the destination, just to match with the left-to-right writing order.\n\n::: {#66370af8 .cell execution_count=21}\n``` {.haskell .cell-code}\n-- Haskell is perfectly willing to let you declare this as a type\ntype NoHalt a = Fix ((->) a)\n```\n:::\n\n\n$$\n\\text {NoHalt}(X) := \\mathcal Y((-)^X)\n= \\mathcal Y(X \\rightarrow)\n$$\n\nThere is no final destination since it gets destroyed by `Fix`.\nIf we regard functions as computations, this is one that never finishes\n  (hence the name `NoHalt`).\nHaskell always wants functions to have a return type,\n  so this suggests the type is unpopulated like `Void`.\n\n\nClosing\n-------\n\nFunction types are one of the reasons Haskell (and functional programming) is so powerful,\n  and fixed-point types allow for recursive data structures.\nFunctions on these structures are recursive, which are dangerous since they can generate paradoxes:\n\n::: {#4cf7c43c .cell execution_count=22}\n``` {.haskell .cell-code}\nvoid      = fix V :: Void            -- old\nneverend  = fix (id :: Void -> Void) -- new\ninfinity  = fix succNat :: Nat\nneverend' = fix (id :: Nat -> Nat)\n```\n:::\n\n\nIn practice, were any of these values actually present and strict computation were performed on them,\n  the program would never halt.\nThe [`absurd` ](\n    https://hackage.haskell.org/package/void-0.6.1/docs/src/Data-Void.html#absurd\n  ) function the older `Data.Void` demonstrates this.\nThe [newer version](https://hackage.haskell.org/package/base-4.16.2.0/docs/src/Data.Void.html)\n  merely raises an exception and obviates giving `Void a` constructor altogether\n  (though it still has an `id`).\n\nSince we are now posed to look at polynomials as types and generate potentially infinite types,\n  the next post will feature a heavy, perhaps surprising focus on algebra.\n\n\n### An Extra Note about Categories\n\nCategory theory is a complex and abstract field (that I myself struggle to apprehend)\n  which is difficult to recommend to total novices.\nI would, however, like to point out something interesting regarding its definition\n  of product and coproduct (sum).\n\n![](./prod_coprod.png)\n\nIn these diagrams, following arrows in one way should be equivalent to following arrows in another way.\nIf you recall the exponential laws and rewrite them in their arrowed form,\n  this definition makes a bit more sense.\n\n$$\n\\begin{gather*}\n  \\begin{matrix}\n    \\stackrel{f \\vphantom{1 \\over 2}}{(X \\times Y)^{Z}} \\vphantom{}\n    \\cong \\vphantom{} \\stackrel{f_1 \\times f_2 \\vphantom{1 \\over 2}}{X^Z \\times Y^Z}\n    \\\\[0.5em]\n    f: Z \\rightarrow(X \\times Y)\n    \\\\[0.5em]\n    f_1: Z \\rightarrow X\n    \\\\[0.5em]\n    f_2: Z \\rightarrow Y\n    \\\\[0.5em]\n    \\pi_1,\\pi_2= \\tt fst, snd\n  \\end{matrix}\n  &&\n  \\begin{matrix}\n    \\stackrel{g_1\\times g_2 \\vphantom{1 \\over 2}}{Z^{X} \\times Z^Y} \\vphantom{}\n    \\cong \\vphantom{} \\stackrel{g \\vphantom{1 \\over 2}}{Z^{X + Y}}\n    \\\\[0.5em]\n    g: (X+Y) \\rightarrow Z\n    \\\\[0.5em]\n    g_1:X \\rightarrow Z\n    \\\\[0.5em]\n    g_2: Y \\rightarrow Z\n    \\\\[0.5em]\n    \\iota_1,\\iota_2 = \\tt Left, Right\n  \\end{matrix}\n\\end{gather*}\n$$\n\nCategory theory is more general, since morphisms (function arrows)\n  need not correspond to objects (types) in the category.\nThe (pseudo-)category in which Haskell types live is \"cartesian closed\",\n  meaning that products and exponential objects exist.\nThis lets more general categories maintain their flexibility,\n  but seems like an arbitrary distinction without mentioning counterexamples.\n\n\n### Additional Links\n\n- [Representable Functors](https://bartoszmilewski.com/2015/07/29/representable-functors/)\n  (from Bartosz Milewski's Categories for Programmers)\n    - An interesting note at the end of this article mentions an interesting formal manipulation:\n      a functor $F(X)$ is represented by $\\log_X( F(X) )$\n\n",
+    "supporting": [
+      "index_files"
+    ],
+    "filters": [],
+    "includes": {}
+  }
+}
\ No newline at end of file
diff --git a/_freeze/posts/type-algebra/3/index/execute-results/html.json b/_freeze/posts/type-algebra/3/index/execute-results/html.json
new file mode 100644
index 0000000..ae2f6c6
--- /dev/null
+++ b/_freeze/posts/type-algebra/3/index/execute-results/html.json
@@ -0,0 +1,12 @@
+{
+  "hash": "3b4c8e56697e744a095c087259db845d",
+  "result": {
+    "engine": "jupyter",
+    "markdown": "---\ntitle: \"Type Algebra and You, Part 3: Combinatorial Types\"\ndescription: |\n  Isomorphisms through algebra on inducive types.\nformat:\n  html:\n    html-math-method: katex\ndate: \"2023-08-01\"\ndate-modified: \"2025-08-07\"\ncategories:\n  - haskell\n  - type theory\n  - power series\n---\n\n\n\nWe know that types have the potential to behave like numbers; the laws for addition, multiplication,\n  and exponentiation are satisfied.\nHowever, in the previous post, we also looked at some (potentially dangerous) inductive,\n  self-referential types where arithmetic tries to include the infinite:\n\n- `Nat`, the natural numbers;\n- `Any`, a chain of `Right`s followed by a `Left` wrapped around a value;\n- and `Stream`, an infinite chain of values.\n\nThis post will focus on better-behaved types which can be made to resemble familiar objects from algebra.\n\n\nGeometric Lists\n---------------\n\nWith `Stream`, there is some difficulty in peeking into the values one contains.\nWe can use its representation from `Nat` to glimpse one value at a time,\n  but we can't group an arbitrary number of them into a collection without it on forever.\n\nOn the other hand, types like `Any` which include a sum are allowed to terminate.\nWe can combine a sum and a product to create a new object, a `List`.\nHaskell comes with its own implementation, but re-implementing them is a common exercise.\n\n::: {#20302763 .cell execution_count=3}\n``` {.haskell .cell-code}\ndata List a = Null | Cons a (List a)\n```\n:::\n\n\n$$\n\\begin{gather*}\n  \\begin{matrix}\n    \\scriptsize \\text{A list of X is}\n    & \\scriptsize \\text{empty}\n    & \\scriptsize \\text{or}\n    & \\scriptsize \\text{an X}\n    & \\scriptsize \\text{and}\n    & \\scriptsize \\text{a list of X}\n    \\\\\n    L(X) = & 1 & + & X & \\times & L(X)\n  \\end{matrix}\n  \\\\ \\\\\n  \\begin{align*}\n    L(X) &= 1 + X \\cdot L(X)\n    \\\\\n    L(X) - X \\cdot L(X) &= 1\n    \\\\\n    L(X) \\cdot (1 - X) &= 1\n    \\\\\n    L(X) &= {1 \\over 1 - X}\n  \\end{align*}\n\\end{gather*}\n$$\n\nUnlike with the infinite types where 0 = 1, nothing goes wrong arithmetically.\nHowever, the resulting expression doesn't seem to make sense from the perspective of types.\nThere are no analogues to subtraction or division in type theory.\nFortunately, all we need is a trick from calculus, the Taylor series.\n\n$$\n\\begin{matrix}\n  \\scriptsize \\text{A list of X is}\n  & \\scriptsize \\text{empty}\n  & \\scriptsize \\text{or}\n  & \\scriptsize \\text{a value of X}\n  & \\scriptsize \\text{or}\n  & \\scriptsize \\text{two values of X}\n  & \\scriptsize \\text{or}\n  \\\\\n  L(X) = {1 \\over 1 - X} = & 1 & + & X & + & X^2 & + & ...\n\\end{matrix}\n$$\n\nThis is the [geometric series](https://en.wikipedia.org/wiki/Geometric_series),\n  which appears throughout algebra and analysis.\nInterestingly, since `Stream` is more primitive than `List`, this type includes its supremum, $X^\\omega$.\n\nSomething to note about the series is that there is an inherent order to the terms.\nThe 1 term is defined first, then *X*, then all subsequent ones recursively.\nThis detail also means that the $X^2$ term is more \"ordered\" than a typical pair like $X \\times X$.\n\n\n### Another Interpretation\n\nWe can equally as well define `List` in terms of `Fix` and arithmetic.\nInstead, the definition is\n\n::: {#cc7c294f .cell execution_count=4}\n``` {.haskell .cell-code}\nnewtype ListU a b = L (Maybe (a,b))\ntype List' a   = Fix (ListU a)\n```\n:::\n\n\n$$\n\\begin{gather*}\n  \\hat L(X,Z) = 1 + XZ\n  \\\\\n  L(X) = \\mathcal Y(\\hat L (X,-))\n\\end{gather*}\n$$\n\nThe expression $1 + XZ$ certainly looks like $1 - X$, if we let *Z* = -1.\nHowever, we again run into the problem that -1 doesn't seem to correspond to a type.\nWorse than that, the actual type we are after is $(1 - X)^{-1} = -1 \\rightarrow 1 - X$.\n\nThe latter type seems to resemble a function with -1 on both sides of the arrow.\nSince the resulting type is intended to resemble a fixed point, we could regard -1 as\n  a sort of \"initial type\" that gets the list started.\nThen, we can use the initial definition to replace the occurrence of -1 on the LHS with the entire LHS.\n\n$$\n\\begin{gather*}\n  (1 - X)^{-1} = -1 ~\\rightarrow~ 1 - X\n  \\\\[8pt]\n  \\begin{align*}\n    &\\phantom{=} -1\n    \\\\[8pt]\n    &\\rightarrow 1 \\textcolor{red}{-} X\n    \\\\[8pt]\n    &\\rightarrow 1 + X \\textcolor{red}{(1 - X)}\n    \\\\\n    &= 1 + X \\textcolor{blue}{-} X^2\n    \\\\[8pt]\n    &\\rightarrow 1 + X + X^2 \\textcolor{blue}{(1 - X)}\n    \\\\\n    &= 1 + X + X^2 + X^3 - X^4\n  \\end{align*}\n\\end{gather*}\n$$\n\nThis interprets the series as a [rewrite rule](https://en.wikipedia.org/wiki/Rewriting#Arithmetic).\nEach step is shown before distributing and applying the rule once more.\nIn the limit, when there are no more negative signs to rewrite, we recover the original series.\n\n\n### Convergence\n\nJust like in math, things go wrong when this expression is applied naively.\nFor example, \"a list of bools\" would seem to have the type\n\n$$\n{\\texttt{List Bool}} = L(2) \\stackrel{?}{=} {1 \\over 1 - 2} = -1\n$$\n\nIf this were true it would mean\n\n- `Either () (List Bool)` is isomorphic to Void, since $1 + (-1) = 0$\n- A list of an object *X* is isomorphic to a function from a list of bools to either\n  a unit or a tuple containing a list of bools and a value of *X*\n    - `List a ≅ List Bool -> Either () (List Bool, a)`\n\nThe first statement is obviously false, since the values `Left ()` and `Right []` will always exist.\nThe second statement is dubious.\nFor it to be true, we must imagine values of *X* can be extracted out of some (possibly infinite)\n  sequence of booleans (the *X* in the tuple), leaving behind enough information to convert\n  the rest of the list (the `List Bool` in the tuple), or be exhausted.\n\nThe latter argument requires far too much information to be generally true, so I am satisfied with\n  my previous description of -1.\nIt should only show up in the context of a fixed point expression,\n  and is only a valid type in a denominator (the return value of a function from -1).\n\n\n### Iteration\n\nConsider also a list of lists of any type *X*.\nThen by iterating lists, it would appear that\n\n$$\n\\begin{align*}\n  \\texttt{List (List a)}\n  &= L(L(X))\n  \\\\\n  &\\stackrel{?}{=}\n  {1 \\over 1 - {1 \\over 1 - X}}\n  = {X - 1 \\over X}\n\\end{align*}\n$$\n\nIf `a` were `Void`, then the only possible `List` to construct is an empty list\n  ($L(0) = {1 \\over 1 - 0} = 1$).\nWrapped in another list, the only possible values are those made by\n  repeating this any (natural) number of times.\nThis means that it is itself isomorphic to `Nat`, and we can write a bijection.\n\n::: {#9579727c .cell execution_count=5}\n``` {.haskell .cell-code}\ntoLists :: Nat -> List (List Void)\ntoLists Zero     = Null\ntoLists (Succ x) = Cons Null (toLists x)\n-- toLists x = replicate x Null\n\nfromLists :: List (List Void) -> Nat\nfromLists Null        = Zero\nfromLists (Cons x xs) = Succ (fromLists xs)\n-- fromLists = toNat . length\n\ninstance Isomorphism Nat (List (List Void)) where\n  toA = fromLists\n  toB = toLists\n\n  identityA = fromLists . toLists\n  identityB = toLists . fromLists\n```\n:::\n\n\nArithmetically, this implies $\\omega = 1 + 1 + 1^2 + ... = {1 \\over 1 - 1}$.\nMore directly, the expression has no Taylor series at 0, and the infinitude of possible values\n  spoils attempting to understand higher order terms.\nThis has big implications, since if we wrap this in another layer of lists,\n\n$$\n\\texttt{List (List (List a))} = L(L(L(X))) \\stackrel{?}{=}\n{1 \\over 1 - {1 \\over 1 - {1 \\over 1 - X}}} = ... = X\n$$\n\nwe get back to where we started, which is perfectly absurd.\nThe left-hand side can contain far more $X$s than the right-hand side.\nIn other words, by going \"past infinity\" we have ruined the correspondence between\n  the functor and a series.\n\n\nA Walk through the Woods\n------------------------\n\nAll types thus far have been of a linear form: a `List` is analogous to a line segment\n  and a `Stream` is analogous to a ray.\nAll we need to do to go from lists to binary trees is to, for every node,\n  include two sub-structures rather than one.\n\n::: {#aee22704 .cell execution_count=6}\n``` {.haskell .cell-code}\ndata Tree2 a = Leaf | Branch a (Tree2 a) (Tree2 a)\n```\n:::\n\n\n$$\n\\begin{gather*}\n  \\begin{matrix}\n    \\scriptsize \\text{A 2-tree of X is}\n    \\\\\n    T_2(X) = & 1\n    & \\scriptsize \\text{a leaf}\n    \\\\\n    & + & \\scriptsize \\text{or}\n    \\\\\n    & X \\times \\phantom{1}\n    & \\scriptsize \\text{a value of X and}\n    \\\\\n    & T_2(X) \\times \\phantom{1}\n    & \\scriptsize \\text{a left subtree of X and}\n    \\\\\n    & T_2(X) \\phantom{\\times 1}\n    & \\scriptsize \\text{a right subtree of X}\n  \\end{matrix}\n  \\\\ \\\\\n  \\begin{align*}\n    0 &= 1 - T_2(X) + X \\times T_2(X)^2\n  \\end{align*}\n\\end{gather*}\n$$\n\nSimple enough, but now we have an equation which is quadratic in our functor $T_2(X)$.\nAt this point, we can try to invoke the quadratic formula.\nLuckily, one of the solutions has a Taylor series  which consists of only positive integers,\n  just like the geometric series.\n\n$$\n\\begin{gather*}\n  a = X, b = -1, c = 1\n  \\\\[10pt]\n  \\begin{align*}\n    T_2(X) &= {1 - \\sqrt{1 - 4X} \\over 2X}\n    \\\\\n    &= 1 + X + 2X^2 + 5X^3 + 14X^4 + 42X^5 + ...\n  \\end{align*}\n\\end{gather*}\n$$\n\nThe coefficients 1, 1, 2, 5, 14, 42, ... are known as the Catalan numbers\n  ([OEIS A000108](http://oeis.org/A000108)).\nThe OEIS article also pleasantly informs that these count a kind of binary tree on\n  a given number of nodes -- one which distinguishes between left and right, as defined by the type.\n\n![\n  Rooted binary trees on a particular number of nodes.\n](./binary_trees.png)\n\nThese coefficients have a direct interpretation.\nIf we have three nodes, then there are three locations to place a value of *X*.\nIn other words, the tree holds an $X^3$.\nThe coefficient of this term tells us that a value from the type 5 tells us the shape of\n  the nodes on the tree.\n\nContrast this with the coefficients in the geometric series.\nThey are all 1, telling us that there is only a single shape for a list of a particular size.\nAs consequence, trees are in some sense \"larger\" than lists.\nFor example, a [breadth-first search](https://en.wikipedia.org/wiki/Breadth-first_search) on a binary tree\n  can collect all values at the nodes into a list.\nBut multiple trees can return the same list, so this is clearly not a bijection.\nAlgebraically, this is because the two series have different coefficients from one another.\n\n\n### Actually Solving the Polynomial\n\nWe invoked the quadratic formula to solve the polynomial $1 - T_2(X) + X \\times T_2(X)^2$,\n  but we haven't justified the ability to use it.\nNot only are square roots more suspect than division and subtraction,\n  but the quadratic formula has a choice in sign.\nCombinatorially, an initial condition determines plus or minus, and the square root is interpreted as a\n  [binomial expansion](https://en.wikipedia.org/wiki/Binomial_theorem#Newton's_generalized_binomial_theorem),\n  since $\\sqrt{1 - X} = (1 - X)^{1/2}$.\n\nNaively, the solution seems to have the following interpretation as a type:\n\n$$\n\\begin{align*}\n{1 - \\sqrt{1 - 4X} \\over 2X}\n&= (1 - (1 - 4X)^{1/2}) \\times (2X)^{-1}\n\\\\\n&= \\textcolor{red}{ (1 - ({\\scriptsize 1 \\over 2} \\rightarrow 1-4X)) \\times (-1 \\rightarrow 2X) }\n\\end{align*}\n$$\n\nCompared to the geometric series, this doesn't make sense.\n-1 appears in the first term of the product, yet originates from the second term.\nIt doesn't seem like the iteration can \"get started\" like it could previously.\n\nWe can do some algebra to get terms into the denominator.\n\n$$\n\\begin{align*}\n  {1 - \\sqrt{1 - 4X} \\over 2X}\n  &= {2 \\over 1 + \\sqrt{1 - 4X}}\n  \\\\\n  &= \\textcolor{red}{ 2 \\times (-1 \\rightarrow1 + ({\\scriptsize 1 \\over 2} \\rightarrow  1 - 4X) ) }\n  \\\\[10pt]\n  {1 \\over {1 \\over 2}(1 + \\sqrt{1 - 4X})}\n  &= \\textcolor{red}{-1 \\rightarrow {\\scriptsize 1 \\over 2} \\times (1 + ({\\scriptsize 1 \\over 2} \\rightarrow  1 - 4X) ) }\n\\end{align*}\n$$\n\nThe first expression keeps a term in the numerator.\nWithout it, the expression would generate half-integer terms which do not make sense as finite types.\nTo combat this, the second places its reciprocal in the denominator alongside the square root,\n  which appears to describe a second rewrite rule.\n\nWhile it looks slightly better, I am still unsure whether this result is interpretable.\nI am also unsure whether it is significant that 1/2 can be expressed as $2^{-1} = (-1 \\rightarrow 2)$.\nMy best guess is that some kind of mutual recursion or alternating scheme is necessary.\n\n\n### Another Solution?\n\nThere might still be some hope.\nThe earlier OEIS page mentions that the map which generates the Mandelbrot set has, in the limit,\n  a Taylor series with the Catalan numbers as coefficients.\n\n$$\n\\begin{gather*}\n  z_{n+1} = z_n^2 + c\n  \\\\\n  z \\mapsto z^2 + c\n  \\\\ \\\\\n  \\begin{matrix}\n    c & \\rightarrow & c^2 + c\n    & \\rightarrow & (c^2 + c)^2 + c\n    \\\\\n    & & & &\n    c^4 + 2c^3 + c^2 + c\n    & \\rightarrow & (c^4 + 2c^3 + c^2 + c)^2 + c\n    \\\\\n    & & & & & &\n    ... + 5c^4 + 2c^3 + c^2 + c\n    \\\\\n    & & & & & &\n    ...\n  \\end{matrix}\n\\end{gather*}\n$$\n\nThe Mandelbrot map is more similar to a type in which leaves, rather than nodes, contain values.\nWe could convert the expression to suit the trees we've been working with and to correspond better\n  with the definition of the list.\n\nThis interpretation requires special care to work, though.\nWe cannot naively assume that the input *i* obeys $i^2 = -1$,\n  since this relationship is not implied by the types.\n\n$$\n\\begin{gather*}\n  z \\mapsto 1 + cz^2\n  \\\\[8pt]\n  i \\rightarrow 1 + i^2 X\n  = (1 + i^2 X)^i\n  \\\\\n  \\stackrel{?}{=} (1 - X)^i\n  \\\\[8pt]\n  \\begin{align*}\n    &\\phantom{=} 1 \\textcolor{red}{-} X\n    \\\\[8pt]\n    &\\rightarrow 1 + X \\textcolor{red}{(1 - X)^2}\n    \\\\\n    &= 1 + X \\textcolor{blue}{-} 2 X^2 + X^3\n    \\\\[8pt]\n    &\\rightarrow 1 + X + 2 X^2 \\textcolor{blue}{(1 - X)^2} + X^3\n    \\\\\n    &= 1 + X + 2 X^2 - 3 X^3 + 2 X^4\n  \\end{align*}\n\\end{gather*}\n$$\n\nDoing so appears to work initially, but turns out to produce the series for\n  $(1 - X)^{-2}$, not $(1 - X)^i$.\n\n\nOther Trees\n-----------\n\nThe OEIS article for the Catalan numbers also mentions that the sequence counts\n  \"ordered rooted trees with *n* nodes, not including the root\".\nIn this kind of tree, a node has any number of children rather than just two.\n\nWe can construct this type of tree by as the product of a value at the node and the node's children\n  (possibly none, but themselves trees), called the *subforest*.\nA *forest* is just a list of trees.\nThis defines trees and forests in a mutually recursive way that easily lends itself to algebraic manipulation.\n\nHaskell's `Data.Graph` agrees with the following definition\n\n::: {#5ead7da6 .cell execution_count=7}\n``` {.haskell .cell-code}\ndata Tree a = Node a (List (Tree a))\ntype Forest a = List (Tree a)\n```\n:::\n\n\n$$\n\\begin{gather*}\n  \\begin{matrix}\n    \\scriptsize \\text{A tree of $X$ is}\n    & \\scriptsize \\text{a value of $X$}\n    & \\scriptsize \\text{and}\n    & \\scriptsize \\text{a forest of $X$}\n    \\\\\n    T(X) = & X & \\times & F(X)\n  \\end{matrix} \\\\\n  \\begin{matrix}\n    \\scriptsize \\text{A forest of $X$}\n    & \\scriptsize \\text{is}\n    & \\scriptsize \\text{a list of trees of $X$}\n    \\\\\n    F(X) & = & L(T(X))\n    \\\\\n    & = & {1 \\over 1-T(X)}\n    \\\\\n    & = & {1 \\over 1-X \\times F(X)}\n  \\end{matrix}\n  \\\\ \\\\\n  \\begin{align*}\n    (1 - X \\times F(X)) \\times F(X) = 1\n    \\\\\n    -1 + F(X) - X \\times F(X)^2 = 0\n    \\\\\n    1 - F(X) + X \\times F(X)^2 = 0\n  \\end{align*}\n\\end{gather*}\n$$\n\nThe resulting equation for *F*(*X*) is the same as the one featured earlier for binary trees,\n  so we know that it generates the same series.\n\n$$\n\\begin{align*}\nF(X) = T_2(X)\n&= {1 - \\sqrt{1 - 4X} \\over 2X}\n\\\\\n&= 1 + X + 2X^2 + 5X^3 + 14X^4 + 42X^5 + ...\n\\end{align*}\n$$\n\n\n### Binary Bijections\n\nTwo finite types were isomorphic when their algebraic equivalents were equal\n  (e.g., `Bool ≅ Maybe ()` because 2 = 1 + 1).\nSince these structures have the same expression in *X*, we might assume that\n  the functors are isomorphic with respect to the type *X* they contain.\n\nFor this to actually be the case, there should be a bijection between the two functors,\n  else \"isomorphic\" ceases to be the proper word.\nWith a bit of clever thinking, we can consider the left (or right) children in a binary tree as siblings,\n  and construct functions that reframe the nodes accordingly.\n\n![\n  An example of the correspondence between binary trees and \"bushes\", or general trees.\n  A root is shown for the latter to make it better resemble a tree.\n  Leaves and empty subforests not shown.\n](./bintree_bush_bijection.png)\n\n::: {#28217969 .cell execution_count=8}\n``` {.haskell .cell-code}\ntreeToForest :: Tree2 a -> Forest a\ntreeToForest Leaf           = Null\ntreeToForest (Branch x l r) =\n  Cons (Node x (treeToForest r)) (treeToForest l)\n\nforestToTree :: Forest a -> Tree2 a\nforestToTree Null                  = Leaf\nforestToTree (Cons (Node x fs) ns) =\n  Branch x (forestToTree ns) (forestToTree fs)\n\ninstance Isomorphism (Tree2 a) (Forest a) where\n  toA = forestToTree\n  toB = treeToForest\n\n  identityA = forestToTree . treeToForest\n  identityB = treeToForest . forestToTree\n```\n:::\n\n\nA weaker equality applies in combinatorics: two generating functions are equal if\n  their coefficients are equal.\nIf a closed algebraic expression is known, then it is sufficient to compare them.\nInstead, we have \"generating functors\", which satisfy the same algebraic equation,\n  have the same coefficients as a series, and most strongly,\n  are isomorphic in the sense that they have a bijection.\n\n\n### Ternary and Larger-order Trees\n\nEven though the general tree structure used above encompasses ternary trees,\n  *strictly* ternary trees have a bit less freedom.\nIn a general tree, a subtree can only appear further along a list of children if all prior elements\n  of the list are filled.\nOn the other hand, in ternary trees, subtrees can occupy any of the three possible positions.\n\nIf the binary trees functor satisfy a quadratic, then it stands to reason that ternary trees\n  should satisfy a cubic.\nAnd they do:\n\n::: {#b0ea5879 .cell execution_count=9}\n``` {.haskell .cell-code}\ndata Tree3 a = Leaf3 | Node3 a (Tree3 a) (Tree3 a) (Tree3 a)\n```\n:::\n\n\n$$\n\\begin{gather*}\n  \\begin{matrix}\n    \\scriptsize \\text{A 3-tree of X is}\n    \\\\\n    T_3(X) = & 1\n    & \\scriptsize \\text{a leaf}\n    \\\\\n    & + & \\scriptsize \\text{or}\n    \\\\\n    & X \\times \\phantom{1}\n    & \\scriptsize \\text{a value of X and}\n    \\\\\n    & T_3(X) \\times \\phantom{1}\n    & \\scriptsize \\text{a left subtree of X and}\n    \\\\\n    & T_3(X) \\times \\phantom{1}\n    & \\scriptsize \\text{a center subtree of X}\n    \\\\\n    & T_3(X) \\phantom{\\times 1}\n    & \\scriptsize \\text{a right subtree of X}\n  \\end{matrix}\n  \\\\ \\\\\n  0 = 1 - T_3(X) + X \\times T_3(X)^3\n\\end{gather*}\n$$\n\nWe can solve a cubic with the\n  [cubic formula](https://en.wikipedia.org/wiki/Cubic_equation#Cardano's_formula),\n  but it yields a result which is less comprehensible than the one for binary trees.\n\n$$\n\\begin{gather*}\n  T_3^3 + p T_3 + q = 0\n  \\\\\n  p = -1/X, q = 1/X\n  \\\\ \\\\\n  \\begin{align*}\n    T_3(X) &= \\sqrt[3]{- {1 \\over 2X}  + \\sqrt{{1 \\over 4X^2} - {1\\over 27X^3}}}\n      + \\sqrt[3]{- {1 \\over 2X} - \\sqrt{{1 \\over 4X^2} - {1\\over 27X^3}}}\n    \\\\\n    &= {1 \\over X}\\left( \\sqrt[3]{- {X^2 \\over 2}  + \\sqrt{{X^4 \\over 4} - {X^3 \\over 27}}}\n    + \\sqrt[3]{- {X^2 \\over 2} - \\sqrt{{X^4 \\over 4} - {X^3\\over 27}}} \\right)\n    \\\\[10pt]\n    &= 1 + X + 3X^2 + 12X^3 + 55X^4 + 273X^5 +...\n  \\end{align*}\n\\end{gather*}\n$$\n\nThe coefficients here are enumerated by [OEIS A001764](http://oeis.org/A001764),\n  which doesn't have a name.\nCube roots now feature prominently in the generating functor.\nThis expression is much too large for me\n  to attempt rewriting in \"functional\" form.\nWolframAlpha refuses to calculate the series from this expression within standard computation time.\nSympy gives an almost-correct series, but which has unsimplified roots of *i*\n  and has half-integer powers of *X*.\n\nA series better-suited to computation, based on angle trisection, is adapted from the OEIS here:\n\n$$\nT_3(X^2) = {2 \\over X \\sqrt{3}} \\cdot\n\\sin \\left( {1\\over 3}\\arcsin \\left(3\\cdot{X\\sqrt {3} \\over 2} \\right) \\right)\n$$\n\nThis expression invokes not only irrationals, but trigonometric functions, which are even harder\n  (if not impossible) to understand as types.\nThe situation gets even worse for higher-order trees, where\n  [no algebraic formula for the solutions exists](https://en.wikipedia.org/wiki/Abel%E2%80%93Ruffini_theorem).\nWithout being sure how to interpret the simplest case with only square roots,\n  I am unsure whether this has implications for rewrite rules.\n\n\nClosing\n-------\n\nThis hardly scratches the surface of constructible datatypes.\nAs a final example, a list which could include pairs as well as singletons of X is counted by the Fibonacci numbers:\n\n::: {#a9c3e35a .cell execution_count=10}\n``` {.haskell .cell-code}\ndata FibList a = NullF | Single a (List a) | Double (a,a) (List a)\n```\n:::\n\n\n$$\n\\begin{gather*}\n  \\begin{matrix}\n  F(X) = 1  + X \\times  F(X) + X^2 \\times F(X)\n  \\end{matrix}\n  \\\\ \\\\\n  \\begin{align*}\n    1 &= F(X) - X \\cdot F(X) - X^2 \\cdot F(X)\n    \\\\\n    1 &= F(X) \\cdot (1 - X - X^2)\n    \\\\\n    F(X) &= {1 \\over 1 - X - X^2}\n    \\\\\n    &= 1 + X + 2 X^2 + 3 X^3 + 5 X^4 + ...\n  \\end{align*}\n\\end{gather*}\n$$\n\nHowever, I do not feel that it is useful to continue plumbing for types to express as a series.\nAt this basic level, there are still mysteries I am not equipped to solve.\n\nI am the most interested in generalizing rewrite rule-style types.\nThe presence of the square root seems almost opaque.\nEven the similar Mandelbrot set rule doesn't cooperate with the \"recursive\" interpretation of -1.\nThis rule is given in terms of the variable *z*, but my goal is to is to give an intermediate meaning to -1,\n  not to introduce intermediate \"dummy\" variables.\n\nI am also interested in extending these ideas to bifunctors (polynomials in multiple variables)\n  and bi-fixes (fixing multiple terms at once, which admittedly the binary tree does already).\nPerhaps I may explore these ideas in the future.\n\nTree diagrams made with GeoGebra.\n\n\n### Links\n\n- [Haskell/Zippers](https://en.wikibooks.org/wiki/Haskell/Zippers) (from Wikibooks)\n    - Another formal manipulation: using the derivative operator on algebraic datatypes.\n      Since the Taylor series is defined in terms of derivatives, there may be a completely\n      type-theoretical characterization that doesn't rely on \"borrowing ideas\" from calculus.\n- [Generating functions for generating trees](https://www.sciencedirect.com/science/article/pii/S0012365X01002503?via%3Dihub)\n  (paper from ScienceDirect)\n    - This paper references enumerates structures by rewrite rules.\n      It also presents a zoo of combinatorial objects and their associated generating functions.\n\n",
+    "supporting": [
+      "index_files"
+    ],
+    "filters": [],
+    "includes": {}
+  }
+}
\ No newline at end of file