#K is the constant function. K(x,y) = x

1 messages · Page 1 of 1 (latest)

fair venture
#

I'm trying to wrap my head around this, but I don't see how you ever get anything out of these functions or their combinations, or why K has two arguments when all it does is relay one of them. K seems just to be like a factorio wire that can only carry one signal. And I don't see how S works given that it seems to need a one argument function and none are defined

thick lark
#

Well for example, you can build the identity function as SKK.

#

You can similarly build whatever other functions you want. The program I’ve linked builds a singly-linked list of integers that match the ASCII values of »hello world«.

fair venture
#

Sorry where are the brackets going for SKK?

#

S takes three operands?

thick lark
#

S(K)(K)

#

Sorry, we often omit function application parentheses in these kinds of calculations, because it fills everything with parentheses

#

So SKK is S(K, K) is (S(K))(K)

#

You can see the definition of K at the very top in plain Javascript in the file

fair venture
#

But S only has 2 operands there?

thick lark
#

K = x => _ => x;

#

S = f => g => x => f(x)(g(x));

#

S has 3 args: f, g, x

serene rose
fair venture
#

How does S apply to K if K gives a constant and S needs two functions and a constant

serene rose
serene rose
#

Simpler example: the "+" operator can be thought of as a function that adds 2 numbers

#

So for example, (+) 2 3 = 5, follow?

fair venture
serene rose
#

We can turn this into a function that takes one argument by defining (+ 2) y = (+) 2 y

#

Follow?

fair venture
#

Follow

serene rose
#

So (+2) 3 = 5

#

So that's basically what he's done with the SKK stuff

#

SKK x = S (K) (K) x etc.

thick lark
#

You can do it by hand! Just insert definitions.

#

SKKx (apply S rule) = Kx(KKx) => (apply K rule) = x

#

SKS would also be the identity. In fact, SKy is the identity for any y now that I look at it.

serene rose
#

I thought you were just being obtuse to sound smart lol

#

This is called partial function? application? something like that

fair venture
#

How could x + y be achieved with S and K logic? You take x and apply the +y function, but how do you define a + operator?

#

or a +y operator

serene rose
#

You see the succ function?

#

That's basically a +1, so to do x + y he just did succ y times

#

You could define (+3) _ = (succ(succ(succ(_)))

#

If you wanted you could do a recursive definition so

(+) x _
x = 1: succ _
else: (+) <x - 1> _

fair venture
#

I see that, how is succ defined here?

serene rose
#

At the bottom, just directly as +1

image.png
fair venture
#

Oh okay

#

That's the bottom level of function being put in

serene rose
#

There's some syntactical sugar here where basically f x = (operations) x is just written as f = (operations) but I've chosen to make it explicit by f _ = (operations) _ just to be clear

#

Eh well top and bottom are going to be a bit more grey depending on who you ask but you're right that it's "bottom"

fair venture
#

I had kinda forgotten that real actual things were being put into the S and K stack, rather than just pure S and K

proper marten
serene rose
fair venture
#

It probably doesn't help that I'm unfamiliar with the syntax used to define the functions in the python file and I'm wholly unfamiliar with javascript

serene rose
serene rose
#

Uh, the notation you need to know here is that the rightmost type is the function type and everything above is an argument

image.png
thick lark
#

All functions take exactly one argument. »Multi-arg functions« are functions that take one argument and return another function that takes another argument.

#

add(x,y) can be thought to take one argument, to return an add-y-to-that function.

#

So that add(5,x) = add5(x).

serene rose
#

So Int -> Int -> Int takes 2 ints and returns another Int, but Int -> (Int, Int) takes an Int and returns an (Int, Int), and Int -> (Int -> Int) takes an Int and returns an (Int -> Int) (which itself is something that takes an Int and returns another Int)

thick lark
#

In other words, if you leave away an argument, it remains left open. :D

serene rose
#

Basically the idea for this kind of thing is that you're reducing the arity (which is the number of arguments a function takes)

serene rose
fair venture
thick lark
#

For the more readable version of the SK hello world, have a look at the original lambda calculus source here

serene rose
fair venture
#

Oh sorry I missed that, I'm unfamiliar with both

thick lark
#

JS doesn’t have automatic currying. Haskell is the only somewhat popular language that has it.

serene rose
#

Yeah, this concept of combining/splitting arguments is called currying/uncurrying, not because of the food but because of the mathematician Haskell Curry (who Haskell is named after)

thick lark
#

In Haskell, answering how many arguments a function takes is

  • hard for the first couple of attempts
  • easy for the next 1000 hours
  • later you get into implementation details and questions about how many arguments foo x = \y -> … takes and it becomes complicated again, but luckily that’s veeeery rarely relevant
fair venture
#

All those let [...] (lambda [name] statements define a function [name] as [...]?

serene rose
#

Important distinction if you're going to look into this more, is that currying is related to but is not partial application, which is what we're doing

serene rose
thick lark
fair venture
#

In quchen's more readable .hs thing

#

oh wow that's very low level

thick lark
#

Note how similar let x = y in body is to (lambda x: body)(y)

#

That’s all there is to it

serene rose
#

Did not expect to see another haskeller here... but somehow it's unsurprising to be the person who's doing all this SKK stuff

thick lark
#

It makes the program more readable, and variable names in my lambda calculus is very simple. Anything except whitespace, parentheses and lambda can be used. See the variables literally named 2 and so on :-D

thick lark
serene rose
#

Ah, the classic haskell avoidance of $

image.png
serene rose
thick lark
#

Implementing infix is hard so I didn’t do it

serene rose
#

I was introduced to the language by Philip Wadler, but I can't claim to be anything more than a student in his lectures

thick lark
#

The lambda in my name is unsurprisingly generated with Haskell. I also wrote a compiler to GCode and literally laser-engraved it into my laptop’s lid. :-D

#

How’s that for academic language! haha

serene rose
thick lark
serene rose
#

Well it's glad to hear you're haskelling too because that means my understanding of what you were trying to do is correct lol

#

btw you can surround your links with angle brackets to prevent the embeds from appearing

thick lark
#

Neat!

fair venture
#

Not to be a philistine but if you can define functions in hs, why did you need to define let, and if you can't define functions in hs, how did you define let?

thick lark
#

I’m not that deep into Haskell anymore I’m afraid, I have too many other hobbies, and I’ve worked with it quite excessively for a while. I do still organize the Munihac (Haskell hackfest in Munich)

serene rose
#

Let is basically a way to define local functions, in other words functions within functions

thick lark
fair venture
#

Oh okay

serene rose
#

When I do though I'd love to talk about it with you

thick lark
#

Sure! :-)

fair venture
#

Assumed because of the .hs file extension

thick lark
fair venture
#

Ah okay, very cool

thick lark
#

The compiler is in Haskell, but it takes as input the long string (green marks), parses it, converts it, prints it out to e.g. Javascript

#

I could have opened a file with the source as well (like all the normal compilers and pretty much any programs do), I just wanted to have it all in one place.

#

The wrapper could have been written in any language, I just liked Haskell. But it’s very much possible to do the same program in whatever, e.g. JS.

fair venture
#

Okay so that file is a lambda calc language and a compiler to convert that language to haskell?

thick lark
#

No, to convert it to whatever you want.

See it this way. g++ is a compiler written in c++ that reads text files containing c++ and converts them to assembly.
my program is written in Haskell and reads text written in my own language and converts them to Javascript.

#

I’ve also written a to-haskell backend, but the output of the Javascript version is the nicest.

fair venture
#

That's really cool, thank you. I currently have some free time and am greatly enjoying nand on your recommendation

thick lark
#

Maybe a shorter example of how these things work.

fair venture
#

Parts of me wish I'd done this sort of thing as my degree, but I think I like it more as a side-interest

thick lark
#

The input is λ x. x
The program parses that to internal data structure EAbs "x" (EVar "x")
It then converts it to a different notation (DeBruijn indices), Abs (Var 1)
It then converts that to a different notation, App (App S K) K
It then converts that to a different notation (Javascript) S(K)(K)
It then converts that to string and prints it

Compilers are all about converting stuff ;-)

thick lark
serene rose
#

Definitely spiralled a lot out of control if you reached the point of being the person who made Applicative.Monad

thick lark
#

That was mostly political though. The actual implementation was adding the => and fixing some 150 non-applicative Monad instances.

serene rose
#

Hahah making it official is an extremely useful thing even if only in appearance

thick lark
#

And making it compatible and convincing others it’s a good idea.

#

I’m happy that I did it but today I’m not sure I had the the energy ;-)

serene rose
#

So... any thoughts on my idea that Spoilage is basically asking you to apply the Maybe monad to all your builds?

thick lark
thick lark
serene rose
#

I might, depending on the context 😛

thick lark
#

I guess you can see spoilables as Maybe X

serene rose
#

Sometimes Int is integer, sometimes Integral, etc.

thick lark
#

That is, spoilable-taking factories are.

serene rose
#

Yeah that's basically what I did, it was a bit of a random click but I haven't had anyone aware enough about monads to know how accurate my opinion was!

#

random click, random thought

thick lark
#

This isn’t about monads. It would still apply if you deleted the Monad instance.

#

All you need is Maybe a = Nothing | Just a, no instances

#

But it’s a personal pet peeve, like when people say the IO monad. Don’t worry too much about it.

serene rose
#

Also more motivation for me to continue getting the practice with monads (and non-monads) that I want to

thick lark
#

Monads are hard until you understand them, then they become easy and you lose the ability to explain them

#

FWIW when I learned about monads it was different – I thought »yeah you can do that but why«. It’s usually either that or confusion. Both resolve after a while. :-D