fix-factorial.hth

# This defines a fixed-point combinator, showing that Haskenthetical doesn't
# need `letrec` to do recursion. (`def` can be used recursively, but that's not
# necessary for this example.)
#
# I can't claim to understand it. It's based on the example at
# http://rosettacode.org/wiki/Y_combinator#Elm, which I also can't claim to
# understand, even though I wrote it myself.

(def (: id (-> $a $a)) (λ x x))

(type (Mu $a $b) (Roll (-> (Mu $a $b) (-> $a $b))))

(def (: unroll (» -> (Mu $a $b) (Mu $a $b) $a $b))
  (elim-Mu id))

(def (: fix (-> (» -> (-> $a $b) $a $b)
                (-> $a $b)))
  (λ f (let ((g (λ r (f (λ v (unroll r r v))))))
         (g (Roll g)))))


(def (: fac (-> Float Float))
  (fix (λ (f n)
         (if~ n 0
              1
              (* n (f (- n 1)))))))

(fac 5)