teodoran / stck

stck is a stack-based programming language
25 stars 4 forks source link

Problem with quotation. #6

Closed mortim closed 4 years ago

mortim commented 4 years ago

Hey, I saw this about concatenative programming. But the quotation [.] doesn't return [[.]] but [true], is it bug ?

d

teodoran commented 4 years ago

Great question! This gives me an excuse to write about Church encoding again.

tl:dr: In short, it's not a bug, and what you're seeing is the effect of a somewhat confusing feature called "unchurching", intended to make STCK easier to use.

Wait what?! How can this be helpful to anyone?

Booleans and integers in STCK are implemented using a clever mathematical representation called Church encoding. You might already be familiar with Church encoding, but in short it lets you create booleans and integers by using functions (or quotations). For instance, in STCK the quotation [.] is the implementation of the boolean true, and [swap .] is the implementation of the boolean false.

An unfortunate side-effect of using Church encoded booleans, is that we constantly have to translate between the Church representation ([.] and [swap .]), and the value they're representing (true and false), in order to understand whats going on.

For instance, it would be hard to understand what [.] [swap .] and is representing, but when we translate it to true false and, it becomes easier to see what's going on.

Unchurching to the rescue!

Unchurching is a feature that tries to do this translation automatically, by looking for quotations that are equal to boolean and integer values, and translating them into the value they're representing. This feature can be turned on and off by using the church/unchurch commands, as shown in the animation below.

un-church-stck-2

How can [.] be true?

The recorded talk about Church encoding and STCK doesn't really go into details about how Church encoding works, but let me give a short example here that illustrates how true, false and and works in STCK.

Encoding true and false

Church encoding represents true and false as two functions/quotations that takes two values and returns one value. The difference between them is that true returns one value, and false return the other. In a more conventional programming like JavaScript, we could implement this as:

function True(x, y) {
    return x;
}

function False(x, y) {
    return y;
}

How would we go about implementing this in STCK? Lets say we have two values in the stack, and want to create a quotation that returns one of the values. A simple implementation would be to use drop (.) to remove the first value from the stack. true-1

If we wrap . in a quotation, we get something that could work as true. true-2

We can do something similar for false, but now we have to swap the two elements on the stack before we drop the other element. false-1

Again we can wrap swap . in a quotation to get something that can work as false. false-2

Why are we doing this again?

By now you might be wondering why this is a useful way to represent true and false, so let's have a look at how we can implement and.

The boolean operator and should return true when both values are true, and false for anything else. and-1

How could we implement something that works like this in STCK? Well, since true and false are functions, we can apply them as part of our implementation of and.

Lets try to use dup app as our implementation of and. and-2

This works! We copy the true quotation, apply it to the stack, and it removes the remaining true quotation, leaving only the false quotation as we wanted. In addition, it turns out that this works for all combinations of true and false that and should handle!

Wrapping things up

Since this answer is getting quite long already, I won't go into more details about Church encoding, but you can have a look at the STCK standard library if you want to see how the other boolean operators are implemented. Hopefully this answer will also make the recorded talk a little bit more accessible.

If you want to learn more about Church encoding, I recommend having a look at the Wikipedia page, and watching this video from the YouTube channel Computerphile about lambda calculus.

Feel free to ask additional follow-up questions if you want me to clarify anything about STCK, Church encoding and concatenative programming languages in general.

mortim commented 4 years ago

Okay, thanks. I understanding better.

teodoran commented 4 years ago

Great! Good luck on your exploration of concatenative programming languages and STCK.