2

I am beginner in functional programming and F#. As an exercise im trying to implement church numerals.
First I coded numbers as:

let ZERO = fun p x -> x
let ONE = fun p x -> p x
let TWO = fun p x -> p(p x)
let THREE = fun p x -> p(p(p x))
let FIVE = fun p x ->p(p(p(p(p x))))
... etc

Then i wrote helper function to see if my numbers work:

let toInt p = p (fun x->x+1) 0

for example:

toInt (THREE) |> printfn "%A"

prints 3, as expected.
Also I implemented some arithemtic functions:

let INC = fun n f x -> f((n(f))(x)) //incrementation
let DEC = fun n f x -> n (fun g -> fun h -> h(g f))(fun y->x)(fun y-> y) //decrementation      
let ADD = fun m n -> n(INC)(m) //addition
let MUL = fun m n s z -> n(m s) z //multiplication
let POW = fun m n -> n(MUL m)ONE //exponential

All of them seem to work fine:

toInt (INC THREE) |> printfn "%A"  //prints 4
toInt (DEC THREE) |> printfn "%A" //prints 2
toInt (ADD THREE FIVE) |> printfn "%A" //prints 8
toInt (MUL THREE FIVE) |> printfn "%A"  //prints 15
toInt (POW THREE FIVE) |> printfn "%A"  //prints 243

But I am really struggling to implement subtraction:

let SUB = fun m n ->  n(DEC m)
toInt (SUB FIVE THREE) |> printfn "%A" //gives 64

Above method looks like some kind of exponential instead of subtraction.
I also tried (as wiki suggests):

let SUB = fun m n ->  n(DEC)m

but it results in type mismatch when i try to use it:

toInt (SUB FIVE THREE) |> printfn "%A"  

"Type mismatch. Expecting a
    '(((('a -> 'b) -> ('b -> 'c) -> 'c) -> ('d -> 'e) -> ('f -> 'f) -> 'g) -> 'a -> 'e -> 'g) -> (('h -> 'h) -> 'h -> 'h) -> (int -> int) -> int -> 'i'    
but given a
    '(((('a -> 'b) -> ('b -> 'c) -> 'c) -> ('d -> 'e) -> ('f -> 'f) -> 'g) -> (('a -> 'b) -> ('b -> 'c) -> 'c) -> ('d -> 'e) -> ('f -> 'f) -> 'g) -> ((('a -> 'b) -> ('b -> 'c) -> 'c) -> ('d -> 'e) -> ('f -> 'f) -> 'g) -> (('a -> 'b) -> ('b -> 'c) -> 'c) -> ('d -> 'e) -> ('f -> 'f) -> 'g'    
The types ''a' and '('a -> 'b) -> ('b -> 'c) -> 'c' cannot be unified"

I'm stuck, what am I doing wrong? And I would also appreciate any suggestions how to improve my code.

mrSelfDestruct
  • 21
  • 4
  • Try annotating the types on DEC? `(n:('a->'a)->'a->'a) (f:'a->'a) (x:'a)` but what are the types of `g`, `h` and `y`? – Charles Roddie Oct 06 '19 at 15:08
  • Maybe there's a problem with applying DEC to itself multiple times? Because `toInt ( (ONE DEC) THREE ) |> printfn "%A" ` prints correctly 2. But `toInt ( (TWO DEC) THREE ) |> printfn "%A" ` is a type mismatch. – mrSelfDestruct Oct 06 '19 at 18:17
  • I am not an expert on Church numerals or on typed/untyped lambda calculus, and in particular I don't understand DEC or even how a decrement function is possible. But F# is a typed language and specifying the generic types of all functions in your list will help diagnose the issue. – Charles Roddie Oct 07 '19 at 12:37
  • @CharlesRoddie I think you are right. It looks like F# compiler couldn't infer the types. If I define `let SUB = fun m n -> n(DEC)m` and then call: `SUB THREE TWO` it is translated to `DEC(DEC(THREE))`. I guess that compiler doesn't know that the result of `DEC(DEC(THREE))` has a type `('a->'a)->'a->'a)` (which is a type of my numbers). But i have no idea how to fix it. I wrote those functions in javascript and in js everything works fine, which is another hint that type inference is a problem. – mrSelfDestruct Oct 07 '19 at 21:00
  • I think found a question with the same problem in Haskell: https://stackoverflow.com/questions/6595749/subtraction-of-church-numerals-in-haskell?rq=1 However i don't know how to translate it to F#. Or if it is even possible. – mrSelfDestruct Oct 08 '19 at 13:06
  • "another hint that type inference is a problem". You can avoid type inference by specifying all the types as I recommended. – Charles Roddie Oct 11 '19 at 20:19

0 Answers0