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 😉

Pingback: Dew Drop – September 30, 2014 (#1866) | Morning Dew()

Pingback: F# Weekly #39-41, 2014 | Sergey Tihon's Blog()

Pingback: Gregory Smith()