Update "catemorphisms" article to new math delimiters
Signedoffby: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
3eddac0a89
commit
7f4d0df366

@ 64,7 +64,7 @@ If we kept going with this process infinitely, we'd eventually have what we need


{{< /latex >}}




But hey, the stuff inside the first set of parentheses is still an infinite sequence of applications


of the function \\(\\text{lengthF}\\), and we have just defined this to be \\(\\text{length}\\). Thus,


of the function \(\text{lengthF}\), and we have just defined this to be \(\text{length}\). Thus,


we can rewrite the above equation as:




{{< latex >}}



@ 77,7 +77,7 @@ such a fixed point. It's defined like this:




{{< codelines "Haskell" "catamorphisms/Cata.hs" 16 16 >}}




This definition is as declarative as can be; `fix` returns the \\(x\\) such that \\(x = f(x)\\). With


This definition is as declarative as can be; `fix` returns the \(x\) such that \(x = f(x)\). With


this, we finally write:




{{< codelines "Haskell" "catamorphisms/Cata.hs" 18 18 >}}



@ 95,7 +95,7 @@ This is a valid criticism, so I'd like to briefly talk about how `fix` is used i


lambda calculus.




In the untyped typed lambda calculus, we can just define a term that behaves like `fix` does. The


most common definition is the \\(Y\\) combinator, defined as follows:


most common definition is the \(Y\) combinator, defined as follows:




{{< latex >}}


Y = \lambda f. (\lambda x. f (x x)) (\lambda x. f (x x ))



@ 107,7 +107,7 @@ When applied to a function, this combinator goes through the following evaluatio


Y f = f (Y f) = f (f (Y f)) =\ ...


{{< /latex >}}




This is the exact sort of infinite series of function applications that we saw above with \\(\\text{lengthF}\\).


This is the exact sort of infinite series of function applications that we saw above with \(\text{lengthF}\).




### Recursive Data Types


We have now seen how we can rewrite a recursive function as a fixed point of some nonrecursive function.



@ 152,7 +152,7 @@ Looking past the constructors and accessors, we might write the above in pseudo


newtype Fix f = f (Fix f)


```




This is just like the lambda calculus \\(Y\\) combinator above! Unfortunately, we _do_ have to


This is just like the lambda calculus \(Y\) combinator above! Unfortunately, we _do_ have to


deal with the cruft induced by the constructors here. Thus, to write down the list `[1,2,3]`


using `MyListF`, we'd have to produce the following:





@ 163,7 +163,7 @@ This is actually done in practice when using some approaches to help address the


it's quite unpleasant to write code in this way, so we'll set it aside.




Let's go back to our infinite chain of type applications. We've a similar pattern before,


with \\(\\text{length}\\) and \\(\\text{lengthF}\\). Just like we did then, it seems like


with \(\text{length}\) and \(\text{lengthF}\). Just like we did then, it seems like


we might be able to write something like the following:




{{< latex >}}



@ 193,8 +193,8 @@ The two mutual inverses \(f\) and \(g\) fall out of the definition of the <code>


data type! If we didn't have to deal with the constructor cruft, this would be more


ergonomic than writing our own <code>myIn</code> and <code>myOut</code> functions.


{{< /sidenote >}}


that take you from one type to the other (and vice versa), such that applying \\(f\\) after \\(g\\),


or \\(g\\) after \\(f\\), gets you right back where you started. That is, \\(f\\) and \\(g\\)


that take you from one type to the other (and vice versa), such that applying \(f\) after \(g\),


or \(g\) after \(f\), gets you right back where you started. That is, \(f\) and \(g\)


need to be each other's inverses. For our specific case, let's call the two functions `myOut`


and `myIn` (I'm matching the naming in [this paper](https://maartenfokkinga.github.io/utwente/mmf91m.pdf)). They are not hard to define:






Loading…
Reference in New Issue
Block a user