GHC.Internal.Control.Monad.Fix

Monads having fixed points with a 'knot-tying' semantics. Instances of MonadFix should satisfy the following laws:

Purity

mfix (Control.Monad.return . h) = Control.Monad.return (fix h)

Left shrinking (or Tightening)

mfix (\x -> a >>= \y -> f x y) = a >>= \y -> mfix (\x -> f x y)

Sliding

mfix (Control.Monad.liftM h . f) = Control.Monad.liftM h (mfix (f . h))

, for strict

h

.

Nesting

mfix (\x -> mfix (\y -> f x y)) = mfix (\x -> f x x)

This class is used in the translation of the recursive do notation supported by GHC and Hugs.

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 5120

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)) 5120

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)

The implementation of Control.Monad.Fix.mfix for IO.

This operation may fail with:

• FixIOException if the function passed to fixIO inspects its argument.

Examples

the IO-action is only executed once. The recursion is only on the values.

>>> take 3 <$> fixIO (\x -> putStr ":D" >> (:x) <$> readLn @Int):D2[2,2,2]

If we are strict in the value, just as with Data.Function.fix, we do not get termination:

>>> fixIO (\x -> putStr x >> pure ('x' : x))* hangs forever *

We can tie the knot of a structure within IO using fixIO:

data Node = MkNode Int (IORef Node)

foo :: IO ()
foo = do
  p <- fixIO (p -> newIORef (MkNode 0 p))
  q <- output p
  r <- output q
  _ <- output r
  pure ()

output :: IORef Node -> IO (IORef Node)
output ref = do
  MkNode x p <- readIORef ref
  print x
  pure p

>>> foo000

The loop operator expresses computations in which an output value is fed back as input, although the computation occurs only once. It underlies the rec value recursion construct in arrow notation. loop should satisfy the following laws:

extension

loop (arr f) = arr (\ b -> fst (fix (\ (c,d) -> f (b,d))))

left tightening

loop (first h >>> f) = h >>> loop f

right tightening

loop (f >>> first h) = loop f >>> h

sliding

loop (f >>> arr (id *** k)) = loop (arr (id *** k) >>> f)

vanishing

loop (loop f) = loop (arr unassoc >>> f >>> arr assoc)

superposing

second (loop f) = loop (arr assoc >>> second f >>> arr unassoc)

where

assoc ((a,b),c) = (a,(b,c))
unassoc (a,(b,c)) = ((a,b),c)