The Y Combinator (2008)(mvanier.livejournal.com)
mvanier.livejournal.com
The Y Combinator (2008)
http://mvanier.livejournal.com/2897.html
13 comments
Do you always need some lazy evaluation to arrive at the Y-combinator? It seems that even for the strict example a lambda was used to hold the recursive call evaluating too early.
Well, anyways, these are very interesting ideas to study and opened up some of the reasoning behind Haskell's laziness for me.
Well, anyways, these are very interesting ideas to study and opened up some of the reasoning behind Haskell's laziness for me.
It doesn't have to be. The stricter version is called 'applicative-order' Y-combinator. The article talks about both versions as well.
The Y combinator may be pictured as
────┬────
┬─┬ ┼─┬─┬
└─┤ │ ├─┘
│ ├─┘
└─┘
Also, check out this video of the lambda terms involved in computing factorial three evolving through beta reductions—to jazz music! It feels oddly fitting somehow...: https://www.youtube.com/watch?v=Bt11BsAZMq8
I'd be curious to hear anyone's thoughts on the graphical notation here—I'd never seen it (or anything similar), and it's intriguing to me, but I wonder if folks have gained some specific concrete benefit from it (e.g. you can look at one of these and figure out what's happening much more quickly or something).
I'd be curious to hear anyone's thoughts on the graphical notation here—I'd never seen it (or anything similar), and it's intriguing to me, but I wonder if folks have gained some specific concrete benefit from it (e.g. you can look at one of these and figure out what's happening much more quickly or something).
Speaking of "Recursion Without Really Recursing" and deep magic, check out this Scala-related paper, "Towards Strong Normalization for Dependent Object Types (DOT)":
http://drops.dagstuhl.de/opus/volltexte/2017/7276/pdf/LIPIcs...
Here, some choice quotes from it:
"We further showed that certain variants of DOT’s recursive self types can be integrated successfully while keeping the calculus strongly normalizing. This result is surprising, as traditional recursive types are known to make a language Turing-complete."
"What is the minimum required change to achieve Turing-completeness? Consistent with our expectations from traditional models of recursive types, we demonstrate that recursive type values are enough to encode diverging computation."
"But surprisingly, with only non-recursive type values via rule (TTYP), we can still add recursive self types to the calculus and maintain strong normalization."
"Can we still do anything useful with recursive self types if the creation of proper recursive type values is prohibited? Even in this setting, recursive self types enable a certain degree of F-bounded quantification, ..."
I wish someone would try to implement Robinson arithmetic (See here: https://en.wikipedia.org/wiki/Robinson_arithmetic and here: https://ncatlab.org/nlab/show/Robinson+arithmetic ) in this. I don't think it'd work - for what I speculate as somewhat obvious reasons - but it'd seem interesting to see where exactly doing so would fail.
http://drops.dagstuhl.de/opus/volltexte/2017/7276/pdf/LIPIcs...
Here, some choice quotes from it:
"We further showed that certain variants of DOT’s recursive self types can be integrated successfully while keeping the calculus strongly normalizing. This result is surprising, as traditional recursive types are known to make a language Turing-complete."
"What is the minimum required change to achieve Turing-completeness? Consistent with our expectations from traditional models of recursive types, we demonstrate that recursive type values are enough to encode diverging computation."
"But surprisingly, with only non-recursive type values via rule (TTYP), we can still add recursive self types to the calculus and maintain strong normalization."
"Can we still do anything useful with recursive self types if the creation of proper recursive type values is prohibited? Even in this setting, recursive self types enable a certain degree of F-bounded quantification, ..."
I wish someone would try to implement Robinson arithmetic (See here: https://en.wikipedia.org/wiki/Robinson_arithmetic and here: https://ncatlab.org/nlab/show/Robinson+arithmetic ) in this. I don't think it'd work - for what I speculate as somewhat obvious reasons - but it'd seem interesting to see where exactly doing so would fail.
> Strong typing simply means that every value in the language has one and only one type, whereas weak typing means that some values can have multiple types.
Aha! Now, any system with subtyping is “weakly typed”! For example, System F-sub!
Aha! Now, any system with subtyping is “weakly typed”! For example, System F-sub!
> Even though we often refer to Y as "the" Y combinator, in actual fact there are an infinite number of Y combinators.
Drop the "the." Just "Y combinator." It's cleaner.
Drop the "the." Just "Y combinator." It's cleaner.
Can you provide a reasonable justification for this?
There's more to it than the joke, because there's a thing or two to say about the use of articles. The "the" there is not incorrect in one reading, as the quote points out, the y combinator can be seen as a generic noun, like "the dog" as a species, or "the blood" as an organ; On the other hand, "the" is "used before an object considered to be unique, or of which there is only one at a time", e.g. "the Queen". So it's kind of contradictory. Just using an indefinite article or nothing at all, is still valid and shorter. People prefer
shorter. I got into an argument before because "some" isn't a useful qualifier. It's perfectly normal to hold seemingly contradictory thoughts like "people like rambling about syntax" and "people don't like that" at the same time, because the meaning that each pertains to only some is obvious from the context. Yes, I'm rambling, and I clicked the article because I need to learn more, so I'm wondering how the y combinator (there, I said it) can illuminate this confusion I just elaborated.
Also, "the" is used to mark abstract terms, e.g. "I go on monday", but "I go on the next monday" (or just next monday).
Does that show why people care about the articles?
One explanation I found for myself why this is a problem is Normal Forms. A DB table can only have one primary key (definite). All else is secondary, n-ary or arbit-ary. The spoken language should be normalizing, too. Spoken lang... it doesn't make a difference in practice though, noone cares to be precise.
Also, "the" is used to mark abstract terms, e.g. "I go on monday", but "I go on the next monday" (or just next monday).
Does that show why people care about the articles?
One explanation I found for myself why this is a problem is Normal Forms. A DB table can only have one primary key (definite). All else is secondary, n-ary or arbit-ary. The spoken language should be normalizing, too. Spoken lang... it doesn't make a difference in practice though, noone cares to be precise.
aw, it's not funny if you have to explain it!
There was a talk using similar examples which I think is very educational.
https://www.infoq.com/presentations/Y-Combinator
I wrote down the examples used in the video (given the poor quality of video) to help myself learn about the Y-Combinator
https://gist.github.com/gdevanla/9171085
Recently, I presented this topic to my team and wrote down a Python equivalent of this example.
https://gist.github.com/gdevanla/07a08d99e183f494d036c6d6fe6...