3 ms·
>It only makes sense in the untyped lambda calculus Is that really true? ISTR you can impose the type (A -> A) -> A on the Y combinator.
by hollerith 2y ago
>It only makes sense in the untyped lambda calculus
Is that really true? ISTR you can impose the type (A -> A) -> A on the Y combinator.
- hollerith 2y agoHere is Haskell code in which the Y combinator (named "fix" in the code) is given the type (a -> a) -> a: https://play.haskell.org/saved/ndm83XBr https://play.haskell.org/saved/ndm83XBr This next a very simple Haskell program that just prints the first 8 non-negative integers: main = putStrLn $ show $ take 8 $ iterate (+ 1) 0 The linked code is just an elaboration of that where instead of using the built-in "iterate" we define an equivalent "iterate2". Usually to define iterate2 a Haskell programmer would use recursion (i.e., call iterate2 inside the definition of iterate2) but today we avoid the need for a recursive call by using the Y combinator. This disproves the assertion that the Y combinator "only makes sense in the untyped lambda calculus" because the Haskell compiler gives a type to every entity in the linked code.
- lacker 2y agoI would not call that the Y combinator. As traditionally defined the Y combinator is Y = lambda f: (lambda x: f(x(x)))(lambda x: f(x(x))) so it involves applying x to x. So clearly as shown here you can express in Python. The language has to not enforce sane types. But I would say it only makes sense in the untyped lambda calculus because in any other language there would be a more reasonable way to achieve the same effect. As you show in your example, because you achieve the same effect of finding a fixed point, by not using the Y combinator.
- hollerith 2y agoYou can say that "fix" is not the Y combinator, but I've demonstrated in Haskell code that "fix" does the thing the Y combinator is famous for doing: namely, to eliminate the need for recursive calls. (In fact, I repeat the Haskell code in this comment.) Just because your definition is syntactically different from mine does not mean the definitions are not equivalent. My guess as to why Python programmers define the Y combinator the way you is that in Python a function's arguments are evaluated eagerly whereas in Haskell they are evaluated lazily with the result that my definition would tend to enter an infinite loop in Python (but even in a language with eager evaluation, I suspect a simpler definition than yours is possible, so I'm not sure what is going on with your definition, which is not surprising since I'm no Python expert). That is all I will to say in reply to you, but I do want to take this opportunity to fix a problem with my previous comment, namely, the fact that although HN comments tend to persist forever, links to sites other than HN rot fairly quickly: I will now repeat here on HN the tiny Haskell program that in my previously comment I put behind a link. I'll also avoid the unnecessary use of "$", "putStrLn" and "show" to make the code easier to read by Haskell newbies. Because the convention in Haskell is to reserve single-character variable names for local variables, we name the Y combinator "fix": fix :: (a -> a) -> a fix f = f (fix f) Now to demonstrate the use of "fix". My go-to toy Haskell program is this next which prints the first 8 non-negative integers. main = print (take 8 (iterate (+1) 0)) Unfortunately that is too much of a toy for our purpose here because I does not contain a recursive call, so we will pretend that the function "iterate" is not pre-defined in Haskell with the result that we would need to define it ourselves (and call it iterate2 because of course the name "iterate" is already taken). All the code in this comment has been tested; all four versions (the one above and the three below) of our toy program produce the same output. main = print (take 8 (iterate2 (+1) 0)) iterate2 :: (a -> a) -> a -> [a] iterate2 f x = x : iterate2 f (f x) The final mention of "iterate2" above is a recursive call. We replace it with a (non-recursive) call to "fix" as follows: main = print (take 8 (iterate2 (+1) 0)) iterate2 :: (a -> a) -> a -> [a] iterate2 f = fix (\self -> \x -> x : self (f x)) And here is an intermediate form of our toy program that might help the reader understand how the form that uses "fix" was derived from the original form: main = print (take 8 (iterate2 (+1) 0)) iterate2 :: (a -> a) -> a -> [a] iterate2 f = loop where loop x = x : loop (f x)
- codethief 2y agoAt least in simply-typed lambda calculus it's not possible, see also https://crypto.stanford.edu/~blynn/lambda/simply.html https://crypto.stanford.edu/~blynn/lambda/simply.html : > This implies the Y combinator and omega combinator cannot be expressed in this system. […] In other words, programs always halt. I assume the reason you can still write down the type in Haskell (as in your example further down) is that Haskell types include the bottom?