cube/zenzicubi.co
cube/zenzicubi.co
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

ensure consistent function order in type-algebra.*

Browse Source
This commit is contained in:
queue-miscreant 2025-08-07 22:33:15 -05:00
parent 71b4f64594
commit 64d2b07865
3 changed files with 46 additions and 38 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

47
posts/type-algebra/1/index.qmd
View File

@ -194,18 +194,18 @@ Constructing a `Just Void` would require that we already had a Void value, which
Therefore, `Nothing` is the only possible value of `Maybe Void`. Therefore, `Nothing` is the only possible value of `Maybe Void`.
```{haskell} ```{haskell}
toUnit :: Maybe Void -> () toUnitM :: Maybe Void -> ()
toUnit Nothing = () toUnitM Nothing = ()
fromUnit :: () -> Maybe Void fromUnitM :: () -> Maybe Void
fromUnit () = Nothing fromUnitM () = Nothing
instance Isomorphism (Maybe Void) () where instance Isomorphism (Maybe Void) () where
toA = fromUnit toA = fromUnitM
toB = toUnit toB = toUnitM
identityA = fromUnit . toUnit identityA = fromUnitM . toUnitM
identityB = toUnit . fromUnit identityB = toUnitM . fromUnitM
``` ```
@ -263,22 +263,22 @@ Using addition, we can actually reconstruct the successor from **1**:
--| code-fold: true --| code-fold: true
--| code-summary: Isomorphism instance for `Maybe a` and `((), a)` --| code-summary: Isomorphism instance for `Maybe a` and `((), a)`
type MaybeEither a = Either () a type MaybeE a = Either () a
toMaybeEither :: Maybe a -> MaybeEither a toMaybeE :: Maybe a -> MaybeE a
toMaybeEither Nothing = Left () toMaybeE Nothing = Left ()
toMaybeEither (Just x) = Right x toMaybeE (Just x) = Right x
fromMaybeEither :: MaybeEither a -> Maybe a fromMaybeE :: MaybeE a -> Maybe a
fromMaybeEither (Left ()) = Nothing fromMaybeE (Left ()) = Nothing
fromMaybeEither (Right x) = Just x fromMaybeE (Right x) = Just x
instance Isomorphism (Maybe a) (MaybeEither a) where instance Isomorphism (Maybe a) (MaybeE a) where
toA = fromMaybeEither toA = fromMaybeE
toB = toMaybeEither toB = toMaybeE
identityA = fromMaybeEither . toMaybeEither identityA = fromMaybeE . toMaybeE
identityB = toMaybeEither . fromMaybeEither identityB = toMaybeE . fromMaybeE
``` ```
`Left ()` now takes on the role of `Nothing`, while all the `Right`s come from the type parameter `a`. `Left ()` now takes on the role of `Nothing`, while all the `Right`s come from the type parameter `a`.
@ -421,7 +421,9 @@ instance Isomorphism (a, b, c) ((a,b), c) where
identityB = toLeftProd . fromLeftProd identityB = toLeftProd . fromLeftProd
``` ```
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. There's still a bit of work to prove associativity *in general* from these local rules.
But that's fine, since we're still primarily concerned with the equivalent functors
`Either` and `(,)` (which are local anyway).
### Other Arithmetic Properties ### Other Arithmetic Properties
@ -549,7 +551,8 @@ data PostDist a b c d = F a c | O a d | I b c | L b d
$$ $$
\begin{matrix} \begin{matrix}
\scriptsize \text{Either $X$ $Y$ and Either $Z$ $W$} & \scriptsize \text{is equivalent to} \\ \scriptsize \text{Either $X$ $Y$ and Either $Z$ $W$} & \scriptsize \text{is equivalent to}
\\
(X + Y) \cdot (Z + W) \cong (X + Y) \cdot (Z + W) \cong
\\ \\
\phantom{+} X \cdot Z \phantom{+} X \cdot Z

25
posts/type-algebra/2/index.qmd
View File

@ -78,14 +78,14 @@ 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. then we can just send the same value to both and put it in a pair.
```{haskell} ```{haskell}
distExp :: (a -> (b, c)) -> (a -> b, a -> c)
distExp f = (fst . f, snd . f)
-- distExp f = (\x -> fst (f x), \x -> snd (f x))
undistExp :: (a -> b, a -> c) -> (a -> (b, c)) undistExp :: (a -> b, a -> c) -> (a -> (b, c))
undistExp (g, h) x = (g x, h x) undistExp (g, h) x = (g x, h x)
-- undistExp (g, h) = \x -> (g x, h x) -- undistExp (g, h) = \x -> (g x, h x)
distExp :: (a -> (b, c)) -> (a -> b, a -> c)
distExp f = (fst . f, snd . f)
-- distExp f = (\x -> fst (f x), \x -> snd (f x))
instance Isomorphism (Exponent a b, Exponent a c) (Exponent a (b, c)) where instance Isomorphism (Exponent a b, Exponent a c) (Exponent a (b, c)) where
toA = distExp toA = distExp
toB = undistExp toB = undistExp
@ -150,12 +150,14 @@ instance Isomorphism (Exponent a c, Exponent b c) (Exponent (Either a b) c) wher
This identity actually tells us something very important regarding the definition 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) of functions on sum types: they must have as many definitions (i.e., a *product* of definitions)
as there are types in the sum. 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`. 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 ### 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. Finally (arguably as consequence of the first law), if we raise a term with an exponent
to another exponent, the exponents should multiply.
$$ $$
\stackrel{ \stackrel{
@ -230,7 +232,8 @@ to2Coeff (Left x) = (False, x)
to2Coeff (Right x) = (True, x) to2Coeff (Right x) = (True, x)
from2Coeff :: (Bool, a) -> LeftRight a from2Coeff :: (Bool, a) -> LeftRight a
from2Coeff = undefined from2Coeff (False, x) = Left x
from2Coeff (True, x) = Right x
instance Isomorphism (LeftRight a) (Bool, a) where instance Isomorphism (LeftRight a) (Bool, a) where
toA = from2Coeff toA = from2Coeff
@ -437,13 +440,14 @@ At best, they afford us a way to bootstrap a way to display numbers that isn't i
Functors from Bifunctors Functors from Bifunctors
------------------------ ------------------------
If their first argument of a bifunctor is fixed, then what remains is a functor. If the first argument of a bifunctor is fixed, then what remains is a functor.
For example, with `Either`:
```haskell ```haskell
forall a. Either a :: * -> * forall a. Either a :: * -> *
``` ```
But since this is a functor, we can apply `Fix` to it. Since this type is functor-like, we can apply `Fix` to it.
```{haskell} ```{haskell}
type Any a = Fix (Either a) type Any a = Fix (Either a)
@ -608,7 +612,8 @@ I would, however, like to point out something interesting regarding its definiti
![](./prod_coprod.png) ![](./prod_coprod.png)
In these diagrams, following arrows in one way should be equivalent to following arrows in another way. 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. If you recall the exponential laws and rewrite them in their arrowed form,
this definition makes a bit more sense.
$$ $$
\begin{gather*} \begin{gather*}

10
posts/type-algebra/3/index.qmd
View File

@ -225,12 +225,12 @@ fromLists Null = Zero
fromLists (Cons x xs) = Succ (fromLists xs) fromLists (Cons x xs) = Succ (fromLists xs)
-- fromLists = toNat . length -- fromLists = toNat . length
instance Isomorphism (List (List Void)) Nat where instance Isomorphism Nat (List (List Void)) where
toA = toLists toA = fromLists
toB = fromLists toB = toLists
identityA = toLists . fromLists identityA = fromLists . toLists
identityB = fromLists . toLists identityB = toLists . fromLists
``` ```
Arithmetically, this implies $\omega = 1 + 1 + 1^2 + ... = {1 \over 1 - 1}$. Arithmetically, this implies $\omega = 1 + 1 + 1^2 + ... = {1 \over 1 - 1}$.