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 😉