Guest User

Untitled

a guest
Nov 14th, 2018
102
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 2.06 KB | None | 0 0
  1. # fixed-point operators
  2.  
  3. 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:
  4.  
  5. ```haskell
  6. newtype Fix f = Fix { unfix :: f (Fix f) }
  7. ```
  8.  
  9. There are some problems with this, however:
  10. 1. most languages provide _general_ recursion (and, in fact, this definition requires it), so such a definition can’t be total; and
  11. 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.
  12.  
  13. There are (at least) a pair of other operators that give more principled and consistent semantics.
  14.  
  15. ```haskell
  16. data Mu f = Mu (forall a. (f a -> a) -> a)
  17.  
  18. data Nu f where
  19. Nu :: (a -> f a) -> a -> Nu f
  20. ```
  21.  
  22. `Mu` defines a recursive structure as a fold, and it’s apparent from the definitions of `cata` and`embed`:
  23.  
  24. ```haskell
  25. cata :: (f a -> a) -> Mu f -> a
  26. cata φ (Mu f) = f φ
  27.  
  28. embed :: f (Mu f) -> Mu f
  29. embed fm = Mu (\f -> f (fmap (cata f) fm))
  30. ```
  31.  
  32. `cata` simply applies the fold in `Mu` to the provided algebra, and `embed` adds another step to the fold in `Mu`.
  33.  
  34. This provides a structure that is always strict and finite – the “least” fixed-point.
  35.  
  36. `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.
  37.  
  38. 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