So once again the time arrives when Santa is looking for Rudolph and I am

writing a blog post for the yearly F# advent

As always I hope I can provide you some insight and fun – practicability is not

the main focus (as you surely find out soon).

## the task at hand

Santa cannot remember christmas-eves date (he is getting quite old kids) but he

remembers it to be a the day after a prime number (tomorrow as it happens) – so

whenever the date showing on his calendar is happens to be prime he rushes out

to see if his elves are getting ready too (this prevents lot’s of running for

Santa).

Of course he has to do this using F# but the Crinch got really nasty this

year and so Santa is only allowed to use pure functions.

## the real thing

Ok the story was lame … I just want to show you how powerful Lambda-Calculus

is by writing a prime-test using nothing (ok almost nothing) but functions.

The reason why I say almost nothing is that I’ll want to keep some types around

(it’s F# after all) and I’ll need rank-2 types for some of this (meaning I

have to get some *for-all types …* in there). In order to do this I am using

**interfaces** and **object-expressions** – you can find more about this and

the reasons behind this in this blog-post here.

So **no** this is not 100% pure lambda-calculus and I take some freedom – but

you can remove the glimmer and translate everything down mechanically – you

just have to write a lot more 😉

So let’s get going.

You can find the example code in this gist

**DISCLAIMER** The following code is not about performance **at all** – indeed

it will work for small numbers but you’ll have to wait quite some time to check

if `1000`

is prime or not – so please keep that in mind.

## Representing the **booleans**

Later on I have to make some decisions (Is this a *prime*? Is a number zero? …)

and of course you’ll want *booleans* and *if* for these situations.

So the first task is to represent both of these using nothing but (lambda-) functions –

also known as Church encodings.

The basic idea is simple: both **true** and **false** will be functions of two

arguments (yeah there is only one … *curry* … bla bla – you know this stuff)

and **true** will just decide to return the first argument while **false** will

return the second.

Packed into an interface `BoolC`

you can do this like this:

type BoolC = abstract apply : 'a -> 'a -> 'a let trueC : BoolC = { new BoolC with member __.apply t _ = t } let falseC : BoolC = { new BoolC with member __.apply _ f = f }

As I’ll gonna need `if`

and `and`

later let’s do this as well.

It turns out `if`

is really just `apply`

here (think about it!):

let ifC (b : BoolC) = b.apply

`and`

is not much harder once we have `if`

– remember `false && x = false`

and

`true && x = x`

:

let andC (a : BoolC) (b : BoolC) : BoolC = ifC a b falseC

The last function I provided gives some way to translate `BoolC`

values back

into F# booleans:

let valueBool (b : BoolC) = b.apply true false

See how nice those rank-2 types work?

## pairs

I need *pairs* to get a working *predecessors* function

so let’s get this done right now.

The idea behind this is similar to the idea behind *booleans* – A pair of two

values `a`

and `b`

is represented as a higher-order function – you give the *pair*

a function taking two arguments and the *pair* is feeding `a`

and `b`

into it.

I like to think of this function as a *selector* function because most often

you feed in a function to select the first or second argument out.

As again I want this nicely typed I did it like this:

type PairC<'a,'b> = abstract apply : ('a -> 'b -> 'c) -> 'c

with selector-functions for the first and second item being:

let fst (p : PairC<_,_>) = p.apply (fun a _ -> a) let snd (p : PairC<_,_>) = p.apply (fun _ b -> b)

finally I’ll need a function to create *pairs* too:

let pair (a : 'a) (b : 'b) : PairC<'a,'b> = { new PairC<'a,'b> with member __.apply f = f a b }

## numbers

To represent numbers you start by observing that a natural number `n`

is

`1+1+1+...+0`

(with `n`

times `1+`

) where `1+`

is the *sucessor*-function and

`0`

is the *initial value*.

Now of course in lambda calculus there are no values but what we are doing is

to give a higher-order function taking in both the *successor* and the *initial
value* and then the task is to apply the

*sucessor*n-times to the

*initial value*.

So let’s start with the type/interface:

type NatC = abstract apply : ('a -> 'a) -> 'a -> 'a

then `zero`

is quite simple:

let zero : NatC = { new NatC with member __.apply _ z = z }

As you can see `zero`

just ignores the *successor* argument and returns the

*initial value*.

Having seen this – it’s not hard to get the **successor** to any number:

let succ (n : NatC) : NatC = { new NatC with member __.apply s z = s (n.apply s z) }

it just applies the *successor* argument to whatever the number evaluates to

with the same *successor* and *initial value* input.

With this it’s easy to represent all numbers – here are some:

let one = succ zero let two = succ one let three = succ two

### addition

If you add `a`

to `b`

you can see this as adding using the *successor* function

`a`

times on `b`

(as `a+b`

= `1+1+1+...+1+0 + b`

):

let add (a : NatC) (b : NatC) = a.apply succ b

and with this we can get a nice series up to `23`

(remember we want to know if

`23`

is prime):

let four = add two two let eight = add four four let sixteen = add eight eight let twenty = add sixteen four let twentythree = add twenty three

### subtraction

As I bloged about before

*subtraction* is a bit harder. We start by defining a *predecessor* function.

The idea is to fold up a tuple

```
(0,0) -> (0,1) -> (1,2) -> ... -> (n-1,n-1+1)
```

and take the first component of the result which can be expressed with what

we have up to now like this:

let pred (n : NatC) : NatC = n.apply (fun p -> pair (snd p) (succ (snd p))) (pair zero zero) |> fst

and with this subtraction is quite easy:

let sub (a : NatC) (b : NatC) = b.apply pred a

### check for equality

Next I need to know if two numbers are equal – I think an easy approach is to

first think how to decide if a number is *zero*:

let isZero (n : NatC) : BoolC = n.apply (fun _ -> falseC) trueC

which is simply done by applying `const false`

n-times to `true`

(so if `n=0`

we will keep `true`

and if not we will override this `n-1`

times with `true`

).

From this we can easily decide if two numbers are equal: they are if the

difference is zero – but since the way the subtraction of `n-m`

will yield always

0 if `m > n`

here we have to do it twice and make sure that both differences are:

let equals (n : NatC) (m : NatC) : BoolC = andC (isZero (sub n m)) (isZero (sub m n))

### divisibility

Now it’s getting a bit more interesting because now I want to know if a

number `m`

divides another `n`

– and I’ll do this by repeatedly subtracting `m`

from

`n`

and look if I end up at `m`

– and because I am to lazy to introduce looping

or recursion I’ll just do it `n`

times and cap the value at `m`

:

let divides (m : NatC) (n : NatC) : BoolC = let decr n' = ifC (equals m n') m (sub n' m) in equals m (n.apply decr n)

Good we have defined `ifC`

😉

Next I’ll reuse this trick to look for the biggest divisor smaller `n`

:

let biggestDivisor (n : NatC) : NatC = let decr m = ifC (divides m n) m (pred m) in n.apply decr (pred n)

### prime-test

And of course with this it’s really easy to see if a number is prime – because

it is if it’s biggest divisor smaller than itself is 1:

let isPrime (n : NatC) : BoolC = equals (biggestDivisor n) (succ zero)

and indeed Santa can check if `23`

is prime (it is) with this:

let is23prime = isPrime twentythree |> valueBool

I really encourage you to play with this and I will happily answer any question you might still have.

**MERRY CHRISTAMS**

Pingback: F# Advent Calendar in English 2015 | Sergey Tihon's Blog()

Pingback: F# Weekly #52, 2015 | Sergey Tihon's Blog()

Pingback: The week in .NET - 12/29/2015 - .NET Blog - Site Home - MSDN Blogs()

Pingback: The week in .NET - 12/29/2015 | 神刀安全网()

Pingback: The Morning Brew - Chris Alcock » The Morning Brew #2000()

Pingback: 주간닷넷 2015년 12월 29일 - Korea Evangelist - Site Home - MSDN Blogs()

Pingback: The week in .NET – 12/29/2015 | .NET Blog()