|
|
@@ -6,11 +6,188 @@ description: Encoding various types using only variables and functions |
|
|
|
tags: general |
|
|
|
--- |
|
|
|
|
|
|
|
TODO |
|
|
|
In this post I will briefly explain the [untyped lambda calculus][], then go on to explain |
|
|
|
[church encoding][]. Following that, we will look at an implementation of church encoding using |
|
|
|
javascript; in this article we will focus on encoding booleans as well as natural numbers, as |
|
|
|
they are the simplest to understand. We will then provide functions to operate on our |
|
|
|
representation as well as functions to marshal to and from our representation to javascripts. |
|
|
|
Along the way we will also cover the topic of [currying][], as it will be used extensively in |
|
|
|
the javascript implementation. In the future I hope to go over pairs, lists, and perhaps some |
|
|
|
other types which are more complicated but for the time being booleans and natural numbers |
|
|
|
should provide a good enough introduction to [church encoding][]. |
|
|
|
|
|
|
|
TLDR: Using only functions of one argument and variables (and assuming infinite space), one can |
|
|
|
compute any computable function. Here we will implement booleans and natural numbers using only |
|
|
|
functions and variable bindings to functions; we also implement functions to operate on those |
|
|
|
types (Eg. and, or, xor, not, add, subtract, multiply, etc…). |
|
|
|
|
|
|
|
<!--more--> |
|
|
|
|
|
|
|
TODO |
|
|
|
As I was learning church encoding and lambda calculus I implemented church encodings of various |
|
|
|
types along with functions that operate on those types. I did this in a few of my favorite |
|
|
|
languages; namely in [Haskell](https://www.haskell.org/), [Racket](https://www.haskell.org/), |
|
|
|
and [Lazy Racket](http://docs.racket-lang.org/lazy/index.html), though the implementations were |
|
|
|
to varying degrees of completion. Now many Haskell and Racket programmers are more likely to be |
|
|
|
aware of the lambda calculus and church encoding. However, I think most javascript programmers |
|
|
|
likely have never heard of the concept and would benefit by taking a moment to bend their |
|
|
|
minds. |
|
|
|
|
|
|
|
Before we get started into the 'meat' of this article, I need to explain curried functions as |
|
|
|
they are used extensively in the javascript implementation of church encoded booleans and |
|
|
|
natural numbers. If you already know what a curried function is, feel free to skip this |
|
|
|
section. |
|
|
|
|
|
|
|
Suppose you are given the challenge of writing a function that takes two arguments and returns |
|
|
|
its first. This is easy in every language, and javascript is no exception. Now consider how |
|
|
|
you would do it if you had the following restrictions: |
|
|
|
|
|
|
|
1. You can only use lambda functions and variables |
|
|
|
2. Lambda functions can only take one argument. It cannot be an object or array with some |
|
|
|
expected structure. For example, accepting an array and expecting the arguments to be at |
|
|
|
index 0 and 1 respectively is considered a violation. |
|
|
|
|
|
|
|
At first glance this may seem like a impossible task, but no need to fret. The solution: write |
|
|
|
a function that accepts the first argument but then returns a function which will accept the |
|
|
|
second argument and throw it away. |
|
|
|
|
|
|
|
``` {.javascript .code-term .numberLines } |
|
|
|
var lconst = function (x) { |
|
|
|
var ret = function {y) { |
|
|
|
return x; |
|
|
|
}; |
|
|
|
return ret; |
|
|
|
}; |
|
|
|
``` |
|
|
|
|
|
|
|
On line 2-5 we use a variable `ret` to temporarily store a function to accept the 'second' |
|
|
|
argument; we then return this function. The function itself closes over the argument to the |
|
|
|
outer function and returns it. I could have written `return function (y) { return x; };` |
|
|
|
instead of lines 1-3 but prefer the added readability of newlines; but to do this and avoid |
|
|
|
javascripts automatic semicolon insertion we have to temporarily store the function in a |
|
|
|
variable. This is because semicolons are inserted automatically after return statements in |
|
|
|
javascript. For more details on javascripts automatic semicolon insertion see section 7.9.1 of the |
|
|
|
[ECMAScript 2015 language specification](http://www.ecma-international.org/publications/standards/Ecma-262.htm). |
|
|
|
|
|
|
|
Now lets see our `lconst` function in action: |
|
|
|
|
|
|
|
``` {.javascript .code-term} |
|
|
|
lconst(1)(2); // 1 |
|
|
|
lconst("Alonzo")("Church"); // "Alonzo" |
|
|
|
var alwaysZero = lconst(0); // undefined |
|
|
|
alwaysZero(1); // 0 |
|
|
|
alwaysZero("Alonzo"); // 0 |
|
|
|
``` |
|
|
|
|
|
|
|
|
|
|
|
TODO: Finish explanation about curried functions |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Now that we have gone over curried functions, we need to take a gander at the lambda calculus |
|
|
|
before we get started with church encoding and its implementation in javascript. Here I will |
|
|
|
describe it in terms of javascript, but I highly recommend taking the time to read the wiki |
|
|
|
page on the subject as it does a better job describing it then I can. Particularly, my |
|
|
|
description of the reduction rules are quite rough and lack rigor, but a full description of |
|
|
|
the lambda calculus is beyond the scope of this article. |
|
|
|
|
|
|
|
The lambda calculus' syntax can be given by three simple rules. A lambda term is any |
|
|
|
one of the following: |
|
|
|
|
|
|
|
Variable |
|
|
|
~ A single letter symbol (Eg. `x`) |
|
|
|
|
|
|
|
Lambda Abstraction |
|
|
|
~ if `t` is a lambda term and `x` is a variable, then `λx.t` is a lambda term |
|
|
|
|
|
|
|
Application |
|
|
|
~ if `t` and `s` are lambda terms, then `(t s)` is a lambda term |
|
|
|
|
|
|
|
Now that we can specify a lambda term we now have to talk about how they can be reduced. There |
|
|
|
are three types of reduction. |
|
|
|
|
|
|
|
α-conversion (alpha) |
|
|
|
|
|
|
|
~ Also called alpha-renaming, allows bound variable names to be changed. For example, |
|
|
|
`λx.λy.x` can be alpha converted to `λa.λb.a` or `λy.λx.y` among others. By changing the |
|
|
|
bound variables, the original meaning of the lambda expression is retained. That is, both |
|
|
|
`λx.λy.x` and `λa.λb.a` both can be thought of as curried functions of two arguments that |
|
|
|
return their first argument. |
|
|
|
|
|
|
|
β-reduction (beta) |
|
|
|
~ TODO |
|
|
|
|
|
|
|
η-conversion (eta) |
|
|
|
~ TODO |
|
|
|
|
|
|
|
When a two lambda terms can be reduced to the same expression by α-conversion we say they are |
|
|
|
α-equivalent. β-equivalence and η-equivalence can be defined similarly. |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
TODO: Talk about lambda term reduction α-conversion (alpha), β-reduction (beta), η-conversion (eta) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Some lambda terms are used commonly, and have standard names. Here are some examples |
|
|
|
|
|
|
|
- The `id` function (identity), that is a function that returns its argument. In the lambda |
|
|
|
calculus its given as `λx.x` whose corresponding javascript is as follows. |
|
|
|
|
|
|
|
``` {.javascript .code-term } |
|
|
|
function id (x) { |
|
|
|
return x; |
|
|
|
}; |
|
|
|
``` |
|
|
|
|
|
|
|
- The `const` function, which is a curried function of two arguments that returns its first |
|
|
|
argument. It is given in the lambda calculus as `λx.λy.x` and can be written in javascript as |
|
|
|
follows. Note however, that the function given in javascript can not have the name `const` as |
|
|
|
its a reserved word in javascript; instead we use `lconst`. |
|
|
|
|
|
|
|
TODO reference lconst js definition above |
|
|
|
|
|
|
|
- Similar to the `const` function but with no standard name, what I'll call `constid` is a |
|
|
|
curried function of two arguments that returns its second argument (unlike `const` which |
|
|
|
returns the first one). It is given by `λx.λy.y` in the lambda calculus and can be written in |
|
|
|
javascript as follows. |
|
|
|
|
|
|
|
``` {.javascript .code-term} |
|
|
|
var constid = function (x) { |
|
|
|
var ret = function (y) { |
|
|
|
return y; |
|
|
|
}; |
|
|
|
return ret; |
|
|
|
}; |
|
|
|
``` |
|
|
|
|
|
|
|
Notice that the `constid` function can be obtained by applying `const` to `id` in the lambda |
|
|
|
calculus (`const id`). Similarly in javascript, the `lconst` function can be applied to the |
|
|
|
`id` to obtain `constid`. |
|
|
|
|
|
|
|
``` {.javascript .code-term} |
|
|
|
var constid = lconst(id); |
|
|
|
``` |
|
|
|
|
|
|
|
Now by this point you are likely scratching your head a little. How in the world can just |
|
|
|
functions and variable bindings alone allow us to represent booleans, and nature numbers; let alone |
|
|
|
have the ability to express any turing computable function. |
|
|
|
|
|
|
|
|
|
|
|
((λx.λy.x) id) |
|
|
|
≡ (λy.id) |
|
|
|
≡ (λy.λa.a) |
|
|
|
≡ constid |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
``` {.javascript .code-term .numberLines} |
|
|
|
/** |
|
|
@@ -397,3 +574,7 @@ for (i = 0; i < 10; i += 1) { |
|
|
|
Find a way to include source files without having to copy-paste them into the article. |
|
|
|
See: http://stackoverflow.com/questions/21584396/pandoc-include-files-filter-in-haskell |
|
|
|
--> |
|
|
|
|
|
|
|
[untyped lambda calculus]: https://en.wikipedia.org/wiki/Lambda_calculus |
|
|
|
[church encoding]: https://en.wikipedia.org/wiki/Church_encoding |
|
|
|
[currying]: https://en.wikipedia.org/wiki/Currying |