Editing Fixed-point combinator (section)

=== Type for the Y combinator ===

In programming languages that support [[recursive data type]]s, the unbounded recursion in <math>t = t\to a</math> which creates the infinite type <math>t</math> is broken by marking the <math>t</math> type explicitly as a recursive type <math>Rec\ a</math>, which is defined so as to be isomorphic to (or just to be a synonym of) <math>Rec\ a \to a</math>. The <math>Rec\ a</math> type value is created by simply tagging the function value of type <math>Rec\ a \to a</math> with the data constructor tag <math>Rec</math> (or any other of our choosing).

For example, in the following Haskell code, has <code>Rec</code> and <code>app</code> being the names of the two directions of the isomorphism, with types:<ref>Haskell mailing list thread on [https://groups.google.com/g/fa.haskell/c/8KYrbeFBbYs How to define Y combinator in Haskell], 15 September 2006</ref><ref>{{cite book |last1=Geuvers |first1=Herman |last2=Verkoelen |first2=Joep |title=On Fixed point and Looping Combinators in Type Theory |citeseerx=10.1.1.158.1478}}</ref>

<syntaxhighlight lang=haskell>
Rec :: (Rec a -> a) -> Rec a
app :: Rec a -> (Rec a -> a)
</syntaxhighlight>

which lets us write:

<syntaxhighlight lang=haskell>
newtype Rec a = Rec { app :: Rec a -> a }

y :: (a -> a) -> a
y f = (\ x -> f (app x x)) (Rec (\ x -> f (app x x)))
--       x :: Rec a
--   app x :: Rec a -> a
-- app x x ::          a
</syntaxhighlight>

Or equivalently in OCaml:

<syntaxhighlight lang=ocaml>
type 'a recc = In of ('a recc -> 'a)
let out (In x) = x

let y f = (fun x a -> f (out x x) a) (In (fun x a -> f (out x x) a))
</syntaxhighlight>

Alternatively:

<syntaxhighlight lang=ocaml>
let y f = (fun x -> f (fun z -> out x x z)) (In (fun x -> f (fun z -> out x x z)))
</syntaxhighlight>