## Tuesday, September 27, 2016

### The fixpoint combinator

Consider the following recursive definition of the factorial function. $FAC = \lambda n.\;IF \left(=\;n\;0\right)\;1\;\left(*\;n\;\left(FAC\;\left(-\;n\;1\right)\right)\right) \nonumber$ The definition relies on the ability to name a $\lambda$-abstraction and then to refer to this name inside the $\lambda$-abstraction itself. No such facility is provided by the $\lambda$-calculus. $\beta$-abstraction is applying $\beta$-reduction backwards to introduce new $\lambda$-abstractions, thus $+\;4\;1\leftarrow \left(\lambda x.\;+\;x\;1\right)\; 4$. By $\beta$-abstraction on $FAC$, its definition can be written $FAC = \left(\lambda fac.\;\left(\lambda n.\;IF\left(=\;n\;0\right)\;1\;\left(*\;n\;\left(fac\;\left(-\;n\;1\right)\right)\right)\right)\right) FAC \nonumber$ This definition has taken the form $FAC = g\;FAC$ where $g = \left(\lambda fac.\;\left(\lambda n.\;IF\left(=\;n\;0\right)\;1\;\left(*\;n\;\left(fac\;\left(-\;n\;1\right)\right)\right)\right)\right)$ is without recursion. We see also that $FAC$ is a fixed point ("fixpoint") of $g$. It is clear this fixed point can only depend on $g$ so supposing there were a function $Y$ which takes a function and delivers a fixpoint of the function as the result, we'd have $FAC = Y\;g = g\;(Y\;g)$. Under the assumption such a function exists, in order to build confidence this definition of $FAC$ works, we will try to compute $FAC\;1$. Recall $\begin{eqnarray} &FAC& = Y\;g \nonumber \\ &g& = \lambda fac.\;\left(\lambda n.\;IF\left(=\;n\;0\right)\;1\;\left(*\;n\;\left(fac\;\left(-\;n\;1\right)\right)\right)\right) \nonumber \end{eqnarray}$ So, $\begin{eqnarray} FAC\;1 &\rightarrow& (Y\;g)\; 1 \nonumber \\ &\rightarrow& (g\;(Y\;g))\;1 \nonumber \\ &\rightarrow& (\left(\lambda fac.\;\left(\lambda n.\;IF\left(=\;n\;0\right)\;1\;\left(*\;n\;\left(fac\;\left(-\;n\;1\right)\right)\right)\right)\right) (Y\;g))\; 1 \nonumber \\ &\rightarrow& \left(\lambda n.\;IF\left(=\;n\;0\right)\;1\;\left(*\;n\;\left(\left(Y\;g\right)\;\left(-\;n\;1\right)\right)\right)\right)\; 1 \nonumber \\ &\rightarrow& *\;1\;\left(\left(Y\;g\right)\;0\right) \nonumber \\ &\rightarrow& *\;1\;\left(\left(g\;\left(Y\;g\right)\right)\;0\right) \nonumber \\ &\rightarrow& *\;1\;\left(\left(\left(\lambda fac.\;\left(\lambda n.\;IF\left(=\;n\;0\right)\;1\;\left(*\;n\;\left(fac\;\left(-\;n\;1\right)\right)\right)\right)\right)\;\left(Y\;g\right)\right)\;0\right) \nonumber \\ &\rightarrow& *\;1\;\left(\left(\lambda n.\;IF\left(=\;n\;0\right)\;1\;\left(*\;n\;\left(\left(Y\;g\right)\;\left(-\;n\;1\right)\right)\right)\right)\;0\right) \nonumber \\ &\rightarrow& *\;1\;1 \nonumber \\ &=& 1 \nonumber \end{eqnarray}$

The $Y$ combinator of the $\lambda$-calculus is defined as the $\lambda$-term $Y = \lambda f.\;\left(\lambda x.\;f\;\left(x\;x\right)\right)\left(\lambda x.\;f\;\left(x\;x\right)\right)$. $\beta$ reduction of this term applied to an arbitrary function $g$ proceeds like this: $\begin{eqnarray} Y\;g &\rightarrow& \left(\lambda f.\;\left(\lambda x.\;f\;\left(x\;x\right)\right) \left(\lambda x.\;f\;\left(x\;x\right)\right)\right)\;g \nonumber \\ &\rightarrow& \left(\lambda x.\;g\;\left(x\;x\right)\right) \left(\lambda x.\;g\;\left(x\;x\right)\right) \nonumber \\ &\rightarrow& g\;\left(\left(\lambda x.\;g\;\left(x\;x\right)\right)\;\left(\lambda x.\;g\;\left(x\;x\right)\right)\right) \nonumber \\ &=& g\;\left(Y\;g\right) \end{eqnarray}$ The application of this term has produced a fixpoint of $g$. That is, we are satisfied that this term will serve as a definition for $Y$ having the property we need and call it the "fixpoint combinator".

In the untyped $\lambda$-calculus, $Y$ can be defined and that is sufficient for expressing all the functions that can be computed without having to add a special construction to get recursive functions. In typed $\lambda$-calculus, $Y$ cannot be defined as the term $\lambda x.\;f\;(x\;x)$ does not have a finite type. Thus, when implementing recursion in a functional programming language it is usual to implement $Y$ as a built-in function with the reduction rule $Y\;g \rightarrow g\;(Y\;g)$ or, in a strict language, $(Y\; g)\;x \rightarrow (g\;(Y\;g))\;x$ to avoid infinite recursion.

For an OCaml like language, the idea then is to introduce a built-in constant $\mathbf{Y}$ and to denote the function defined by $\mathbf{let\;rec}\;f\;x = e$ as $\mathbf{Y}(\mathbf{fun}\;f\;x \rightarrow e)$. Intuitivly, $\mathbf{Y}$ is a fixpoint operator that associates a functional $F$ of type $\alpha \rightarrow \beta$ with a fixpoint $Y(F)$ of type $\alpha \rightarrow \beta \rightarrow \alpha$, that is, a value having the property $\mathbf{Y}\;F = F\;\left(\mathbf{Y}\;F\right)$. The relevant deduction rules involving this constant are: $$$\frac{\vdash f\;(Y\;f)\;x \Rightarrow v} {\vdash (Y\;f)\;x \Rightarrow v} \tag{App-rec}$$$ $$$\frac{\vdash e_{2}\left[Y(\mathbf{fun}\;f\;x \rightarrow e_{1})/f\right] \Rightarrow v} {\vdash \mathbf{let\;rec}\;f\;x=e_{1}\;\mathbf{in}\;e_{2} \Rightarrow v} \nonumber \tag {Let-rec}$$$

References:
[1] The Implementation of Functional Programming Languages,Simon Peyton Jones, 1987.
[2] The Functional Approach to Programming, Guy Cousineau, Michel Mauny, 1998.

## Tuesday, September 20, 2016

### Custom operators in OCaml

If like me, you've always been a little hazy on the rules for defining OCaml operators then, this little post might help!

It is possible to "inject" user-defined operator syntax into OCaml programs. Here's how it works. First we define a set of characters called "symbol characters".

## Symbol character (definition)

A character that is one of

! $% & * + - . / : < = > ? @ ^ | ~  ## Prefix operators The ! ("bang") prefix operator, has a predefined semantic as the operation of "de-referencing" a reference cell. A custom prefix operator can made by from a ! followed by one or more symbol characters. So, to give some examples, one can define prefix operators like !!, !~ or even something as exotic as !::>. For example, one might write something like let ( !+ ) x : int ref → unit = incr x  as a syntactic sugar equivalent to fun x → incr x Additionally, prefix operators can begin with one of ~ and ? and, as in the case of !, must be followed by one or more symbol characters. So, in summary, a prefix operator begins with one of ! ~ ?  and is followed by one or more symbol characters. For example let ( ~! ) x = incr x defines an alternative syntax equivalent to the !+ operator presented earlier. Prefix operators have the highest possible precedence. ## Infix operators It is in fact possible to define operators in 5 different categories. What distinguish these categories from each other are their associativity and precedence properties. ### Level 0 Level 0 operators are left associative with the same precedence as =. A level 0 operator starts with one of = < > | &$

and is followed by zero or more symbol chars. For example, >>= is an operator much beloved by monadic programmers and |> (pipe operator) is a builtin equivalent to let ( |> ) x f = f x.

### Level 1

Level 1 operators are right associative, have a precedence just above = and start with one of

@ ^

. That is, these operators are consistent with operations involving joining things. @@ (the "command" operator) of course has a predefined semantic as function application, that is, equivalent to the definition let ( @@ ) f x = f x.

### Level 2

Level 2 operators are left associative have a precedence level shared with + and - and indeed, are defined with a leading (one of)

+ -

and, as usual, followed by a sequence of symbol characters. These operators are consistent for usage with operations generalizing addition or difference like operations. Some potential operators of this kind are +~, ++ and so on.

### Level 3

Level 3 operators are also left associative and have a precedence level shared with * and /. Operators of this kind start with one of

* / %

followed by zero or more symbol characters and are evocative of operations akin to multiplication, division. For example, *~ might make a good companion for +~ of the previous section.

### Level 4

Level 4 operators are right associative and have a precedence above *. The level 4 operators begin with

**

and are followed by zero or more symbol characters. The operation associated with ** is exponentiation (binds tight and associates to the right). The syntax **~ would fit nicely into the +~, *~ set of the earlier sections.