2

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?

9
  • 2
    f x = x (x $) = x x. It has no type, lambda or no lambda. By eta-expansion f x y = x x y which still has no type. g x = id x = x. I can't follow your reasoning. Commented Mar 29, 2019 at 8:59
  • @WillNess It has no Rank-1 type but it has a Rank-2 type: (forall a. a -> b) -> b. Commented Mar 29, 2019 at 10:17
  • @AaditMShah interesting. doesn't look like it helps us to type f . (. f) though. :) Commented Mar 29, 2019 at 11:52
  • @WillNess Lol, the Y combinator? Let me try to see if I can devise a type for that. Most likely I won't be able to though. AFAIK, little omega can't be typed. Commented Mar 29, 2019 at 11:53
  • @AaditMShah I googled for "does y combinator have a Rank-2 type" and no immediately apparent "yes / no" answer has popped up. Of course it can be done with a newtype... Commented Mar 29, 2019 at 11:56

2 Answers 2

5

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.

Sign up to request clarification or add additional context in comments.

10 Comments

Deleted and apologise.
Slightly more strictly: f x = x x can be typed with rank-2 types (so in GHC, but not in standard Haskell), but not inferred.
I agree with @AlexeyRomanov. You can assign the type (forall a. a -> b) -> b to f x = x x.
@AaditMShah Ah, right. In my amended answer I opted for the shorter type f :: (forall a. a) -> b, but yours is more useful, since it allows non-bottom constant functions.
f x y = x x y is eta-equivalent to the correct definition, so not altogether wrong. the "derivation" is completely out of it, though.
|
1

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.

Comments

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.