Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- # fixed-point operators
- In general, finds the “fixed point” of some endofunctor, which means some type `t`, such that `f t ~ t`. The simplest operator is often called `Fix`, and takes advantage of a language’s primitive recursion to provide a very straightforward definition:
- ```haskell
- newtype Fix f = Fix { unfix :: f (Fix f) }
- ```
- There are some problems with this, however:
- 1. most languages provide _general_ recursion (and, in fact, this definition requires it), so such a definition can’t be total; and
- 2. this definition can have different semantics in different languages – e.g., in Scala, it would be strict (and therefore finite), while in Haskell the recursion would be lazy, and thus potentially infinite.
- There are (at least) a pair of other operators that give more principled and consistent semantics.
- ```haskell
- data Mu f = Mu (forall a. (f a -> a) -> a)
- data Nu f where
- Nu :: (a -> f a) -> a -> Nu f
- ```
- `Mu` defines a recursive structure as a fold, and it’s apparent from the definitions of `cata` and`embed`:
- ```haskell
- cata :: (f a -> a) -> Mu f -> a
- cata φ (Mu f) = f φ
- embed :: f (Mu f) -> Mu f
- embed fm = Mu (\f -> f (fmap (cata f) fm))
- ```
- `cata` simply applies the fold in `Mu` to the provided algebra, and `embed` adds another step to the fold in `Mu`.
- This provides a structure that is always strict and finite – the “least” fixed-point.
- `Nu`, on the other hand, is for defining the “greatest” fixed-point, which includes potentially-infinite values in addition to the finite values covered by `Mu`. It subsumes all of `Mu`’s values (hence the terms “greatest” and “least”), and it’s trivial to define `Mu f -> Nu f` … but that discards the proof that the value is finite, and so folding it can no longer be guaranteed to terminate.
- Looking at `Nu`’s structure, you can see it holds both a coalgebra (`a -> f a`) to unfold a single step, and a seed value to be passed to that algebra. It’s the delayed application of the seed to the algebra that makes `Nu` lazy, and therefore capable of representing infinite values.
Add Comment
Please, Sign In to add comment