Concatenative Combinators
Christopher Diggins — 2006-12-23 03:43:17
I have posted a new chart of combinators along with their associated
bird names, lambda expressions, concatenative algebraic expressions,
joy implementations (ala Brent Kerby's theory of applicative
combinators), and their types.
This is available at
http://www.fundamentals-of-programming.com/combinators.html
This chart is very interesting to me because it has allowed me to
pinpoint what was troubling me about Brent Kerby's system of
applicative combinators.
Both "\a.ab" and "\a.a" map to the "i" operation in Joy despite having
distinct types. It appears that his system is consistent and logical
but only maps unambiguously onto the SK calculus, not the other way
around.
Unfortunately I still haven't solved William's binary concatenative
language problem yet, but I think this is on the right track.
--
http://www.cdiggins.com
William Tanksley, Jr — 2006-12-27 01:55:36
Christopher Diggins <
cdiggins@...> wrote:
> This chart is very interesting to me because it has allowed me to
> pinpoint what was troubling me about Brent Kerby's system of
> applicative combinators.
> Both "\a.ab" and "\a.a" map to the "i" operation in Joy despite having
> distinct types. It appears that his system is consistent and logical
> but only maps unambiguously onto the SK calculus, not the other way
> around.
I believe Manfred noted this characteristic earlier, although I don't
recall where he noted it (probably one of the earlier papers). It's
natural to want two types of substitution rules -- one that only
allows strict identities, and one that is a bit looser (for example,
"swap swap == nop" is only true under the loose rules).
What do you think the result of using stricter rules would be?
> Unfortunately I still haven't solved William's binary concatenative
> language problem yet, but I think this is on the right track.
I suspect it is :-). Thank you!
-Billy
Christopher Diggins — 2006-12-28 17:11:48
On 12/26/06, William Tanksley, Jr <
wtanksleyjr@...> wrote:
>
> Christopher Diggins <cdiggins@...> wrote:
> > This chart is very interesting to me because it has allowed me to
> > pinpoint what was troubling me about Brent Kerby's system of
> > applicative combinators.
>
> > Both "\a.ab" and "\a.a" map to the "i" operation in Joy despite having
> > distinct types. It appears that his system is consistent and logical
> > but only maps unambiguously onto the SK calculus, not the other way
> > around.
>
> I believe Manfred noted this characteristic earlier, although I don't
> recall where he noted it (probably one of the earlier papers). It's
> natural to want two types of substitution rules -- one that only
> allows strict identities, and one that is a bit looser (for example,
> "swap swap == nop" is only true under the loose rules).
It doesn`t surprise me that Manfred has already managed to wrap his
large brain around all of the subtle implications. I think I am
starting to understand more clearly that Brent`s paper did not
particularly care about mapping the SK calculus to Joy but rather his
intent was simply to create an analogue in order to guide the reader
through the process of finding a minimal base for Joy.
> What do you think the result of using stricter rules would be?
I don`t see any reason to use the stricter rules in untyped dialects
of Joy since everything is checked on the fly as you go, however in a
typed dialect I believe this kind of rule is an important part of
eliminating all dynamic checks for stack underflow. One of the
concrete advantages of a type system for Joy dialects is elimination
of some runtime checks and still maintain certain safety guarantees.
> > Unfortunately I still haven't solved William's binary concatenative
> > language problem yet, but I think this is on the right track.
>
> I suspect it is :-). Thank you!
Things are going slowly for the time being because I am on vacation.
More to come in the new year.
Cheers,
Christopher
William Tanksley, Jr — 2006-12-28 21:01:32
Christopher Diggins <
cdiggins@...> wrote:
> On 12/26/06, William Tanksley, Jr <wtanksleyjr@...> wrote:
> > I believe Manfred noted this characteristic earlier, although I don't
> > recall where he noted it (probably one of the earlier papers). It's
> > natural to want two types of substitution rules -- one that only
> > allows strict identities, and one that is a bit looser (for example,
> > "swap swap == nop" is only true under the loose rules).
> It doesn`t surprise me that Manfred has already managed to wrap his
> large brain around all of the subtle implications. I think I am
> starting to understand more clearly that Brent`s paper did not
> particularly care about mapping the SK calculus to Joy but rather his
> intent was simply to create an analogue in order to guide the reader
> through the process of finding a minimal base for Joy.
That makes sense, and also explains two things: first, it explains why
I was able to read his paper instead of being completely baffled; and
second, it explains why I remain completely baffled when reading REAL
combinatorial papers.
In my "spare time" I'm going to have to search for an intro. Reading
Wikipedia isn't quite enough...
> > What do you think the result of using stricter rules would be?
> I don`t see any reason to use the stricter rules in untyped dialects
> of Joy since everything is checked on the fly as you go, however in a
> typed dialect I believe this kind of rule is an important part of
> eliminating all dynamic checks for stack underflow. One of the
> concrete advantages of a type system for Joy dialects is elimination
> of some runtime checks and still maintain certain safety guarantees.
I agree.
Of course, eliminating dynamic checks means that there must be no
dynamic effects. This means that at least every variable-length loop
body and 'if/else' must be completely balanced, so that it neither
consumes nor produces any net stack effect.
This is a little cruel unless you have some other mechanism for
functions to produce variable results. My favorite is dynamic length
arrays.
> > > Unfortunately I still haven't solved William's binary concatenative
> > > language problem yet, but I think this is on the right track.
> > I suspect it is :-). Thank you!
> Things are going slowly for the time being because I am on vacation.
> More to come in the new year.
I'm working on it too... Going slow, but it's going.
> Christopher
-Billy