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:
valid
to check if the proposition is logically valid (true for all possible inputs)
contradiction
to check if the proposition is false for all possible inputs.
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.
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).
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
.
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 valid
ity 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.
::
symbols line up. 2. Instead ofcontradiction f = f == false
, why notcontradiction = not.id
? This makes it the logical negation ofid
. \$\endgroup\$ – Myridium Sep 26 '16 at 14:00contradiction f = (f == False)
is applied to an instance of the typeclassTF a
wherea => Bool
(a
is of typeBool
). This means that in that expression you have,f
is simply aBool
-- it is eitherTrue
orFalse
. So in this case, I think all you want to do is take the negation off
. \$\endgroup\$ – Myridium Sep 26 '16 at 14:09