Lambda is fun!

Lambda is certainly fun, but what I mean here is that the λ in lambda calculus is similar to the expression fun in OCaml.

Recall that in lambda calculus, we have function expressions and function applications:

λx.λy.x+y      (*A function expression*) 
λx.λy.x+y 3 4      (*A function application*)

In OCaml, you can express the same with –fun:

fun x y -> x + y 
(fun x y -> x + y) 3 4

Each term separated by a space after fun and before -> are all arguments to the function expression.  -> is similar to the last dot in lambda calculus, i.e., the expression after -> is the function definition.  In fact, you can treat fun as λ and -> as . in lambda calculus.  The following are the same in OCaml:

fun x -> fun y -> x + y
fun x y -> x + y

A function expression is an anonymous function, i.e., a function without a name.  Of course, you can name the function.  In OCaml:

let f = fun x y -> x + y

Which is equivalent to (the usual way of defining a function) :

let f x y = x + y

Note that the order of evaluation of fun is similar to in lambda calculus too.  The function is evaluated first, then the argument is evaluated (OCaml is eager).  After that, the application is performed.  That is, in OCaml f x y z is equivalent to ((f x) y) z.

Eta Reduction and function

In lambda calculus, we have α-conversion and β-reduction, as discussed in this post.  Here we introduce the last kind of conversion/reduction: η-conversion.  η-conversion is the concept that two functions are the same if and only if they give the same result for all values of an argument.  That is,

λx.M x ↔ M where x must not be a free variable in M

Specifically, when the longer form (λx.M x) is reduced to the shorter form (M), it’s called η-reduction.

Why is η-reduction relevant here?  It’s because function in OCaml can be an η-reduction of fun!  In OCaml, function is like fun that takes only one argument.  E.g., the following are equivalent:

fun x -> x + 1 
function x -> x + 1

function also enables pattern matching.  The argument you pattern match is omitted in function.  E.g., the following are equivalent:

fun x -> match x with
         | 0 -> 1
         | _ -> 0
function | 0 -> 1 | _ -> 0      (*η-reduction of the argument x.*)

An Example: RNA Transcription

We can apply the above when solving the coding problem of RNA transcription (taken from the exercism OCaml track exercise):

Given a DNA strand, return its RNA complement (per RNA transcription).

Both DNA and RNA strands are a sequence of nucleotides.

The four nucleotides found in DNA are adenine (A), cytosine (C), guanine (G) and thymine (T).

The four nucleotides found in RNA are adenine (A), cytosine (C), guanine (G) and uracil (U).

Given a DNA strand, its transcribed RNA strand is formed by replacing each nucleotide with its complement:

• G -> C
• C -> G
• T -> A
• A -> U

First, we define the types according to the mli file in the exercise:

type dna = [ `A | `C | `G | `T ]
type rna = [ `A | `C | `G | `U ]

To convert each DNA nucleotide, we can use pattern matching:

let convert dna =
  match dna with
    | `A -> `U
    | `C -> `G
    | `G -> `C
    | `T -> `A

Note that we are writing in the form of let f x = match x with …this means we can write it using function instead, without specifying the argument dna:

let convert = function `A -> `U | `C -> `G | `G -> `C | `T -> `A

Now, we just need to apply convert to the whole DNA strand.  We can use List.map:

let to_rna dnalist =
  List.map convert dnalist

Note that we are writing in the form of let f x = … x, another chance to η-reduce:

let to_rna = List.map convert

What we did here is also called pointfree style.  Note that because of the value restriction it is sometimes not possible to omit the argument like this.