Fixed point combinator derivied without knot-tying, via recursive types

AnnotatedFix.hs

{-# LANGUAGE GADTSyntax #-}

-- | Derivation of fix without general recursion
-- | Transliteration of PFPL 2nd Ed, pp. 180

module AnnotatedFix where

newtype Self t where
  Fold :: (Self t -> t) -> Self t

unfold :: Self t -> (Self t -> t)
unfold (Fold x) = x

fix :: (a -> a) -> a
fix f = unroll . Fold $ f . unroll

unroll :: Self t -> t
unroll e = unfold e e
-- unroll (Self f) = f (Self f)



-- example
fac :: Int -> Int
fac = fix g
  where
    g f x
      | x == 0    = 1
      | otherwise = x * f (x - 1)