Converting from Church Encoding to Numerals

Question

I am trying to convert Church Encoding to numerals. I have defined my own Lambda definition as follows:

type Variable = String

data Lambda = Lam Variable Lambda
            | App Lambda Lambda
            | Var Variable
            deriving (Eq, Show)

I have already written a conversion of numerals to church encoding and it works as I expect it to, here's how I defined it:

toNumeral :: Integer -> Lambda
toNumeral n = Lam "s" (Lam "z" (wrapWithAppS n (Var "z")))
  where
    wrapWithAppS :: Integer -> Lambda -> Lambda
    wrapWithAppS i e
        | i == 0 = e
        | otherwise = wrapWithAppS (i-1) (App (Var "s") e)

I ran my own tests and here's the outputs from the terminal when testing for 0, 1, and 2:

*Church> toNumeral 0
Lam "s" (Lam "z" (Var "z"))
*Church> toNumeral 1
Lam "s" (Lam "z" (App (Var "s") (Var "z")))
*Church> toNumeral 2
Lam "s" (Lam "z" (App (Var "s") (App (Var "s") (Var "z"))))

Now I am trying to do the opposite and I just cannot wrap my head around the arguments that need to be passed. Here's what I have:

fromNumeral :: Lambda -> Maybe Integer
fromNumeral  (Lam s (Lam z (App e (Var x))))
    | 0 == x = Just 0
    | ...

I tried replacing (App e (Var x)) with (Var x) but I get this error for both when I try to test my base case of converting church encoding of 0 to Just 0:

*** Exception: Church.hs:(166,1)-(167,23): Non-exhaustive patterns in function fromNumeral

The way I am understanding the lambda encoding for the 3 numbers is this way:

0: \s. \z. z

1: \s. \z. s z

2: \s. \z. s (s z)

So I assume my logic is correct, but I am having a difficult time figuring out how the reverse conversion would be. I am fairly new to Haskell so any help with explaining what I could be doing wrong is greatly appreciated.

Fyodor Soikin Fyodor Soikin · Accepted Answer · 2019-11-04T05:38:00

You should match on the outer (Lam "s" (Lam "z" )), but the inner chain of Apps should be parsed recursively, mirroring the way it was constructed:

fromNumeral (Lam s (Lam z apps)) = go apps
    where
        go (Var x) | x == z = Just 0
        go (App (Var f) e) | f == s = (+ 1) <$> go e
        go _ = Nothing

fromNumeral _ = Nothing

Converting from Church Encoding to Numerals

1 Answers