# Establishing equiv­a­lences in Haskell

Created: Mon Jan 14 15:20:28 CET 2019

Last mod­i­ﬁed: Sat Feb 2 06:02:28 CET 2019

Might be use­ful when read­ing chap­ter 2 of The Haskell Road to Maths, Logic and Programming. The code comes from there.

So we want to es­tab­lish that, for ex­am­ple, `p` and `not (not p)` are equivalent no mat­ter what `p` is.

So we need a func­tion that will test the value of both truth func­tions for every pos­si­ble `p`.

We are look­ing at `not (not p)` as a func­tion, and not as a Boolean value. Let’s de­ter­mine both ex­pres­sions’ sig­na­tures.

``````p :: Bool -> Bool

not (not p) :: Bool -> Bool``````

With `p` be­ing the iden­tity func­tion. Given two booleans, equiv­a­lence reduces to `==`. But when we in­tro­duce vari­ables, we in­tro­duce func­tions, and us­ing `==` on func­tion sounds pretty ir­rel­e­vant in this case.

So we want some­thing that will ap­ply an ar­gu­ment to our func­tions so that they re­duce to a sim­ple boolean.

And we want it to work no mat­ter how many vari­ables there are in each expressions. To sim­plify, we want both ex­pres­sions to al­ways hold the same num­ber of free names.

So when `f` and `g` are booleans, we will `f == g`. And when `f` and `g` are func­tions such as `h :: ... -> Bool -> Bool`, we’ll just ask whether or not `f True` is equiv­a­lent to `g True` and same ques­tion asked with `False`.

The point is that given the sig­na­ture `Bool -> Bool -> Bool` for `f` and `g`, we get the fol­low­ing call tree; our func­tion 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 of­fer just that, you can ac­ti­vate them with `-XFlexibleInstances` or `--ghci-options -XFlexibleInstances` when using Stack.

Type classes (with FlexibleInstances)

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

For both bol­leans and `... -> Bool -> Bool`, we de­ﬁne `lequiv` as a function of two ar­gu­ments, re­turn­ing a boolean.

Given `p :: Bool -> Bool`, we would have `lequiv :: (Bool -> Bool) -> ((Bool -> Bool) -> Bool)`. (Note that this im­ple­men­ta­tion does­n’t strictly re­quire 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 nat­ural re­cur­sion, when both `p` and `Bool -> p` are in­stances of `TF`.

(Flexible in­stances are re­spon­si­ble for deﬁn­ing the syn­tax 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 sam­ple,

``lequiv (\ p -> p) (\ p -> not (not p))``

I pro­duced a Scheme ver­sion of `lequiv`. You can down­load it there.

source code