Javascript and Mathematical Logic

Overview


Concurrent with the development of mathematical logic, a (roughly) equivalent theory of computability was developed. This involved of the development of Lambda Calculus which then also led to Type Theory.

Many programming languages, especially functional languages drew inspiration from these mathematical developments. In fact, the syntax of some Javascript features mirror those that of type theory, and to some degree the lambda calculus.

Function Definition


In type theory, a function is denoted by specifying the type of the input, a right arrow, and the type of the output, as in the following.
{% a \rightarrow b %}
While there are many ways to specify a Javascript function, the arrow notation can be used to specify a function, as in


a => b
					

As an example, consider the following:


let twice = a => 2*a;
					

While the terms in an arrow function do not represent types, as in type theory, the arrow syntax mirrors the type theory declarations.

In the lambda calculus, a function is declared with a {% \lambda %}, followed by the name of the arugment, followed by a {% . %} and then followed by the function body.
{% \lambda x.x %}
The javascript arrow notation mirrors this to a degree. It eliminates the {% \lambda %} and replaces the {% . %} by the arrow =>

The above lambda function in Javascript can be written as


x=>x
					

Function Application


Function application is defined within the lambda calculus. In the formal lambda calculus, functions are not assigned names, rather they are declared anonymously and applied to their arguments immediately.

The following shows the syntax of applying the identity function to the argument {% y %}.
{% \lambda x.x \; y %}
The corresponding Javascript looks like the following:


x=>x(y)
					

Currying


In the initial formal definition of the lambda calculus, functions only take a single argument. Multi argument functions are defined using function currying. That is, a function which takes a single argument and returns another function that takes a single argument.

Consider the following function:
{% a \rightarrow b \rightarrow c %}
This is a function that takes an argument of type {% a %}, which then returns a function that takes an argument of type {% b %}, which then returns an output of type {% c %}.

Currying can be implemented in Javascript. Consider the following declaration.


a=>b=>a+b
					


This is a curried function that returns the result of adding two arguments together. It can be evaluated as in the following:


(a=>b=>a+b) (1)(2)
					
Try it!


Here, the function is declared anonymously and then evaluated right away on the first argument, {% 1 %}. This will return a new function, which is then applied to the argument {% 2 %}. The result of evaluating (beta reduction) this expression is {% 3 %}.