Editing Fixed-point combinator (section)

==Typing==

In [[System F]] ([[Polymorphism (computer science)|polymorphic]] lambda calculus) a polymorphic fixed-point combinator has type<ref>{{cite journal
 |last1=Girard |first1=Jean-Yves
 |year=1986
 |title=The system {{mvar|F}} of variable types, fifteen years later
 |journal=Theoretical Computer Science
 |volume=45
 |issue=2
 | pages=159–192
 |doi=10.1016/0304-3975(86)90044-7
 |mr=867281
}} See especially p. 180.</ref>
: ∀a.(a → a) → a
where <math>a</math> is a [[type variable]].  That is, if the type of <math>fix\ f </math> fulfilling the equation <math>fix\ f\ =\ f\ (fix\ f) </math> is <math>a</math>, – the most general type, – then the type of <math>f</math> is <math>a \to a</math>. So then, <math>fix</math> takes a function which maps <math>a</math> to <math>a</math> and uses it to return a value of type <math>a</math>.

In the simply typed lambda calculus extended with [[recursive data type]]s, fixed-point operators can be written, but the type of a "useful" fixed-point operator (one whose application always returns) may be restricted.

In the [[simply typed lambda calculus]], the fixed-point combinator Y cannot be assigned a type<ref>[http://cs.anu.edu.au/courses/COMP3610/lectures/Lambda.pdf An Introduction to the Lambda Calculus] {{webarchive |url=https://web.archive.org/web/20140408014716/http://cs.anu.edu.au/courses/COMP3610/lectures/Lambda.pdf |date=2014-04-08}}</ref> because at some point it would deal with the self-application sub-term <math>x~x</math> by the application rule:
: <math>{\Gamma\vdash x\!:\!t_1 \to t_2\quad\Gamma\vdash x\!:\!t_1}\over{\Gamma\vdash x~x\!:\!t_2}</math>

where <math>x</math> has the infinite type <math>t_1 = t_1\to t_2</math>. No fixed-point combinator can in fact be typed; in those systems, any support for recursion must be explicitly added to the language.

=== 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>