I find it kindof fun to play with lambda calculus from time to time. Recently I had another go at the church numerals and the goal of my little kata was get a nice type-representation for them:
Have something lie
– zero :: Number
– a successor function succ :: Number -> Number
– and the most trivial operators: add :: Number -> Number -> Number
and mult :: Number -> Number -> Number
Easy: Haskell
It’s not too hard to do this in Haskell, if you allow me to use existential types:
{-# LANGUAGE RankNTypes #-} module ChurchNumerals where import Prelude hiding (succ) newtype Number = Nr (forall a. (a -> a) -> a -> a) eval :: Number -> Integer eval (Nr a) = a (+1) 0 zero :: Number zero = Nr (\ _ z -> z) succ :: Number -> Number succ (Nr a) = Nr (\ s z -> s (a s z)) add :: Number -> Number -> Number add (Nr a) = a succ mult :: Number -> Number -> Number mult (Nr a) b = a (add b) zero one :: Number one = succ zero two :: Number two = succ one
Using .net / Fsharp
Well for algebraic data-types there is are no existentials in F# but maybe we don’t really need it (??):
module Numbers = type Number<'a> = Nr of ( ('a->'a) -> 'a -> 'a) let zero = Nr (fun _ z -> z) let succ (Nr n) = Nr (fun s z -> s (n s z)) let eval (Nr f) = f ( (+) 1) 0 let show (Nr f) = f ( (+) "1+") "0" |> printf "%s" let add (Nr f : _ Number) (b : _ Number) = f succ b let mult (Nr f : _ Number) (b : _ Number) = f (add b) zero
So it might look just like a minor annoyance (to move the generic-parameter around) and on first glance it seems to work:
let multiplyStuff = let one = succ zero let two = succ one let three = succ two let res = mult two three eval res // return 6
But just the innocent looking addition of a sideeffekt that does not alter the behviour:
let multiplyStuff = let one = succ zero let two = succ one let three = succ two let res = mult two three show res // print the structure eval res
bust the compiler:
Type mismatch. Expecting a Number<int> but given a Number<string> The type 'int' does not match the type 'string'
And the even more innocent looking definition of just the 1-literal:
let one = succ zero
gives us a value restricition error:
Value restriction. The value 'one' has been inferred to have generic type val one : Number<'_a> Either define 'one' as a simple data term, make it a function with explicit arguments or, if you do not intend for it to be generic, add a type annotation.
What is going on
In the first example I cheated – I wraped it into a local binding so that the compiler could infer concrete types for one
, two
, three
and res
– indeed the eval res
forces res
to be of type Number<int>
and mult
(which indeed is Number<Number<'a>> -> Number<Number<'a>> -> Number<'a>
) forces the others to be Number<Number<'int>>
.
The second example now of course cannot compile as res
suddenly needs to be both Number<int>
and Number<string>
(from show : Number<string> -> unit
).
The third example finaly just tells you that the compiler simply does not know what the 'a
in one : Number<'a>
is supposed to be (You cannot have a generic value in .net).
Interfaces to the rescue
While we cannot have generic functions in data-types/records in .net/F# we can have generic methods on interfaces.
And indeed we get a reasonable nice solution to our problem using an interface INumber
that just contains the same application Nr
had in the above example:
module Churchs = type INumber = abstract apply : ('a -> 'a) -> 'a -> 'a let eval (n : INumber) = n.apply ( (+) 1) 0 let show (n : INumber) = n.apply ( (+) "1+") "0" |> printf "%s" let zero = { new INumber with member __.apply(_: 'a -> 'a) (z: 'a): 'a = z } let succ (n : INumber) = { new INumber with member __.apply(s: 'a -> 'a) (z: 'a): 'a = s (n.apply s z) } let one : INumber = succ zero let two : INumber = succ one let three : INumber = succ two let add (a : INumber) (b : INumber) : INumber = a.apply succ b let mult (a : INumber) (b : INumber) : INumber = a.apply (add b) zero
Yes the definition of zero
and succ
is a bit more verbose but the rest of the code stays the same and the types now finally are as simple as we wanted them (or as Haskell got them).
Indeed this is another reason why interfaces are often more usefull than records of functions in F# and should not be considered to be an antipattern – even if you have some Haskell background 😉