Establishing equiv­a­lences in Haskell

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

Last mod­i­fied: 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­fine 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 defin­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