Created: Mon Jan 14 15:20:28 CET 2019
Last modiﬁed: Sat Feb 2 06:02:28 CET 2019
Might be useful when reading chapter 2 of The Haskell Road to Maths, Logic and Programming. The code comes from there.
So we want to establish that, for example,
not (not p) are
equivalent no matter what
So we need a function that will test the value of both truth functions
for every possible
We are looking at
not (not p) as a function, and not as a Boolean
value. Let’s determine both expressions’ signatures.
p :: Bool -> Bool not (not p) :: Bool -> Bool
p being the identity function. Given two booleans, equivalence
==. But when we introduce variables, we introduce functions,
== on function sounds pretty irrelevant in this case.
So we want something that will apply an argument to our functions so that they reduce to a simple boolean.
And we want it to work no matter how many variables there are in each expressions. To simplify, we want both expressions to always hold the same number of free names.
g are booleans, we will
f == g. And when
are functions such as
h :: ... -> Bool -> Bool, we’ll just ask whether
f True is equivalent to
g True and same question asked with
The point is that given the signature
Bool -> Bool -> Bool for
g, we get the following call tree; our function will be named
lequiv, for Logical Equivalence.
lequiv f g == lequiv (f T) (g T) && lequiv (f F) (g F) == lequiv ((f T) T) ((g T) T) && lequiv ((f T) F) ((g T) F) && lequiv ((f F) T) ((g F) T) && lequiv ((f F) F) ((g F) F)
Haskell’s FlexibleInstances offer just that, you can activate them
--ghci-options -XFlexibleInstances when
Type classes (with FlexibleInstances)
class TF p where lequiv :: p -> p -> Bool
For both bolleans and
... -> Bool -> Bool, we deﬁne
lequiv as a
function of two arguments, returning a boolean.
p :: Bool -> Bool, we would have
lequiv :: (Bool -> Bool) -> ((Bool -> Bool) -> Bool). (Note that this
implementation doesn’t strictly require type
p to hold only booleans.)
Here is the base case, when
f :: Bool and
g :: Bool,
instance TF Bool where lequiv f g = f == g
And the natural recursion, when both
Bool -> p
are instances of
(Flexible instances are responsible for deﬁning the syntax for
TF p => TF (Bool -> p).)
instance TF p => TF (Bool -> p) where lequiv f g = (lequiv (f True) (g True)) && (lequiv (f False) (g False))
With a sample,
lequiv (\ p -> p) (\ p -> not (not p))
I produced a Scheme version of
lequiv. You can download it