fix -package:Agda

fix f is the least fixed point of the function f, i.e. the least defined x such that f x = x. When f is strict, this means that because, by the definition of strictness, f ⊥ = ⊥ and such the least defined fixed point of any strict function is ⊥.

Examples

We can write the factorial function using direct recursion as

>>> let fac n = if n <= 1 then 1 else n * fac (n-1) in fac 5
120

This uses the fact that Haskell’s let introduces recursive bindings. We can rewrite this definition using fix, Instead of making a recursive call, we introduce a dummy parameter rec; when used within fix, this parameter then refers to fix’s argument, hence the recursion is reintroduced.

>>> fix (\rec n -> if n <= 1 then 1 else n * rec (n-1)) 5
120

Using fix, we can implement versions of repeat as fix . (:) and cycle as fix . (++)

>>> take 10 $ fix (0:)
[0,0,0,0,0,0,0,0,0,0]

>>> map (fix (\rec n -> if n < 2 then n else rec (n - 1) + rec (n - 2))) [1..10]
[1,1,2,3,5,8,13,21,34,55]

Implementation Details

The current implementation of fix uses structural sharing

fix f = let x = f x in x

A more straightforward but non-sharing version would look like

fix f = f (fix f)

fix f is the least fixed point of the function f, i.e. the least defined x such that f x = x. For example, we can write the factorial function using direct recursion as

>>> let fac n = if n <= 1 then 1 else n * fac (n-1) in fac 5
120

This uses the fact that Haskell’s let introduces recursive bindings. We can rewrite this definition using fix,

>>> fix (\rec n -> if n <= 1 then 1 else n * rec (n-1)) 5
120

Instead of making a recursive call, we introduce a dummy parameter rec; when used within fix, this parameter then refers to fix’s argument, hence the recursion is reintroduced.

The fix function applies another function to matching events in a pattern of controls. fix is contrast where the false-branching function is set to the identity id. It is like contrast, but one function is given and applied to events with matching controls. For example, the following only adds the crush control when the n control is set to either 1 or 4:

d1 $ slow 2
$ fix (# crush 3) (n "[1,4]")
$ n "0 1 2 3 4 5 6"
# sound "arpy"

You can be quite specific; for example, the following applies the function hurry 2 to sample 1 of the drum sample set, and leaves the rest as they are:

fix (hurry 2) (s "drum" # n "1")

In fix $ go a -> do ...; go xy any action after a go is ignored.

If you turn OverloadedStrings extension on, GHC can't deduce the type of string literal. This function fix the type to Builder Builder without type annotation.

Monadic fixpoints. For a detailed discussion, see Levent Erkok's thesis, Value Recursion in Monadic Computations, Oregon Graduate Institute, 2002.

Greatest fixpoint of a Bifunctor (a Functor over the first argument with zipping).

Fixed points of a functor. Type f should be a Functor if you want to use simple recursion schemes or Traversable if you want to use monadic recursion schemes. This style allows you to express recursive functions in non-recursive manner. You can imagine that a non-recursive function holds values of the previous iteration. An example: First we define a base functor. The arguments b are recursion points.

>>> data ListF a b = Nil | Cons a b deriving (Show, Functor)

The list is then a fixed point of ListF

>>> type List a = Fix (ListF a)

We can write length function. Note that the function we give to foldFix is not recursive. Instead the results of recursive calls are in b positions, and we need to deal only with one layer of the structure.

>>> :{
let length :: List a -> Int
length = foldFix $ \x -> case x of
Nil      -> 0
Cons _ n -> n + 1
:}

If you already have recursive type, like '[Int]', you can first convert it to `Fix (ListF a)` and then foldFix. Alternatively you can use recursion-schemes combinators which work directly on recursive types.

A fix-point type.

Monadic fixpoints. For a detailed discussion, see Levent Erkok's thesis, Value Recursion in Monadic Computations, Oregon Graduate Institute, 2002.

A fixed-point constructor that uses Haskell's built-in recursion. This is strict/recursive.

Fixed point newtype. Ideally we should use the data-fix package, but right now we're rolling our own due to an initial idea to avoid dependencies to be easier to upstream into GHC (for improvements to the pattern match checker involving equality graphs). I no longer think we can do that without vendoring in some part of just e-graphs, but until I revert the decision we use this type.