Haskell church numerals can't print | Expected a type, but T has kind `f`

Question

I'm following a guide on Wikipedia on how to deal with church literals. As per article there is a Haskell snippet:

Link to Wiki Here

type Church a = (a -> a) -> a -> a

church :: Integer -> Church Integer
church 0 = \f -> \x -> x
church n = \f -> \x -> f (church (n-1) f x)

unchurch :: Church Integer -> Integer
unchurch cn = cn (+ 1) 0

However when I try to run it through GHCI I get following error :

main.hs:3:15: error:
    * Expecting one more argument to `Church'
      Expected a type, but `Church' has kind `* -> *'
    * In the first argument of `Show', namely `Church'
      In the instance declaration for `Show Church'
  |
3 | instance Show Church where

I've tried to use deriving show on the type and also

instance Show Church Integer where
    show = church

And unfortunately, both produced more errors. I'm not sure what does Church Integer mean in the function declaration or if that is the part why I cannot derive show?

How can I make this function print?

Can you add link to tutorial, please? I'm not sure if I understand how you can build instance of Show for function. — Dima Kurilo
Well, looks like there is no Show instance in this guide. And you can't define it for type (without language extension). So most probably you want to show not Church, but something like (unchurch . church) 5 — Dima Kurilo

Iceland_jack Iceland_jack · Accepted Answer · 2021-07-02T11:31:26

The idiomatic way is defining it as a newtype, the a should also be universally quantified

>> church 10
10

{-# Language GADTs                    #-}
{-# Language InstanceSigs             #-}
{-# Language RankNTypes               #-}
{-# Language ScopedTypeVariables      #-}
{-# Language StandaloneKindSignatures #-}
{-# Language TypeApplications         #-}

import Data.Kind

type    Church :: Type
newtype Church where
 Church :: (forall a. (a -> a) -> (a -> a)) -> Church

church :: Integer -> Church
church n = Church (ch n) where

 ch :: Integer -> forall a. (a -> a) -> (a -> a)
 ch 0 succ zero = zero
 ch n succ zero = succ (ch (n-1) succ zero)

unchurch :: Church -> Integer
unchurch (Church church) = church @Integer (+ 1) 0

instance Show Church where
 show :: Church -> String
 show = show . unchurch

Haskell church numerals can't print | Expected a type, but T has kind `f`

1 Answers