[SOLVED] Converting from Church Encoding to Numerals

Converting from Church Encoding to Numerals

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.

Solution

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