add type.1 from wordpress
This commit is contained in:
parent
dcba3a400c
commit
0c37410a7c
477
type_alg/1/index.qmd
Normal file
477
type_alg/1/index.qmd
Normal file
@ -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) <br>
|
||||
[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)
|
||||
Loading…
x
Reference in New Issue
Block a user