How would you implement a fixed-point operator (Y combinator) in F#?

Question

I'm using F# to create a lambda calculus. I am currently stuck trying to figure out how I would implement the fixed-point operator (also called Y combinator).

I think everything else is in order. Expressions are represented by the following discriminated union:

type Expr =
 | Const of int
 | Plus  of Expr * Expr
 | Times of Expr * Expr
 | Minus of Expr * Expr
 | Div   of Expr * Expr
 | Neg   of Expr
 | Var   of string
 | Fun   of string * Expr
 | App   of Expr * Expr
 | If    of Expr * Expr * Expr

My eval function seems to work. The following examples all yield the expected results.
example 1:
> eval (Fun("x",Plus(Const 7,Var("x"))));;
val it : Expr = Fun ("x",Plus (Const 7,Var "x"))
example 2:
> eval (App(Fun("x",Plus(Const 7,Var("x"))),Const 3));;
val it : Expr = Const 10
example 3:
> eval (If(Const 0,Const 3,Const 4));;
val it : Expr = Const 4

But as I mentioned, I'm having difficulty implementing the fixed-point operator within my lambda calculus. It is defined here as:
Y = lambda G. (lambda g. G(g g)) (lambda g. G(g g))

Does anyone have any suggestions? I've looked at other questions regarding the Y combinator, but couldn't find anything that I was able to successfully adopt.

All help is appreciated.

Edit: Fixed a typo in the code... previously I had Mult instead of Minus in the discriminated union. Funny that I just noticed that!

Answer 1

The version that you're referring to works only with a lazy language, and if your language isn't using a lazy evaluation strategy, you'll get stuck in an infinite loop. Try translating this:

Y = lambda G. (lambda g. G(lambda x. g g x)) (lambda g. G(lambda x. g g x))

Answer 2

As far as I recall it, there are a whole class of Y Combinators in untyped lambda calculus, but it gets difficult to implement even one if your language is strictly typed, although people have tried to do special cases in ML and also F#. It doesn't seem to be very useful if your language supports recursion (which lambda calculus does not). Have a look at the discussions on that topic that Stackoverflow has seen flagged with generic "functional programming" or ML, I think there are some insights to be had:

Y-Combinator Practical Example