Logical contradiction type definitions

Question

(Homework alert)

Working my way through "The Haskell Road...", not sure about my solution to exercise 2.15 on page 48 of the second edition:

A propositional contradiction is a formula that yields false for every combination of truth values for its propositional letters. Write Haskell definitions of contradiction tests for propositional functions with one, two, and three variables.

I somehow gather from the way the question is asked that they expect something along the lines of:

contradiction_1 :: (Bool -> Bool) -> Bool
contradiction_1 f = (f True) == False && (f False) == False

and so on.

However, previously in the text it has been shown how to use a type class to implement validity and logical equivalence:

{-# LANGUAGE FlexibleInstances #-}

class TF p where
  valid :: p -> Bool
  lequiv :: p -> p -> Bool

instance TF Bool where
  valid = id
  lequiv f g = f == g

instance TF p => (Bool -> p) where
  valid = valid (f True)
       && valid (f False)
  lequiv f g = lequiv (f True) (g True)
            && lequiv (f False) (g False)

This above is all in the textbook.

So I thought that I can simply add the definition for contradiction as follows:

class TF p where
  valid :: p -> Bool
  contradiction :: p -> Bool -- added
  lequiv :: p -> p -> Bool

instance TF Bool where
  valid = id
  contradiction f = f == False -- added
  lequiv f g = f == g

instance TF p => (Bool -> p) where
  valid = valid (f True)
       && valid (f False)
  contradiction f = contradiction (f True) -- added
                 && contradiction (f False) -- added
  lequiv f g = lequiv (f True) (g True)
            && lequiv (f False) (g False)

This now is the code from the textbook, still unchanged, only with my additions.

It seems to work, in the sense that it only returns true for actual contradictions for what I've tried so far, for example, with GHCI:

*Main> contradiction (\p -> p && (not p))
True
*Main> contradiction (\p q -> (p || q) && ((not p) && (not q)))
True
*Main> contradiction (\p q r -> p && q && ((not p) && r))
True

But I have to admit that I really don't understand what exactly the code I wrote is doing (I did it with "pattern matching", if you know what I mean).

PS: I cannot tag the question as I would like because I don't have enough rep to create new tags.

Answer 1

Alright, this is the first time I've used Typeclasses so someone feel free to slap me with a tuna if I mess something up.

First of all, I don't understand why the use of "FlexibleInstances" is necessary, and it scares me because these kinds of warnings are usually put in place for a reason. With that out of the way, I'll go through the code.

---

The first thing you should realize is that in Haskell, typeclasses are basically the same thing as Java's interfaces. They define a contract of behaviour which instances of the class must obey. In this case, the typeclass I'm calling Prop promises the user three methods:

1. valid to check if the proposition is logically valid (true for all possible inputs)
2. contradiction to check if the proposition is false for all possible inputs.
3. lequiv to check if two propositions of the same number of arguments have an identical truth value given the same inputs.

These correspond to three questions which we could ask of any proposition which is a function of any number of propositional atoms. In case you're unfamiliar with this terminology, an 'atom' is one of the inputs to a proposition which is a function taking some number of atoms and itself evaluating to either True or False.

Typeclass Declaration

The name TF for the type class bears no meaning for me, so I changed it to Prop short for "Proposition".

-- A typeclass which different types may implement.
class Prop p where
  valid         :: p -> Bool            -- Same thing as a Tautism
  contradiction :: p -> Bool            -- False under all conditions/opposite of Tautism
  lequiv        :: p -> p -> Bool   

What we're doing here is creating a new typeclass called Prop. We need the syntax Prop p because we need to define the behaviour of an instance p of the Prop class. If we don't introduce a symbol for it, then how will the compiler know what we're talking about the in the typeclass definition? For example, the line valid :: p -> Bool says that for every instance p of typeclass Prop, there must be a method called valid which maps p to a boolean value. Likewise, there must be a similar method for contradiction.

Now the line lequiv :: p -> p -> Bool may cause some confusion because p appears twice. It's important to understand that p, being an instance of a typeclass, is a type. There are no "objects" as in object-oriented languages. Remember: p is a type which satisfies the typeclass contract given by Prop. The Java equivalent would be a class p implementing an interface Prop. What we're saying here is that for type which implements/is a part of this typeclass Prop, there is a method called lequiv of comparing them. And its type is p -> p -> Bool meaning that it takes in two expressions of type p and returns a boolean indicating whether or not they're equivalent.

---

Boolean Instance Definition

All we've told the compiler so far are our promises: there will be methods for checking whether an instance of Prop is valid or a contradiction, and a method for comparing two propositions of the same type for equality.

To start, we implement these procedures for the most basic type of proposition: one that is just True or False.

-- This is a proposition which is simply a literal Bool!
instance Prop Bool where
  valid         = id
  contradiction = not
  lequiv b1 b2  = b1 == b2

Here, Prop Bool says that in the expression Prop p above, the type whose behaviour/implementation we're defining is the Bool type. How do we check if a Bool is valid? Well, it takes no arguments, so a proposition that is just True or False is valid if it's true, and otherwise a contradiction.

1. valid = id says that the function valid mapping our proposition type of Bool to whether or not it's a valid formula is the function id. (This function just returns whatever it's given).
2. contradiction = not says that the function contradiction mapping the proposition type Bool to whether or not it's a contradiction is the function not. Just as well, because not takes just one Bool as an argument, and returns a Bool. This is compatible with the contract we laid out earlier in the typeclass definition of Prop.
3. lequiv b1 b2 = (b1 == b2) says that the way of comparing two of these propositions (once again, of type Bool here) for logical equivalence is to simply invoke the already existing method ==.

---

Inductive Instance Definition - First Step

This is the fun part. We're using induction. Here's the full code snippet, and then I'll break down each line.

instance (Prop p) => Prop (Bool -> p) where
  valid f         = (valid (f True)) && (valid (f False))
  lequiv f g      = (lequiv (f True) (g True)) && (lequiv (f False) (g False))
  contradiction f = (contradiction $ f True) && (contradiction $ f False)

Now the first line says this: (Bool -> p) is of type Prop, as long as the constraints in what we call the context are met. Here the context is what comes before the =>, and what it says is that p, the type, is a member of the Prop typeclass. This means that we're saying that any type which maps a Bool to any type of Prop is itself an instance of Prop. Why are we doing this? Well, let's start with the simplest case.

Bool is an instance of typeclass Prop, because we defined this 'base case' explicitly. Okay, so then (Bool -> Bool) is also of typeclass prop, because we said that any type (Bool -> <something in class Prop>) is in class Prop. This gives us the functions which take in one boolean argument and return a boolean. Examples: not, id, (\a -> True), (\a -> False). (In fact, these are all such functions).

How have we defined whether to determine whether one of these functions is valid? Our definition says that

valid f = (valid (f True)) && (valid (f False))

It says that a boolean function f of one boolean is valid if and only if (f True) and (f False) are both valid. Of course, the validity of boolean is just that boolean. So in this case, valid can be thought of as being a bit simpler:

valid f = (f True) && (f False)

Alright, so f is valid if and only if it evaluates to True for both arguments! That's what we want.

Now for contradiction:

contradiction f = (contradiction $ f True) && (contradiction $ f False)

This is the key: contradiction asks the question "Is this proposition false for all possible inputs"? To test this, we split f into two parts: its first argument and the rest. If the first argument is True, then is it possible to satisfy proposition f with the remaining arguments? If not, then it's a contradiction. This is the part contradiction $ f True.

f True is itself a function of 1 Bool argument, so it is in class Prop, and so we're able to apply contradiction to it to see if it's a contradiction. We also need to be sure that it's not possible to satisfy f if the first argument is False either, which is why we && this with contradiction $ f False.

I'll leave the lequiv function as an exercise, and move on to the next inductive step.

Inductive Instance Definition - Inception

Since (Bool -> Bool) is of class Prop, then so too is Bool -> (Bool -> Bool). I could be mistake, but I'm fairly sure that Bool -> Bool -> Bool is actually just short-hand for this. So this means that a boolean function of two boolean variables is itself a proposition. How do we determine its validity? We check if both f True and f False are valid. The former means 'if f True False and f True True both evaluate to True'.

Hopefully you can see now the recursion that's going on (I haven't done a great job explaining it; sorry)-- what we're doing is recursively defining the validity of the type Bool -> Bool -> .... -> Bool so that such a function is valid if and only if it evaluates to True for all possible inputs.