From c47d9cb6f11f5d5458c03e5968d7cd58376dbc92 Mon Sep 17 00:00:00 2001 From: queue-miscreant Date: Tue, 5 Aug 2025 23:37:15 -0500 Subject: [PATCH] import type-algebra from from-wordpress --- posts/type-algebra/1/index.qmd | 477 +++++++++++++++++++++++++++++++++ posts/type-algebra/2/index.qmd | 447 ++++++++++++++++++++++++++++++ posts/type-algebra/3/index.qmd | 444 ++++++++++++++++++++++++++++++ 3 files changed, 1368 insertions(+) create mode 100644 posts/type-algebra/1/index.qmd create mode 100644 posts/type-algebra/2/index.qmd create mode 100644 posts/type-algebra/3/index.qmd diff --git a/posts/type-algebra/1/index.qmd b/posts/type-algebra/1/index.qmd new file mode 100644 index 0000000..dc5afdb --- /dev/null +++ b/posts/type-algebra/1/index.qmd @@ -0,0 +1,477 @@ +--- +format: + html: + html-math-method: katex +jupyter: python3 +--- + + +Type Algebra and You, Part 1: Basics +==================================== + +When learning a new programming language, its type system can be a point of contention. Dynamic systems are fairly common in scripting languages like Python and JavaScript, which makes them great for beginners. However, it appears to be a general principle that imposing type-strictness (staticness, strength, ...) will generally allow errors to be caught before someone discovers them. + +To the computer, types are illusory, but they are not to the human. Beyond their use in programming languages, mathematicians also work with types in a purely abstract way (putting aside the fact that "type" is already an abstract concept). Types bear some resemblance to sets, yet in other ways resemble numbers and can be manipulated via algebra. In the following couple of posts, I would like to investigate these resemblances. This post will primarily focus on making the numerical resemblance clear, since it is more fundamental and everyone tends to agree on [how to define arithmetic](https://en.wikipedia.org/wiki/Peano_axioms). + +Since it can be difficult to appreciate relatively simple expressions without retreating back to programming language, I will use Haskell to demonstrate some interesting consequences of this topsy-turvy world. + + +### Starting from Square Zero + +If we can treat types as numbers, then we best start with 0. We interpret this as the number of possible values which populate the type. There are exactly zero possible values of type **0**, i.e., there is no way to construct a value with this type. In Haskell, this type is referred to as `Void`. Here is a paraphrased definition from (an earlier version of) [`Data.Void`](https://hackage.haskell.org/package/void-0.7/docs/src/Data-Void.html): + + +```{.haskell} +newtype Void = V Void +``` + +In other words, `V`, the only constructor of `Void`, requires already having a `Void`. This requires infinite regress, so it is logically impossible. + + +### Wait a minute, "only"? + +Notice that `Void` has a constructor, `V`. It has type `Void -> Void`, which means that this type is definitely populated. It resembles the [empty function](https://en.wikipedia.org/wiki/Function_%28mathematics%29#empty_function) from set theory, of which there is only one for the empty set. This means that by constructing an empty type, we've also constructed a singleton. + +Haskell already has a type with only one possible value: `()` (pronounced "unit", its only value is written identically). Can we prove that this is somehow the "same" type as `Void -> Void`? Of course! Remember, Haskell is a functional language. Therefore, we should focus on writing functions between the two types. + +```{.haskell} +toUnit :: (Void -> Void) -> () +fromUnit :: () -> (Void -> Void) +``` + +The "to" and "from" in the names suggests that if we do one followed by the other, we should end up where we started. Or, in the language of functions, the composition of the functions is the identity. + +```{.haskell} +-- fromUnit . toUnit = id :: (Void -> Void) -> (Void -> Void) +-- toUnit . fromUnit = id :: () -> () +``` + +In other words, we can reversibly map values from one type to the other (and vice versa). If such functions (also known as bijections) exist, then the types are *isomorphic*. I haven't actually defined the bijection yet; it is simple, if exhaustive: + +```{.haskell} +toUnit V = () +fromUnit () = V +``` + +In future examples showing isomorphic types, I will define only of the bijections to save a bit of vertical space. For the other, I'll show only the type annotation. + + +Hyperoperative (Multi)functors +------------------------------ + +Another way to go from 0 to 1 is to just add one, an operation also called the [successor function](https://en.wikipedia.org/wiki/Successor_function). "Function" is vague here, since it is evocative of a mapping between values, rather than a mapping between types. [Kinds](https://wiki.haskell.org/Kind) live one step up from types, and we can conjecture the kind a successor "function" on types would have. + +```{.haskell} +succ :: Int -> Int -- the successor function constructs an integer from an integer +Succ :: * -> * -- so we need to be able to construct a "bigger" type from a type +``` + +The word with the closest meaning is [*functor*](https://wiki.haskell.org/Functor), which Haskell already uses to refer to types with a manipulable "inside" that can be mapped over. Fortunately, the kind of `Succ` matches what Haskell expects `Functor`s to look like (and in fact, since GHC 6.12.1, the compiler is smart enough to derive the definition on its own). + +The functor in Haskell which most closely resembles the successor is `Maybe`. + +```{.haskell} +data Maybe a = Nothing | Just a +type One = Maybe Void +``` + +$$ +\begin{matrix} +\scriptsize \text{A Maybe of $X$ is either} & +\scriptsize \text{Nothing} & +\scriptsize \text{or} & +\scriptsize \text{a value of $X$} & +\\ +S(X) := & 1 & + & X \\ +\scriptsize \text{The 1-valued type is} & +\scriptsize \text{Nothing} & +\scriptsize \text{or} & +\scriptsize \text{logically impossible} & \\ +\bold{1} =& 1 &+& 0 +\end{matrix} +$$ + +Since `Void` is has zero possible values, we should expect `Maybe Void` to have exactly one possible value. Constructing a `Just Void` would require that we already had a Void value, which is impossible. Therefore, `Nothing` is the only possible value of `Maybe Void`. + +```{.haskell} +toUnitM :: Maybe Void -> () +toUnitM Nothing = () +-- toUnitM (Just Void) is fictitious + +-- fromUnitM :: () -> Maybe Void +-- fromUnitM . toUnitM = id :: Maybe Void -> Maybe Void +-- toUnitM . fromUnitM = id :: () -> () +``` + + +### Sums and Products + +If there's a functor which resembles the successor, then are there ones which also resemble addition and multiplication? Not exactly. Functors are strictly a single-argument kind, and luckily the successor is a unary function. Addition and multiplication are binary, so they require a slightly more complicated kind: + +```{.haskell} +(+) :: Int -> Int -> Int -- we can add two things together +Plus a b :: * -> * -> * -- so we want to be able to add two types together +(*) :: Int -> Int -> Int -- likewise, we can multiply two things +Mult a b :: * -> * -> * -- and we want to be able to multiply two types +``` + +These kinds match what Haskell expects `Bifunctor`s to look like. Types get complicated when more than one parameter is involved, so GHC cannot derive `Bifunctor`. Alternatively, we can just consider bifunctors as they appear here: a functor with an arity of 2. + +Putting aside semantics, Haskell indeed has two types resembling type addition and type multiplication. Respectively, they are `Either` and `(,)` (i.e., a 2-tuple): + +```{.haskell} +data Either a b = Left a | Right b +data (,) a b = (,) a b +``` + +$$ +\begin{matrix} +\scriptsize \text{Either $X$ or $Y$ is} & +\scriptsize \text{a value of $X$} & +\scriptsize \text{or} & +\scriptsize \text{a value of $Y$} & +\\ +E(X,Y) := & X & + & Y +\\ +\scriptsize \text{A tuple of $X$ and $Y$ is} & +\scriptsize \text{a value of $X$} & +\scriptsize \text{and} & +\scriptsize \text{a value of $Y$} & +\\ +P(X,Y) := & X & \times & Y +\end{matrix} +$$ + +Product types are common (consider any `struct` or tuple in a more common language, but sum types are less so. `union`s in C get close, but they are bound too memory for our purposes. Using addition, we can actually reconstruct the successor from **1**: + +```{.haskell} +type Maybe' a = Either () a + +toMaybe' :: Maybe a -> Maybe' a +toMaybe' Nothing = Left () +toMaybe' (Just x) = Right x + +-- fromMaybe' :: Maybe' a -> Maybe a +-- fromMaybe' . toMaybe' = id :: Maybe a -> Maybe a +-- toMaybe' . fromMaybe' = id :: Maybe' a -> Maybe' a +``` + +`Left ()` now takes on the role of `Nothing`, while all the `Right`s come from the type parameter `a`. + + +### Rearranging and Rebracketing + +Within the world of numbers, addition and multiplication are commutative and associative. Is the same true for types? + +Commutativity is obvious, since we can construct functions which switch *X* and *Y* around. Haskell already provides these functions, whose definitions I have copied here + +```{.haskell} +swapEither :: Either a b -> Either b a +swapEither (Left x) = Right x +swapEither (Right x) = Left x + +swap :: (a, b) -> (b, a) +swap (x, y) = (y, x) + +-- swapEither . swapEither = id :: Either a b -> Either a b +-- swap . swap = id :: (a, b) -> (a, b) +``` +[swapEither](https://hackage.haskell.org/package/either-5.0.2/docs/Data-Either-Combinators.html#v:swapEither)
+[swap](https://hackage.haskell.org/package/base-4.16.1.0/docs/Data-Tuple.html#v:swap) + +Associativity is a bit trickier, since it deals with triples rather than pairs. + +```{.haskell} +assocRightSum :: Either a (Either b c) -> Either (Either a b) c +assocRightSum (Left x) = Left (Left x) +assocRightSum (Right (Left y)) = Left (Right y) +assocRightSum (Right (Right z)) = Right z + +-- assocLeftSum :: Either (Either a b) c -> Either a (Either b c) +-- assocLeftSum . assocRightSum = id :: Either a (Either b c) -> Either a (Either b c) +-- assocRightSum . assocLeftSum = id :: Either (Either a b) c -> Either (Either a b) c + +assocRightProd :: (a, (b, c)) -> ((a, b), c) +assocRightProd (x, (y, z)) = ((x, y), z) + +-- assocLeftProd :: ((a, b), c) -> (a, (b, c)) +-- assocLeftProd . assocRightProd = id :: (a, (b, c)) -> (a, (b, c)) +-- assocRightProd . assocLeftProd = id :: ((a, b), c) -> ((a, b), c) +``` + +In fact, since we don't care about order or grouping, we can forget both entirely and map them instead into 3-tuples and a triple-sum type: + +```{.haskell} +data Either3 a b c = Left3 a | Center3 b | Right3 c +data (,,) a b c = (,,) a b c + +toLeftSum :: Either3 a b c -> Either (Either a b) c -- x+y+z = (x+y)+z +toLeftSum (Left3 x) = Left (Left x) +toLeftSum (Center3 y) = Left (Right y) +toLeftSum (Right3 z) = Right z + +-- fromLeftSum :: Either (Either a b) c -> Either3 a b c +-- fromLeftSum . toLeftSum = id :: Either3 a b c -> Either3 a b c +-- toLeftSum . fromLeftSum = id :: Either (Either a b) c -> Either (Either a b) c + +toLeftProd :: (a,b,c) -> ((a,b),c) +toLeftProd (x,y,z) = ((x,y),z) + +-- fromLeftProd :: ((a,b),c) -> (a,b,c) +-- fromLeftProd . toLeftProd = id :: (a,b,c) -> (a,b,c) +-- toLeftProd . fromLeftProd = id :: ((a,b),c) -> ((a,b),c) +``` + +There's still a bit of work to prove associativity *in general* from these local rules, but we're still primarily concerned with the equivalent functors `Either` and `(,)`, which are local anyway. + + +### Other Arithmetic Properties + +Naturally, **0** and **1** satisfy their typical properties. There are additional interpretations, however: + +| Property | Arithmetic | Haskell | Reasoning +|----------------------------|---------------------|---------|----------- +| Additive Identity | $0 + X \cong X$ | `Either Void a` is equivalent to `a` | Since **0** is unoccupied, its sum with any other type can only ever contain values from that other type (i.e., only `Right` values). +| Multiplicative Identity | $1 \cdot X \cong X$ | `((), a)` is equivalent to `a` | Since **1** has exactly one possible value, its product with any other type is this value and any value from the other type (i.e., tuples of the form `((), x)`). +| Multiplicative Annihilator | $0 \cdot X \cong 0$ | `(Void, a)` is equivalent to `Void` | Since **0** is unoccupied, we cannot construct a type which requires a value from it (i.e., writing a tuple of the form `(Void, x)` requires having a `Void` value). + + +### Distributivity + +Finally, to hammer home the resemblance to normal arithmetic, we should consider the distribution of multiplication over addition. We can first see that multiplication does distribute over the successor: + +```{.haskell} +type SuccDist a b = ((Maybe a), (Maybe b)) +data SumProd a b = Nada | LProd a | RProd b | BothProd a b +``` + +$$ +\begin{matrix} +\scriptsize \text{Maybe $X$ and Maybe $Y$} & \scriptsize \text{is equivalent to} \\ +(1 + X) \cdot (1 + Y) \cong \\ +1 +& \scriptsize \text{Both Nothing}\\ ++ X \phantom{\cdot Y} +& \scriptsize \text{or Just $x$, Nothing} \\ ++ \phantom{X \cdot} Y & \scriptsize \text{or Nothing, Just $y$} \\ ++ X \cdot Y & \scriptsize \text{or Just $x$, Just $y$} \\ +\end{matrix} +$$ + +If we forbade the first and last cases (in other words, if we "subtract" them out), then the type would be equivalent to the sum of *X* and *Y*. + +```{.haskell} +toSuccDist :: Either a b -> SuccDist a b +toSuccDist (Left x) = (Just x, Nothing) +toSuccDist (Right y) = (Nothing, Just y) + +fromSuccDist :: SuccDist a b -> Either a b +fromSuccDist (Just x, Nothing) = Left x +fromSuccDist (Nothing, Just y) = Right y +fromSuccDist _ = undefined -- non-exhaustive! + +-- fromSuccDist . toSuccDist = id :: Either a b -> Either a b +-- toSuccDist . fromSuccDist /= id -- because of extra values +``` + +Fortunately, general distributivity is also relatively simple. We do as grade schoolers do and FOIL out the results... + +```{.haskell} +type PreDist a b c d + = (Either a b, Either c d) +data PostDist a b c d + = F a c | O a d | I b c | L b d + -- first, outer, inner, last +``` + +$$ +\begin{matrix} +\scriptsize \text{Either $X$ $Y$ and Either $Z$ $W$} & \scriptsize \text{is equivalent to} \\ +(X + Y) \cdot (Z + W) \cong \\ + \phantom{+} X \cdot Z +& \scriptsize \text{Firsts,}\\ +\vphantom{} + X \cdot W +& \scriptsize \text{Outers,} \\ +\vphantom{}+ Y \cdot Z +& \scriptsize \text{Inners,} \\ +\vphantom{}+ Y \cdot W +& \scriptsize \text{or Lasts} \\ +\end{matrix} +$$ + +...then construct our bijections: + +```{.haskell} +distribute :: PreDist a b c d -> PostDist a b c d +distribute (Left x, Left z) = F x z +distribute (Left x, Right w) = O x w +distribute (Right y, Left z) = I y z +distribute (Right y, Right w) = L y w + +-- undistribute :: PostDist a b c d -> PreDist a b c d +-- undistribute . distribute = id :: PreDist a b c d -> PreDist a b c d +-- distribute . undistribute = id :: PostDist a b c d -> PostDist a b c d +``` + +This works primarily because without further information about any of the types `a`, `b`, `c`, `d`, we can only rearrange them. It may be the case that `a ~ (b -> d)` (a function from `b` to `d`), meaning that we could lose the distinction between the instances `O` and `L` (and be unable to `undistribute`). But we don't have enough information to define `distribute` in any other way than the above. A similar argument holds for our other bijections. + + +Bools, Bools, and more Bools +---------------------------- + +While it's all well and good that these operations appear to mirror familiar arithmetic, we haven't counted farther than **0** and **1**. Everyone past the age of four recognizes that **2** comes next. Fortunately, this corresponds to a much better-known type: booleans. Rather than defining them as numbers like in lower-level languages (as a computer would understand), we can construct them directly as abstract values in Haskell + +```{.haskell} +data Bool = True | False +``` + +$$ +\begin{matrix} +\scriptsize \text{A bool is either} & +\scriptsize \text{True} & +\scriptsize \text{or} & +\scriptsize \text{False} & +\\ +\text{Bool} := & 1 & + & 1 &= \bold{2} +\end{matrix} +$$ + +Bools may also be defined using the above functors, either by two successors or by addition: + +```{.haskell} +type BoolSucc = Maybe (Maybe Void) -- succ (succ 0) + +toBoolSucc :: Bool -> BoolSucc +toBoolSucc False = Nothing +toBoolSucc True = Just Nothing + +-- fromBoolSucc :: BoolSucc -> Bool +-- fromBoolSucc . toBoolSucc = id :: Bool -> Bool +-- toBoolSucc . fromBoolSucc = id :: BoolSucc -> BoolSucc + +type BoolEither = Either () () -- 1 + 1 + +toBoolEither :: Bool -> BoolEither +toBoolEither False = Left () +toBoolEither True = Right () + +-- fromBoolEither :: BoolEither -> Bool +-- fromBoolEither . toBoolEither = id :: Bool -> Bool +-- toBoolEither . fromBoolEither = id :: BoolEither -> BoolEither +``` + + +### Four Great Justice + +Rather than progressing to **3**, let's jump to **4**. The number 2 has an interesting property: its sum with itself is its product with itself (is its exponent with itself...) is 4. Thus, the following types all encode a four-valued type: + +```{.haskell} +data Four = Zero | One | Two | Three +type FourSucc = Maybe (Maybe Bool) +type FourSum = Either Bool Bool +type FourProd = (Bool, Bool) +``` + +$$ +\begin{align*} +4 &:= 1+1+1+1 \\ +&\phantom{:}\cong S(S(2)) \\ +&\phantom{:}\cong E(2,2) = 2 + 2 \\ +&\phantom{:}\cong P(2,2) = 2 \cdot 2 \\ +\end{align*} +$$ + +Showing 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. + +```{.haskell} +toFourSucc :: Four -> FourSucc +toFourSucc Zero = Nothing +toFourSucc One = Just Nothing +toFourSucc Two = Just (Just False) +toFourSucc Three = Just (Just True) + +-- fromFourSucc :: FourSucc -> Four +-- fromFourSucc . toFourSucc = id :: Four -> Four +-- toFourSucc . fromFourSucc = id :: FourSucc -> FourSucc + +toFourSum :: Four -> FourSum +toFourSum Zero = Left False -- 00 +toFourSum One = Left True -- 01 +toFourSum Two = Right False -- 10 +toFourSum Three = Right True -- 11 + +-- fromFourSum :: FourSum -> Four +-- fromFourSum . toFourSum = id :: Four -> Four +-- toFourSum . fromFourSum = id :: FourSum -> FourSum + +toFourProd :: Four -> FourProd +toFourProd Zero = (False, False) -- 00 +toFourProd One = (False, True) -- 01 +toFourProd Two = (True, False) -- 10 +toFourProd Three = (True, True) -- 11 + +-- fromFourProd :: FourProd -> Four +-- fromFourProd . toFourProd = id :: Four -> Four +-- toFourProd . fromFourProd = id :: FourProd -> FourProd +``` + + +### Hiding in the Clouds + +Though I mentioned exponentiation earlier, I did not show the equivalent for types. Set theorists sometimes write [the set of functions from one set *A* to another set *B*](https://en.wikipedia.org/wiki/Function_type) as $B^A$ because the number of possible functions comes from the cardinalities of the sets: $|B|^{|A|}$. We previously examined how the constructor for Void is a singleton, which satisfies the equation $0^0 = 1$. At least in the finite world, sets and types are not so different, and indeed, we can write + +```{.haskell} +type FourFunc = Bool -> Bool +-- there are exactly four functions: +taut x = True -- tautology +cont x = False -- contradiction +id' x = x -- identity +not' x = not x -- negation +``` + +$$ +2 \rightarrow 2 = 2^2 \cong \bold 4 +$$ + +If we want to map these functions onto our `Four` type, we can again examine the binary expansion of the numbers 0-3. This time, the first place value encodes the value of the function on `False`, and the second value the same on `True`. + +```{.haskell} +toFourFunc :: Four -> FourFunc +-- easiest to consider binary place values as input +-- 10 +toFourFunc Zero = cont -- 00 +toFourFunc One = not' -- 01 +toFourFunc Two = id' -- 10 +toFourFunc Three = taut -- 11 + +-- fromFourFunc :: FourFunc -> Four +-- fromFourFunc . toFourFunc = id :: Four -> Four +-- toFourFunc . fromFourFunc = id :: FourFunc -> FourFunc +``` + +For larger functions, we can see a more generalizable mapping from the truth table, shown here for AND + +| Column Number | Binary | Input (x) | Input (y) | x AND y | +|---------------|--------|-----------|-----------|---------| +| 0 | 00 | False | False | False | +| 1 | 01 | False | True | False | +| 2 | 10 | True | False | False | +| 3 | 11 | True | True | True | + +Going up the final column and converting to binary digits, we can read "1000", which is the binary expansion of 8. The other numbers from 0 to $(2^2)^2 - 1$ can similarly be associated to boolean functions `Bool -> (Bool -> Bool)`. Note that function arrows are assumed to be right-associative, but this is opposite the right-associativity of typical exponentiation. I'll dive deeper into why this needs to be the case later. + + +Closing +------- + +If you know your Haskell, especially the difference between `data` and `newtype`, then you know about the slight stretching of the truth I have performed. Yes, it is true that types defined with `data` implicitly add a possible `undefined` value which can tell the runtime to error out. Everyone who knows Haskell better than me says [not to worry about it in most cases](https://wiki.haskell.org/Newtype). At worst, it would make some of the pretty arithmetic above go away. + +Other fascinating concepts live in this world, such as the [Curry-Howard correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence). Rather than discussing them, in the next post I would like to press onward with the algebra. I have spent this post laying the groundwork for arithmetic on types, so it will focus more upon recursion and fixed points. + +A Haskell file containing all of the code on this page can be found [here](). + + +### Additional Links + +- [Algebraic Data Types](https://en.wikipedia.org/wiki/Algebraic_data_type) (Wikipedia) +- [Generically Deriving Bifunctor](https://blog.csongor.co.uk/generic-deriving-bifunctor/) (Blogpost by Csongor Kiss) diff --git a/posts/type-algebra/2/index.qmd b/posts/type-algebra/2/index.qmd new file mode 100644 index 0000000..635e7e5 --- /dev/null +++ b/posts/type-algebra/2/index.qmd @@ -0,0 +1,447 @@ +--- +format: + html: + html-math-method: katex +jupyter: python3 +--- + + +Type Algebra and You, Part 2: A Fixer-upper +=========================================== + +In the [previous post](), I wrote mostly about finite types, as well as type addition (`Either`) and multiplication (`(,)`). This post will focus on another important operation, exponentiation, before moving on to recursively-defined types. + + +Exponent Laws +------------- + +I mentioned at the end of the previous post that exponents correspond to functions. It's not a stretch to say that without them, nothing would get done in a program. They are denoted in the following way + +```{.haskell} +type Exponent a b = (->) a b +-- equivalent to `a -> b` +``` + +$$ +\text{Exp}(X,Y) := Y^X = X \rightarrow Y +$$ + +The arrow constructor (typically infixed) appears everywhere in Haskell types. But is the corresponding notation $Y^X$ fitting or merely illusory? + + +### Exponentiation Distributes over Multiplication + +One law of exponents states that if we have a product raise it to an exponent, then the exponent should distribute to both terms. In types, this is + +$$ +\stackrel{\text{A function to a product}}{Z \rightarrow (X \times Y)} += (X\times Y)^{Z} +\stackrel{?}{\cong} X^Z \times Y^Z += \stackrel{\text{A pair of functions with a common input}}{(Z \rightarrow X) \times (Z \rightarrow Y)} +$$ + +This says that a function `f` returning a pair can be decomposed as a pair of functions `g` and `h` returning each component. If we wish to convert form the former to the latter, we can call `f`, then use the functions that give either element of the tuple (`fst` and `snd`). Conversely, if we instead have a pair of functions from the same type, then we can just send the same value to both and put it in a pair. + +```{.haskell} +distExp :: (a -> (b, c)) -> (a -> b, a -> c) +distExp f = (\x -> fst (f x), \x -> snd (f x)) +-- distExp f = (fst . f, snd . f) + +undistExp :: (a -> b, a -> c) -> (a -> (b, c)) +undistExp (g, h) = \x -> (g x, h x) + +-- undistExp . distExp = id :: (a -> (b, c)) -> (a -> (b, c)) +-- distExp . undistExp = id :: (a -> b, a -> c) -> (a -> b, a -> c) +``` + +Unlike with the sum and product, the identities here exist on functions themselves. Fortunately, Haskell is [referentially transparent](https://en.wikipedia.org/wiki/Referential_transparency), so we could deepen the proof by composing the functions and using lambda calculus rules until the expression is clearly an identity. If we wanted to, it would be possible to do the same for the identities on the previous post. In the interest of being concise, I won't be doing so. + + +### Product of Exponents is an Exponent of a Sum + +We also know that if two expressions with same base are multiplied, their exponents should add. So at the type level, we must check the equivalence of the following + +$$ +\stackrel{\text{A pair of functions with a common return}}{(X \rightarrow Z) \times (Y \rightarrow Z)} += Z^{X} \times Z^Y +\stackrel{?}{\cong} Z^{X + Y} += \stackrel{\text{A function on a sum}}{(X + Y) \rightarrow Z} +$$ + +This says that a pair of functions `g` and `h` with the same return type can be composed into a function `f`. If we start with the former, we must create a function `f` on `Either` which decides which function to use. If we have this function already, we can get back to where we started by putting our values into `Either` with `Left` or `Right` before using `f`. The bijections look like + +```{.haskell} +toExpSum :: (a -> c, b -> c) -> (Either a b -> c) +toExpSum (g, h) = \w -> case w of + Left x -> g x + Right y -> h y + +fromExpSum :: (Either a b -> c) -> (a -> c, b -> c) +fromExpSum f = (\x -> f (Left x), \y -> f (Right y)) +-- fromExpSum f = (f . Left, f . Right) + +-- fromExpSum . toExpSum = id :: (a -> c, b -> c) -> (a -> c, b -> c) +-- toExpSum . fromExpSum = id :: (Either a b -> c) -> (Either a b -> c) +``` + +This identity actually tells us something very important regarding the definition of functions on sum types: they must have as many definitions (i.e., a *product* of definitions) as there are types in the sum. This has been an implicit part of all bijections involving `Either`, since they have a path for both `Left` and `Right`. + + +### Exponent of an Exponent is an Exponent of a Product + +Finally (arguably as consequence of the first law), if we raise a term with an exponent to another exponent, the exponents should multiply. + +$$ +\stackrel{\text{A function returning a function}}{X \rightarrow (Y \rightarrow Z)} = (Z^{Y})^X +\stackrel{?}{\cong} +Z^{X \times Y} = \stackrel{\text{A function on a product}}{(X \times Y) \rightarrow Z} +$$ + +We start with a function which returns a function and end up with a function from a product. The equivalence of these two types is [currying](https://en.wikipedia.org/wiki/Currying), an important concept in computer science. Haskell treats it so importantly that the bijections are almost trivial + +```{.haskell} +curry' :: (a -> (b -> c)) -> ((a, b) -> c) +curry' f = \(x, y) -> (f x) y +-- curry' f (x, y) = f x y + +uncurry' :: ((a, b) -> c) -> (a -> b -> c) +uncurry' f = \x -> \y -> f (x, y) +-- uncurry' f x y = f (x, y) + +-- uncurry' . curry' = id :: (a -> b -> c) -> (a -> b -> c) +-- curry' . uncurry' = id :: ((a, b) -> c) -> ((a, b) -> c) +``` + +These come pre-implemented in Haskell since tuples are harder to define than a chain of arrows. + + +Double-Checking for Algebra +--------------------------- + +Even though we've established that sums, products, and exponents obey their normal arithmetical rules, we've yet to lay the groundwork for algebra. In algebra, we start by introducing a symbol called *x* and allow it to interacting with numbers. This means that it obeys the arithmetical laws that have been established. + +Functors allow us to parametrize a type in a similar way to this. We already know how to add and multiply finite types, for a "variable" type *X*, it bears checking that it can add and multiply with itself. + + +### Coefficients + +Is it truly the case that an object's sum with itself is its product with a 2-valued type? It should follow from addition laws, but it might behoove us to check + +```{.haskell} +type LeftRight a = Either a a +-- LeftRight a ≅ (Bool, a) +``` +$$ +X + X \stackrel{?}\cong 2 \times X +$$ + +It's actually quite simple if we look back at the implementation of `Bool` as `Either () ()`. `False` values go on the `Left`, and `True` values go on the `Right`: + +```{.haskell} +to2Coeff :: LeftRight a -> (Bool, a) +to2Coeff (Left x) = (False, x) +to2Coeff (Right x) = (True, x) + +-- from2Coeff :: (Bool, a) -> LeftRight a +-- from2Coeff . to2Coeff = id :: Either a a -> Either a a +-- to2Coeff . from2Coeff = id :: (Bool, a) -> (Bool, a) +``` + +We can continue adding *X* to itself using `Either` to obtain arbitrarily high coefficients. This is simplest as `Either a (Either a (... (Either a a)))`, where values are a chain of `Right`s ending in a `Left`. Then, the maximum number of `Right`s allowed is *n* - 1. Counting zero, there are *n* values, demonstrating the type *n*. + + +### Exponents + +Multiplying *X* by a finite type is all well and good, but we should also check that it can multiply like itself. If all is well, then this should be equivalent to raising *X* to an exponent. We've already discussed those laws, but just in case, we should check + +```{.haskell} +type Pair a = (a, a) +-- Pair a ≅ (Bool -> a) +``` + +$$ +X \times X \stackrel{?}{\cong} +X^2 = 2 \rightarrow X +$$ + +To wit, we express the pair as a function from the finite type `Bool`. If we have our pair of *X*, then we know our output is one of the two, and return a function that decides to return. On the other hand, we need only apply a function from `Bool` to every possible value in `Bool` as many times as it appears (twice) and collect it in a product to get back to where we started. The bijections to and from this type look like this + +```{.haskell} +to2Exp :: (a, a) -> (Bool -> a) +to2Exp (x, y) = \p -> case p of + False -> x + True -> y + +from2Exp :: (Bool -> a) -> (a, a) +from2Exp f = (f False, f True) + +-- from2Exp . to2exp = id :: (a, a) -> (a, a) +-- to2Exp . from2Exp = id :: (Bool -> a) -> (Bool -> a) +``` + +This a special case of what are called *representable functors*. The functor in question is `Pair`, represented by functions from `Bool`. A similar argument can be shown for any *n* that $\overbrace{X \times X \times ... \times X}^n$ can be represented functions from *n*. + +Together, these two isomorphisms mean that any polynomial whose coefficients are positive integers can be interpreted as a functor in *X*. + + +Fixing What Ain't Broke +----------------------- + +Exponents, finite types and polynomials are wonderful, but we need to go further. Even though we have access to types for any natural number, we can only define finite arithmetic within them. We could inflate the number of possible values in a naive way... + + +```{.haskell} +data Nat = Zero | One | Two | Three | Four | Five | ... +``` + +$$ +\begin{matrix} & +\scriptsize \text{Zero} & \scriptsize \text{or} & +\scriptsize \text{One} & \scriptsize \text{or} & +\scriptsize \text{Two} & \scriptsize \text{or} +\\ +X =& 1 &+& 1 &+& 1 &+& ... +\end{matrix} +$$ + +...but this is akin to programming without knowing how to use loops. In Haskell, we approach (potentially infinite) loops recursively. One of the simplest ways we can recurse is by using a [fixed-point combinator](https://en.wikipedia.org/wiki/Fixed-point_combinator). While typically discussed at the value level as a higher-order function, there also exists a similar object at the type level which operates on functors. Haskell implements this type in [`Data.Fix`](https://hackage.haskell.org/package/data-fix-0.3.2/docs/Data-Fix.html), from which I have copied the definition below + +```{.haskell} +-- Fix :: (* -> *) -> * +data Fix f = In { out :: (f (Fix f)) } + +-- compare with the functional fixed-point +fix :: (a -> a) -> a +fix f = let x = f x in x +``` + +$$ +\mathcal{Y}(F(X)) := F(\mathcal Y (F)) +$$ + +("Y" here comes from the Y-combinator, which isn't entirely accurate, but is fitting enough) + +If we `Fix` a functor `f` Values of this type are the functor `f` containing a `Fix f`. In other words, it produces a new type containing itself. + + +Au Naturale +----------- + +To demonstrate how this extends what the kinds of types we can define, let's work out the natural numbers. [Peano arithmetic](https://en.wikipedia.org/wiki/Peano_axioms) gives them a recursive definition: they are either 0 or the successor of another natural number. The "naive" definition in Haskell is very simple. Arithmetically, though, things seem to go wrong. + +```{.haskell} +data Nat' = Zero | Succ Nat' + +zero = Zero +one = Succ Zero +two = Succ one +... +``` + +Values in `Nat'` are a string of `Succ`s which terminate in a `Zero`. Of course, we also could define this in terms of `Fix`. First, we need to define a type to fix, then apply the operator + +```{.haskell} +type NatU a = Zero | Succ a +type NatF = Fix NatU -- possible values are "Y Zero" or "Y (Succ (x :: Fix NatU))" +``` + +If we look at things a little closer, we realize that this type has the exact same form as the successor functor, `Maybe`. + +```{.haskell} +type Nat = Fix Maybe + +zero = In Nothing +one = In (Just zero) +two = In (Just one) +... +``` + +$$ +\text{Nat} \text{ or } \omega := \mathcal Y(S) +$$ + +Looking back, the statement $X = 1 + X$ is identical to the statement "*X* is the fixed point of the successor", as its definition implies. Using the latter form, we can define a bijection to and from `Int` (which I'm regarding as only containing positive integers) as + +```{.haskell} +toNat :: Int -> Nat +toNat 0 = In Nothing +toNat x = In $ Just $ toNat $ x - 1 -- the successor Nat of the predecessor of x + +fromNat :: Nat -> Int +fromNat (In Nothing) = 0 +fromNat (In (Just x)) = 1 + fromNat x -- ...of the predecessor of In (Just x) + +-- fromNat . toNat = id :: Int -> Int -- for positive integers +-- toNat . fromNat = id :: Nat -> Nat +``` + +These bijections are different from the ones we have seen thus far. Both of them are defined recursively, just like our functorial `Fix`. Consequently, rather than exhausting the possible cases, it relies on deconstructing `Nat`s and arithmetic on `Int`s. + +```{.haskell} +succNat :: Nat -> Nat +succNat x = In (Just x) +-- succNat x = In . Just + +succInt :: Int -> Int +succInt x = x + 1 +``` + +There's actually no way to know whether the functions above do the same thing, at least without knowing more about `Int`. At best, they afford us a way to bootstrap a way to display numbers that isn't iterated `Just`s. + + +Functors from Bifunctors +------------------------ + +If their first argument of a bifunctor is fixed, then what remains is a functor. + +```{.haskell} +forall a. Either a :: * -> * +``` + +But since this is a functor, we can apply `Fix` to it. + +```{.haskell} +type Any a = Fix (Either a) +--Any' a ~ (Either a (Any' a)) + +leftmost x = In (Left x) +oneRight x = In (Right (leftmost x)) +twoRight x = In (Right (oneRight x)) +``` + +$$ +\text{Any}(X) := \mathcal Y(E(X,-)) += \mathcal Y(X +) +$$ + +Remember what was said earlier about types which look like nested `Either a`? This type encompasses all of those (granted, interspersed with the `Fix` constructor). + +I used the names "one" and "two" in the above example functions to suggest similarity to Nat above. In fact, if `a ~ ()`, then because we already our functor `Either ()` is isomorphic to `Maybe`, we know that `Any ()` is isomorphic to `Nat`. If the type was `Any Bool`, We could terminate the chains in either `Left True` or `Left False`; it is isomorphic to `(Nat, Bool)`. In general, `Any a` is isomorphic to `(Nat, a)`. + +```{.haskell} +toAny :: (Nat, a) -> Any a +toAny (In Nothing, x) = In (Left x) +toAny (In (Just n), x) = In (Right (toAny (n, x))) + +-- fromAny :: Any a -> (Nat, a) +-- fromAny . toAny = id :: (Nat, a) -> (Nat, a) +-- toAny . fromAny = id :: Any a -> Any a +``` + +Note how fixing a sum-like object gives a product-like object. + + +### What about Products? + +If we can do it for sums, we should be able to do it for products. However, unlike sums, products don't have a builtin exit point. For `Either`, all we need to do is turn `Left` and be done, but fixing a product goes on endlessly. + +```{.haskell} +type Stream a = Fix ((,) a) +-- Stream a ~ (a, Stream a) + +repeatS x = In (x, repeatS x) + -- = In (x, In (x, ... +``` + +$$ +\text{Stream}(X) := \mathcal Y(P(X,-)) = +\mathcal Y(X \times) +$$ + +Unlike `Void`, whose "definition" would require an infinite chain of constructors, we can actually create values of this type, as seen above with the definition of `repeatS.` Fortunately, Haskell is lazy and doesn't actually try to evaluate the entire result. + +If fixing a sum produced a product object with a natural number, then it stands to reason that fixing a product will produce an exponential object with a natural number. By this token, we should try to verify that $\text{Stream}(X) \cong X^{\omega} = \text{Nat} \rightarrow X$. Intuitively, we have an value of type *X* at every position of a stream defined by a natural number (the input type). This specifies every possible position. + +```{.haskell} +toStream :: (Nat -> a) -> Stream a +toStream f = toStream' (In Nothing) where + toStream' n = In (f n, toStream' (In (Just n))) + +fromStream :: Stream a -> (Nat -> a) +fromStream (In (x,y)) = \n -> case n of + In Nothing -> x + In (Just m) -> fromStream y m + +-- fromStream . toStream = id :: (Nat -> a) -> (Nat -> a) +-- toStream . fromStream = id :: Stream a -> Stream a +``` + +Notice that in `toStream`, an equal number of "layers" are added to `Nat` and `Stream` with the `In` constructor, and in `fromStream`, an equal number of layers are peeled away. + +As you might be able to guess, analogously to `Bool` functions representing `Pairs`, this means that `Stream`s are represented by functions from `Nat`. + + +### And Exponents? + +Fixing exponents is a bad idea. For one, we'd need to pick a direction to fix since exponentiation, even on types, is obviously non-commutative. Let's choose to fix the destination, just to match with the left-to-right writing order. + +```{.haskell} +type NoHalt a = Fix ((->) a) +``` + +$$ +\text {NoHalt}(X) := \mathcal Y((-)^X) += \mathcal Y(X \rightarrow) +$$ + +There is no final destination since it gets destroyed by `Fix`. If we regard functions as computations, this is one that never finishes (hence the name `NoHalt`). Haskell always wants functions to have a return type, so this suggests the type is unpopulated like `Void`. + + +Closing +------- + +Function types are one of the reasons Haskell (and functional programming) is so powerful, and fixed-point types allow for recursive data structures. Functions on these structures are recursive, which are dangerous since they can generate paradoxes + +```{.haskell} +void = fix V :: Void -- old +neverend = fix (id :: Void -> Void) -- new +infinity = fix succNat :: Nat +neverend' = fix (id :: Nat -> Nat) +``` + +In practice, were any of these values actually present and strict computation were performed on them, the program would never halt. The [ `absurd` +](https://hackage.haskell.org/package/void-0.6.1/docs/src/Data-Void.html#absurd) function the older `Data.Void` demonstrates this. The [newer version](https://hackage.haskell.org/package/base-4.16.2.0/docs/src/Data.Void.html) merely raises an exception and obviates giving `Void a` constructor altogether (though it still has an `id`). + +Since we are now posed to look at polynomials as types and generate potentially infinite types, the next post will feature a heavy, perhaps surprising focus on algebra. + +Haskell code used in this post can be found [here](). + + +### A Note about Categories + +Category theory is a complex and abstract field (that I myself struggle to apprehend) which is difficult to recommend to total novices. I would, however, like to point out something interesting regarding its definition of product and coproduct (sum). + +![]() + +In these diagrams, following arrows in one way should be equivalent to following arrows in another way. If you recall the exponential laws and rewrite them in their arrowed form, this definition makes a bit more sense. + +$$ +\begin{gather*} +\begin{matrix} +\stackrel{f \vphantom{1 \over 2}}{(X \times Y)^{Z}} \vphantom{} \cong +\vphantom{} \stackrel{f_1 \times f_2 \vphantom{1 \over 2}}{X^Z \times Y^Z} \\[0.5em] +f: Z \rightarrow(X \times Y) \\[0.5em] +f_1: Z \rightarrow X \\[0.5em] +f_2: Z \rightarrow Y \\[0.5em] +\pi_1,\pi_2= \tt fst, snd +\end{matrix} +&& +\begin{matrix} +\stackrel{g_1\times g_2 \vphantom{1 \over 2}}{Z^{X} \times Z^Y} \vphantom{} \cong +\vphantom{} \stackrel{g \vphantom{1 \over 2}}{Z^{X + Y}} \\[0.5em] +g: (X+Y) \rightarrow Z \\[0.5em] +g_1:X \rightarrow Z \\[0.5em] +g_2: Y \rightarrow Z \\[0.5em] +\iota_1,\iota_2 = \tt Left, Right +\end{matrix} +\end{gather*} +$$ + +Category theory is more general, since morphisms (function arrows) need not correspond to objects (types) in the category. The (pseudo-)category in which Haskell types live is "cartesian closed" (products and exponential objects exist), which lets more general categories maintain their flexibility, but which seem like arbitrary distinctions without mentioning counterexamples. + + +### Additional Links + +- [Representable Functors](https://bartoszmilewski.com/2015/07/29/representable-functors/) (from Bartosz Milewski's Categories for Programmers) + + - An interesting note at the end of this article mentions an interesting formal manipulation: a functor $F(X)$ is represented by $\log_X( F(X) )$ diff --git a/posts/type-algebra/3/index.qmd b/posts/type-algebra/3/index.qmd new file mode 100644 index 0000000..25209ef --- /dev/null +++ b/posts/type-algebra/3/index.qmd @@ -0,0 +1,444 @@ +--- +format: + html: + html-math-method: katex +jupyter: python3 +--- + + +Type Algebra and You, Part 3: Combinatorial Types +================================================= + +We know that types have the potential to behave like numbers; the laws for addition, multiplication, and exponentiation are satisfied. However, in the previous post, we also looked at some potentially dangerous inductive, self-referential types where arithmetic tries to include the infinite: `Nat`, the natural numbers; Any, a chain of `Right`s followed by a `Left` wrapped around a value; and `Stream`, an infinite chain of values. This post will focus on better-behaved types which can be made to resemble familiar objects from algebra. + + +Geometric Lists +--------------- + +With `Stream`, there is some difficulty in peeking into the values one contains. We can use its representation from `Nat` to glimpse one value at a time, but we can't group an arbitrary number of them into a collection without it on forever. On the other hand, types like `Any` which include a sum are allowed to terminate. We can combine a sum and a product to create a new object, a `List`. Haskell comes with its own implementation, but re-implementing them is a common exercise. + +```{.haskell} +data List a = Null | Cons a (List a) +``` + +$$ +\begin{matrix} +\scriptsize \text{A list of X is} & +\scriptsize \text{empty} & +\scriptsize \text{or} & +\scriptsize \text{an X} & +\scriptsize \text{and} & +\scriptsize \text{a list of X} & +\\ +L(X) = & 1 & + & X & \times & L(X) +\end{matrix} +\\ \ \\ +\begin{align*} +L(X) &= 1 + X \cdot L(X) \\ +L(X) - X \cdot L(X) &= 1 \\ +L(X) \cdot (1 - X) &= 1 \\ +L(X) &= {1 \over 1 - X} \\ +\end{align*} +$$ + +Unlike with the infinite types where 0 = 1, nothing goes wrong arithmetically. However, the resulting expression doesn't seem to make sense from the perspective of types. There are no analogues to subtraction or division in type theory. Fortunately, all we need is a trick from calculus, the Taylor series. + +$$ +\begin{matrix} +\scriptsize \text{A list of X is} & +\scriptsize \text{empty} & +\scriptsize \text{or} & +\scriptsize \text{a value of X} & +\scriptsize \text{or} & +\scriptsize \text{two values of X} & +\scriptsize \text{or} & +\scriptsize \text{three values of X} & +\scriptsize \text{or} & +\\ +L(X) = {1 \over 1 - X} = & 1 & + & X & + & X^2 & + & X^3 & + & ... +\end{matrix} +$$ + +This is the [geometric series](https://en.wikipedia.org/wiki/Geometric_series), which appears throughout algebra and analysis. Interestingly, since `Stream` is more primitive than `List`, this series includes its supremum, $X^\omega$. + +Something to note about the series is that there is an inherent order to the terms. The 1 term is defined first, then *X*, then all subsequent ones recursively. This detail also means that the $X^2$ term is more "ordered" than a typical pair like $X \times X$. + + +### Another Interpretation + +We can equally as well define `List` in terms of `Fix` and arithmetic. Instead, the definition is + +```{.haskell} +data ListU a b = L (Maybe (a,b)) +type List' a = Fix (ListU a) +``` + +$$ +\hat L(X,Z) = 1 + XZ \\ +L(X) = \mathcal Y(\hat L (X,-)) +$$ + +The expression $1 + XZ$ certainly looks like $1 - X$, if we let *Z* = -1. However, we again run into the problem that -1 doesn't seem to correspond to a type. Worse than that, the actual type we are after is $(1 - X)^{-1} = -1 \rightarrow 1 - X$. + +The latter type seems to resemble a function with -1 on both sides of the arrow. Since the resulting type is intended to resemble a fixed point, we could regard -1 as a sort of "initial type" that gets the list started. Then, we can use the initial definition to replace the occurrence of -1 on the LHS with the entire LHS. + +$$ +(1 - X)^{-1} = -1 ~\rightarrow~ 1 - X \\ \\ +\begin{matrix} +-1 +& \rightarrow& +1 - X +\\&& +1 + (-1) \times X +& \rightarrow & +1 +(1 - X)X +\\ & & & & +1 + X + (- 1) \times X^2 +& \rightarrow & +1 + X + (1-X)X^2 +\\ &&&&&& ... +\end{matrix} +$$ + +This interprets the series as a [rewrite rule](https://en.wikipedia.org/wiki/Rewriting#Arithmetic). Each step is shown before distributing and applying the rule once more. In the limit, when there are no more negative signs to rewrite, we recover the original series. + + +### Convergence + +Just like in math, things go wrong when this expression is applied naively. For example, "a list of bools" would seem to have the type + +$$ +{\texttt{List Bool}} = L(2) \stackrel{?}{=} {1 \over 1 - 2} = -1 +$$ + +If this were true it would mean + +- `Either () (List Bool)` is isomorphic to Void, since $1 + (-1) = 0$ +- A list of an object *X* is isomorphic to a function from a list of bools to either a unit or a tuple containing a list of bools and a value of *X* + - `List a ≅ List Bool -> Either () (List Bool, a)` + +The first statement is obviously false, since the values `Left ()` and `Right []` will always exist. The second statement is dubious. For it to be true, we must imagine values of *X* can be extracted out of some (possibly infinite) sequence of booleans (the *X* in the tuple), leaving behind enough information to convert the rest of the list (the `List Bool` in the tuple), or be exhausted. + +The latter argument requires far too much information to be generally true, so I am satisfied with my previous description of -1. It should only show up in the context of a fixed point expression, and is only a valid type in a denominator (the return value of a function from -1). + + +### Iteration + +Consider also a list of lists of any type *X*. Then by iterating lists, it would appear that + +$$ +\texttt{List (List a)} = L(L(X)) \stackrel{?}{=} +{1 \over 1 - {1 \over 1 - X}} = {1 - X \over 1-X-1} = {X - 1 \over X} +$$ + +If a were `Void`, then the only possible `List` to construct is an empty list ($L(0) = {1 \over 1 - 0} = 1$). Wrapped in another list, the only possible values are those made by repeating this any (natural) number of times. This means that it is itself isomorphic to `Nat`, and we can write a bijection. + +```{.haskell} +toLists :: Nat -> List (List Void) +toLists Zero = Null +toLists (Succ x) = Cons Null (toLists x) +-- toLists x = replicate x Null + +fromLists :: List (List Void) -> Nat +fromLists Null = Zero +fromLists (Cons x xs) = Succ (fromLists xs) +-- fromLists = toNat . length + +-- fromLists . toLists = id :: Nat -> Nat +-- toLists . fromLists = id :: (List (List Void)) -> (List (List Void)) +``` + +Arithmetically, shows that $\omega = 1 + 1 + 1^2 + ... = {1 \over 1 - 1}$. More directly, the expression has no Taylor series at 0, and the infinitude of possible values spoils attempting to understand higher order terms. This has big implications, since if we wrap this in another layer of lists, + +$$ +\texttt{List (List (List a))} = L(L(L(X))) \stackrel{?}{=} +{1 \over 1 - {1 \over 1 - {1 \over 1 - X}}} = ... = X +$$ + +we get back to where we started, which is perfectly absurd. The left-hand side can contain far more $X$s than the right-hand side. In other words, by going "past infinity" we have ruined the correspondence between the functor and a series. + + +A Walk through the Woods +------------------------ + +All types thus far have been of a linear form: a `List` is analogous to a line segment and a `Stream` is analogous to a ray. All we need to do to go from lists to binary trees is to, for every node, include two sub-structures rather than one. + +```{.haskell} +data Tree2 a = Leaf | Branch a (Tree2 a) (Tree2 a) +``` + +$$ +\begin{matrix} +\scriptsize \text{A 2-tree of X is} \\ +T_2(X) = & 1 & +\scriptsize \text{a leaf} \\ +& + & \scriptsize \text{or} \\ +& X \times \phantom{1} & +\scriptsize \text{a value of X and} \\ +& T_2(X) \times \phantom{1} & +\scriptsize \text{a left subtree of X and} \\ +& T_2(X) \phantom{\times 1} & +\scriptsize \text{a right subtree of X} & +\end{matrix} \\ ~ \\ +\begin{align*} +0 &= 1 - T_2(X) + X \times T_2(X)^2 +\end{align*} +$$ + +Simple enough, but now we have an equation which is quadratic in our functor $T_2(X)$. At this point, we can try to invoke the quadratic formula. Luckily, one of the solutions has a Taylor series which consists of only positive integers, just like the geometric series. + +$$ +a = X, b = -1, c = 1 +\\ \ \\ +T_2(X) = {1 - \sqrt{1 - 4X} \over 2X} = 1 + X + 2X^2 + 5X^3 + 14X^4 + 42X^5 + ... +$$ + +The coefficients 1, 1, 2, 5, 14, 42, ... are known as the Catalan numbers ([OEIS A000108](http://oeis.org/A000108)). The OEIS article also pleasantly informs that these count a kind of binary tree on a given number of nodes -- the kind which distinguishes between left and right, as defined by the type. + +::: {} +![]() +Rooted binary trees on a particular number of nodes. +::: + +These coefficients have a direct interpretation. If we have three nodes, then there are three locations to place a value of *X*. In other words, the tree holds an $X^3$. The coefficient of this term tells us that a value from the type 5 tells us the shape of the nodes on the tree. + +Contrast this with the coefficients in the geometric series. They are all 1, telling us that there is only a single shape for a list of a particular size. As consequence, trees are in some sense "larger" than lists. For example, a [breadth-first search](https://en.wikipedia.org/wiki/Breadth-first_search) on a binary tree can collect all values at the nodes into a list. But multiple trees can return the same list, so this is clearly not a bijection. Algebraically, this is because the two series have different coefficients from one another. + + +### Actually Solving the Polynomial + +We invoked the quadratic formula to solve the polynomial $1 - T_2(X) + X \times T_2(X)^2$, but we haven't justified the ability to use it. Not only are square roots more suspect than division and subtraction, but the quadratic formula has a choice in sign. Combinatorially, an initial condition determines plus or minus, and the square root is interpreted as a [binomial expansion](https://en.wikipedia.org/wiki/Binomial_theorem#Newton's_generalized_binomial_theorem), since $\sqrt{1 - X} = (1 - X)^{1/2}$. + +Naively, the solution seems to have the following interpretation as a type: + +$$ +{1 - \sqrt{1 - 4X} \over 2X} = (1 - (1 - 4X)^{1/2}) \times (2X)^{-1} += \textcolor{red}{ (1 - ({\scriptsize 1 \over 2} \rightarrow 1-4X)) \times (-1 \rightarrow 2X) } +$$ + +Compared to the geometric series, this doesn't make sense. -1 appears in the first term of the product, yet originates from the second term. It doesn't seem like the iteration can "get started" like it could previously. We can do some algebra to get terms into the denominator. + +$$ +\begin{gather*} +{1 - \sqrt{1 - 4X} \over 2X} += {2 \over 1 + \sqrt{1 - 4X}} += \textcolor{red}{ 2 \times (-1 \rightarrow1 + ({\scriptsize 1 \over 2} \rightarrow 1 - 4X) ) } \\ + {1 \over {1 \over 2}(1 + \sqrt{1 - 4X})} += \textcolor{red}{-1 \rightarrow {\scriptsize 1 \over 2} \times (1 + ({\scriptsize 1 \over 2} \rightarrow 1 - 4X) ) } \\ +\end{gather*} +$$ + +The first expression keeps a term in the numerator. Without it, the expression would generate half-integer terms which do not make sense as finite types. To combat this, the second places its reciprocal in the denominator alongside the square root, which appears to describe a second rewrite rule. While it looks slightly better, I am still unsure whether this result is interpretable. I am also unsure whether it is significant that 1/2 can be expressed as $2^{-1} = (-1 \rightarrow 2)$. My best guess is that some kind of mutual recursion or alternating scheme is necessary. + + +### Another Solution? + +There might still be some hope. The earlier OEIS page mentions that the map which generates the Mandelbrot set has, in the limit, a Taylor series with the Catalan numbers as coefficients. + +$$ +z_{n+1} = z_n^2 + c \\ +z \mapsto z^2 + c \\ \ \\ +\begin{matrix} +c +& \rightarrow& +c^2 + c +& \rightarrow & +(c^2 + c)^2 + c +\\ & & & & +c^4 + 2c^3 + c^2 + c +& \rightarrow & +(c^4 + 2c^3 + c^2 + c)^2 + c +\\ &&&&&& +c^8 + 4c^7 + 6c^6 + 6c^5 + 5c^4 + 2c^3 + c^2 + c +\\ &&&&&& ... +\end{matrix} +$$ + +The Mandelbrot map is more similar to a type in which leaves, rather than nodes, contain values. We could convert the expression to suit the trees we've been working with and to correspond better with the definition of the list. + +$$ +z \mapsto 1 + cz^2 \\ +i \rightarrow 1-X = (1 - X)^i +\\ \ \\ +\begin{gather*} +i ~\rightarrow~ 1 - X ~\rightarrow~ 1 + (X - 2X^2 + X^3) ~\rightarrow~ \\ +\hline +\vphantom{x^{x^{x^x}}} +1 + X + (2X^2 - 3X^3 + 2X^4) &\rightarrow& ... & \textcolor{red}{\times} \\ +1 + X + 2X^2 + 5X^3 - 6X^4 -4X^5 + 12X^6 -8X^7 + 2X^8 & +\rightarrow & ... & \textcolor{red}{\times} +\end{gather*} +$$ + +This interpretation is worse, though. In the case of lists, either the initial expression ($1 - X$) or the most recent expression could replace any occurrence of -1. Here, neither work, though one appears to do so initially. Finally, the resulting expression is not the Taylor series of $(1-X)^i$. + + +Other Trees +----------- + +The OEIS article for the Catalan numbers also mentions that the sequence counts "ordered rooted trees with *n* nodes, not including the root". In this kind of tree, a node has any number of children rather than just two. + +We can construct this type of tree by as the product of a value at the node and the node's children (possibly none, but themselves trees), called the *subforest*. A *forest* is just a list of trees. This defines trees and forests in a mutually recursive way that easily lends itself to algebraic manipulation. Haskell's `Data.Graph` agrees with the following definition + +```{.haskell} +data Tree a = Node a (List (Tree a)) +type Forest a = List (Tree a) +``` + +$$ +\begin{matrix} +\scriptsize \text{A tree of $X$ is} & +\scriptsize \text{a value of $X$} & +\scriptsize \text{and} & +\scriptsize \text{a forest of $X$} \\ +T(X) = & +X & +\times & F(X) +\end{matrix} \\ +\begin{matrix} +\scriptsize \text{A forest of $X$} & +\scriptsize \text{is} & +\scriptsize \text{a list of trees of $X$} +\\ +F(X) +& = & +L(T(X)) +\\ & = & +{1 \over 1-T(X)} +\\ & = & +{1 \over 1-X \times F(X)} +\end{matrix} +\\ \ \\ +\begin{align*} +(1 - X \times F(X)) \times F(X) = 1 \\ +-1 + F(X) - X \times F(X)^2 = 0 \\ +1 - F(X) + X \times F(X)^2 = 0 \\ +\end{align*} +$$ + +The resulting equation for *F*(*X*) is the same as the one featured earlier for binary trees, so we know that it generates the same series. + +$$ +F(X) = T_2(X) = {1 - \sqrt{1 - 4X} \over 2X} = 1 + X + 2X^2 + 5X^3 + 14X^4 + 42X^5 + ... +$$ + + +### Binary Bijections + +Two finite types were isomorphic when their algebraic equivalents were equal (e.g., `Bool ≅ Maybe ()` because 2 = 1 + 1). Since these structures have the same expression in *X*, we might assume that the functors are isomorphic with respect to the type *X* they contain. + +For this to actually be the case, there should be a bijection between the two functors, else "isomorphic" ceases to be the proper word. With a bit of clever thinking, we can consider the left (or right) children in a binary tree as siblings, and construct functions that reframe the nodes accordingly. + +::: {} +![]() +An example of the correspondence between binary trees and "bushes", or general trees. A root is shown for the latter to make it better resemble a tree. Leaves and empty subforests not shown. +::: + +```{.haskell} +treeToForest :: Tree2 a -> Forest a +treeToForest Leaf = Null +treeToForest (Branch x l r) = Cons (Node x (treeToForest r)) (treeToForest l) + +forestToTree :: Forest a -> Tree2 a +forestToTree Null = Leaf +forestToTree (Cons (Node x fs) ns) = Branch x (forestToTree ns) (forestToTree fs) + +-- forestToTree . treeToForest = id :: Tree2 a -> Tree2 a +-- treeToForest . forestToTree = id :: Forest a -> Forest a +``` + +A weaker equality applies in combinatorics: two generating functions are equal if their coefficients are equal. If a closed algebraic expression is known, then it is sufficient to compare them. Instead, we have "generating functors", which satisfy the same algebraic equation, have the same coefficients as a series, and most strongly, are isomorphic in the sense that they have a bijection. + + +### Ternary and Larger-order Trees + +Even though the general tree structure used above seems to encompass ternary trees, *strictly* ternary trees have a bit more freedom. In a general tree, a subtree can only appear further along a list of children if all prior elements of the list are filled. On the other hand, in ternary trees, subtrees can occupy any of the three possible positions. + +If the binary trees functor satisfy a quadratic, then it stands to reason that ternary trees should satisfy a cubic. And they do: + +```{.haskell} +data Tree3 a = Leaf | Node a (Tree3 a) (Tree3 a) (Tree3 a) +``` + +$$ +\begin{matrix} +\scriptsize \text{A 3-tree of X is} \\ +T_3(X) = & 1 & +\scriptsize \text{a leaf} \\ +& + & \scriptsize \text{or} \\ +& X \times \phantom{1} & +\scriptsize \text{a value of X and} \\ +& T_3(X) \times \phantom{1} & +\scriptsize \text{a left subtree of X and} \\ +& T_3(X) \times \phantom{1} & +\scriptsize \text{a center subtree of X} & \\ +& T_3(X) \phantom{\times 1} & +\scriptsize \text{a right subtree of X} & +\end{matrix} \\ ~ \\ +\begin{align*} +0 &= 1 - T_3(X) + X \times T_3(X)^3 +\end{align*} +$$ + +We can solve a cubic with the [cubic formula](https://en.wikipedia.org/wiki/Cubic_equation#Cardano's_formula), but it yields a result which is less comprehensible than the one for binary trees. + +$$ +T_3^3 +pT_3 + q = 0 \\ p = -1/X, q =1/X +\\ \ \\ +\begin{align*} +T_3(X) &= \sqrt[3]{- {1 \over 2X} + \sqrt{{1 \over 4X^2} - {1\over 27X^3}}} + \sqrt[3]{- {1 \over 2X} - \sqrt{{1 \over 4X^2} - {1\over 27X^3}}} \\ +&= {1 \over X}\left( \sqrt[3]{- {X^2 \over 2} + \sqrt{{X^4 \over 4} - {X^3 \over 27}}} + \sqrt[3]{- {X^2 \over 2} - \sqrt{{X^4 \over 4} - {X^3\over 27}}} \right) \\ +\end{align*} +\\ \ \\ += 1 + X + 3X^2 + 12X^3 + 55X^4 + 273X^5 +... +$$ + +The coefficients here are enumerated by [OEIS A001764](http://oeis.org/A001764), which doesn't have a name. Cube roots now feature prominently in the generating functor. This expression is much too large for me to even attempt rewriting in "functional" form. WolframAlpha refuses to calculate the series from this expression within standard computation time. Sympy gives an almost-correct series, but which has unsimplified roots of *i* and has half-integer powers of *X*. + +A series better-suited to computation, based on angle trisection, is adapted from the OEIS here: + +$$ +T_3(X^2) = {2 \over X \sqrt{3}} \cdot +\sin \left( {1\over 3}\arcsin \left(3\cdot{X\sqrt {3} \over 2} \right) \right) +$$ + +This expression invokes not only irrationals, but trigonometric functions, which are even harder, if not impossible to understand as types. The situation gets even worse for higher-order trees, where [no algebraic formula for the solutions exists](https://en.wikipedia.org/wiki/Abel%E2%80%93Ruffini_theorem). Without being sure how to interpret the simplest case with only square roots, I am unsure whether this has implications for rewrite rules. + + +Closing +------- + +This hardly scratches the surface of constructible datatypes. As a final example, a list which could include pairs as well as singletons of X is counted by the Fibonacci numbers: + +```{.haskell} +data FibList a = NullF | Single a (List a) | Double (a,a) (List a) +``` + +$$ +\begin{matrix} +F(X) = 1 + X \times F(X) + X^2 \times F(X) +\end{matrix} +\\ \ \\ +\begin{align*} +1 &= F(X) - X \cdot F(X) - X^2 \cdot F(X) \\ +1 &= F(X) \cdot(1 - X - X^2) \\ +F(X) &= {1 \over 1 - X - X^2} \\ +&=1 + X + 2X^2+3X^3 +5X^4 +... +\end{align*} +$$ + +However, I do not feel that it is useful to continue plumbing for types to express as a series. At this basic level, there are still mysteries I am not equipped to solve. + +I am the most interested in generalizing rewrite rule-style types. The presence of the square root seems almost opaque. Even the similar Mandelbrot set rule doesn't cooperate with the "recursive" interpretation of -1. This rule is given in terms of the variable *z*, but my goal is to is to give an intermediate meaning to -1, not to introduce intermediate "dummy" variables. + +I am also interested in extending these ideas to bifunctors (polynomials in multiple variables) and bi-fixes (fixing multiple terms at once, which admittedly the binary tree does already). Perhaps I may explore these ideas in the future. + +Haskell code used in this post can be found [here](). Tree diagrams made with GeoGebra. + + +### Links + +- [Haskell/Zippers](https://en.wikibooks.org/wiki/Haskell/Zippers) (from Wikibooks) + - Another formal manipulation: using the derivative operator on algebraic datatypes. Since the Taylor series is defined in terms of derivatives, there may be a completely type-theoretical characterization that doesn't rely on "borrowing ideas" from calculus. +- [Generating functions for generating trees](https://www.sciencedirect.com/science/article/pii/S0012365X01002503?via%3Dihub) (paper from ScienceDirect) + - This paper references enumerates structures by rewrite rules. It also presents a zoo of combinatorial objects and their associated generating functions.