CODEWITHSUNDEEP
haskellfunctional-programming
SavannahGemp
SavannahGemp

Reputation: 405

How to understand nested lambda functions in Haskell

I am trying to understand the meaning of the following 2 lambda expressions in Haskell:

f = \x -> x (\y -> x y)
g = \x -> (\y -> y) x

I tried to convert them, and I got this:

f x y = x x y
g x y = y x

Is this correct? I assumed the arguments of both functions have to be x and y, as they are both found in a lambda expression in the function description. I basically understood it this way: f(x) = x f(y) and f(y) = y x. And for g, g(x) = g(y) x and g(y) = y. But as I am new to Haskell, I'm not very confident with these types of conversion. If not correct, what would be a correct conversion?

Upvotes: 2

Views: 813

Answers (2)

chi
chi

Reputation: 116139

Neither is correct. Your solution uses the functions

f x y = x x y
g x y = y x

which actually mean

f = \x -> (\y -> x x y)
g = \x -> (\y -> y x)

and those differ from the original expressions

f = \x -> x (\y -> x y)
g = \x -> (\y -> y) x

The above two equations can be rewritten as

f x = x (\y -> x y)
g x = (\y -> y) x

But from here, there is no way to turn the remaining lambdas into more arguments for f or g. At best, we can simplify them using beta/eta conversion and get

f x = x x            -- eta  (\y -> x y) = x
g x = x              -- beta (\y -> y) x = x

(Also see the comment below by Will Ness, who points out that through an additional eta expansion in f we could reach the OP's definition. Still, that is incidental.)

Finally, note that Haskell will not accept f x = x x since that can not be typed, unless we use rank-2 types and explicitly provide a type annotation like f :: (forall a. a) -> b. The original code f = \x -> x (\y -> x y) suffers from the same issue. That would also be fine in untyped languages, e.g. the untyped lambda calculus in programming languages theory.

Upvotes: 5

AntC
AntC

Reputation: 2806

The :type command at the GHCi prompt is your friend. Let's take your second example first

λ> :type let g = \x -> (\y -> y) x in g
let g = \x -> (\y -> y) x in g :: p -> p

So g is well-typed and is a convoluted way to write an identity function :: p -> p. Specifically, g takes some x and applies an identity function (\y -> y) to x, resulting in x. GHCi in giving the type uses a fresh type name p, to avoid confusion. No your g x y = ... is not equivalent. (Check it with :type.)

You can abbreviate :type to just :t. Then let's take your first example.

λ> :t let f = \x -> x (\y -> x y) in f
* Occurs check: cannot construct the infinite type: t2 ~ t2 -> t3
* In the first argument of `x', namely `(\ y -> x y)'
  In the expression: x (\ y -> x y)
  In the expression: \ x -> x (\ y -> x y)
* Relevant bindings include
    x :: t2 -> t3 (bound at <interactive>:1:10)
    f :: (t2 -> t3) -> t3 (bound at <interactive>:1:5)

Errk. Is your suggested f the same as that?

λ> :t let f x y = x x y in f
* Occurs check: cannot construct the infinite type:
    t3 ~ t3 -> t4 -> t5
* In the first argument of `x', namely `x'

It at least looks like a similar error message. What are these t2, t3, t4, t5? Again it's GHCi using fresh names for the types, to avoid confusion.

Looking at the let f = ..., GHCi sees x is applied to something, so it gives x :: t2 -> t3 where t2 is the type of its argument, t3 is the return type. It also sees f = \x -> x (blah). So the return type of f must be whatever x returns, i.e. t3, and the argument to f is x. So f :: (t2 -> t3) -> t3.

Inside the (blah), there's x applied to something. So the something (i.e. y) must be the type of x's argument, and the return type must be x's return type. I.e. (\y -> x y) :: t2 -> t3. Errk: then we must have x's argument type same as that, because x is applied to it. And the way we write 'same as' is with ~.

Then the error message tells you GHCi is trying to make sense of t2 ~ (t2 -> t3). (-> binds tighter than ~.) And if you try to subsitute that equivalence for t2 into the RHS you'll get t2 ~ (((... -> t3) -> t3)-> t3) ad infinitum.

Your suggested equivalent for f x y = is not equivalent (the message/typing is a little different). But they're both infinite types, so not allowed.

Upvotes: 1

Related Questions