# Church numerals, .net and working around the value restriction

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

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) =


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,


## 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 =

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).