Printing Church Booleans

问题:

The following code is meant to print Church encoding of booleans as Haskell's Bool:

{-#LANGUAGE FlexibleInstances #-}

instance Show (t -> t -> t) where
  show b = show $ b True False

Which leads to this error:

<interactive>:4:21: error:
• Couldn't match expected type ‘t’ with actual type ‘Bool’
  ‘t’ is a rigid type variable bound by
    the instance declaration at <interactive>:3:10-27
• In the first argument of ‘b’, namely ‘True’
  In the second argument of ‘($)’, namely ‘b True False’
  In the expression: show $ b True False
• Relevant bindings include
    b :: t -> t -> t (bound at <interactive>:4:8)
    show :: (t -> t -> t) -> String (bound at <interactive>:4:3)

How to make it work?

回答1:

The problem is that show :: (t -> t -> t) -> String should work for any function working on any type t. You are assuming that t is Boolean which is illegal, because (according to GHC) "t is a rigid type variable" and cannot be unified with specialized type.

---

One possible solution would be to specialize your instance by Bool (FlexibleInstances are necessary)

{-#LANGUAGE FlexibleInstances #-}

instance Show (Bool -> Bool -> Bool) where
  show b = show $ b True False

But this will reduce generality of your Church's boolean.

It is impossible to define flexible solution that would work on any type, because you will need to have two representatives of that type that would describe true and false cases, and there are types such like Void which have no (defined) values.

---

An idea that comes to my mind and is quite universal is to add few more class constraints to t:

{-#LANGUAGE FlexibleInstances #-}
import Data.Boolean

instance (Show t, Boolean t) => Show (t -> t -> t) where
  show b = show $ b true false

The Boolean class collects types that can be understood as logic values in some terms. For example for Bool:

instance Boolean Bool where
  true = True
  false = False
  notB = not
  (||*) = (||)
  (&&*) = (&&)

And now we can ensure that

• t is a thing that you can actually show
• There are at least two valid and different values of type t that appear as true and false

Which are the required circumstances to actually be able to show a function of such signature in this way.

IMPORTANT

Following example won't work:

show (true :: (Show t, Boolean t) => t -> t -> t) 

The problem is that typechecker won't guess which t are you going to have here. This solution provides valid and working instance, but only for fully instantiated types. If you get ambiguity error, you will need to specify what is t:

show (true :: Bool -> Bool -> Bool)
>>> "True"

show (true :: Int -> Int -> Int)  -- assuming Boolean instance
>>> "1"

---

EDIT:

Yet another idea was mentioned in the comments. The solution would be to wrap your Church boolean with Rank2Type:

{-# LANGUAGE Rank2Types #-}

newtype ChBool = ChBool (forall t. t -> t -> t)

Which will let t be any type independent of the context. Then you may define casual instance like this:

instance Show ChBool where
  show (ChBool f) = show $ f True False