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, `p`

and `not (not p)`

are
equivalent no matter what `p`

is.

So we need a function that will test the value of both truth functions
for every possible `p`

.

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
```

With `p`

being the identity function. Given two booleans, equivalence
reduces to `==`

. But when we introduce variables, we introduce functions,
and using `==`

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.

So when `f`

and `g`

are booleans, we will `f == g`

. And when `f`

and `g`

are functions such as `h :: ... -> Bool -> Bool`

, we’ll just ask whether
or not `f True`

is equivalent to `g True`

and same question asked with
`False`

.

The point is that given the signature `Bool -> Bool -> Bool`

for `f`

and
`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
with `-XFlexibleInstances`

or `--ghci-options -XFlexibleInstances`

when
using Stack.

**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.

Given `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* `p`

*and* `Bool -> p`

*are instances of* `TF`

.

(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
there.