Printing Church Booleans

Question

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?

Impetus

How does it "not work"? Please edit your post to include the exact error messages you get or the exact differences in the behaviour you get and the behaviour you expect. – Bobette

You're defining an instance for any t -> t -> t, but you're specifically using Bools in the definition of show, which prevents it being a valid definition for arbitrary t. – Bobette

You need a newtype ChBool = ChBool (forall x. x -> x -> x) if you want instances – Pilsudski

yes, if you do as @Pilsudski says (you need to use the Rank2Types or RankNTypes extension) then it works. (You also have to change show b = to show (ChBool b = – Mccaskill

[Although I have my own question about this, it doesn't work to just put instance Show (forall t. t -> t -> t) where even with Rank2Types enabled, I get an error about an "illegal polymorphic type" which I don't really understand, particularly as using a newtype wrapper for the type seems to be absolutely fine.] – Mccaskill

Would be much easier if you didn't insist on implementing Show and instead just had something like showBoolean :: (forall t. t -> t -> t) -> String; showBoolean b = b "True" "False" – Bula

Answer 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

Valladolid

Why doesn't it work with the class Boolean (from Data.Boolean) instead of BiExample? – Impetus

I was just not aware of this class. I will update my answer – Valladolid

Your solution with the Boolean class does not work. Try the following to see the error message: myTrue :: t -> t -> t myTrue = \t _ -> t main = print $ myTrue – Impetus

First of all, you missed class constraints for myTrue: myTrue :: (Show t, Boolean t) => t -> t -> t. Second, this won't work for general type obviously because neither Boolean nor Show class provide sufficient defaults. The instance however is completely valid, and will work for any instantiated type (for example for myTrue :: Bool -> Bool -> Bool) – Valladolid