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
