REVISED: Thursday, February 8, 2024
Haskell Equational Reasoning.
x + y = y + x -- Commutative Laws
x * y = y * x
(x + y) + z = x + (y + z) -- Associative Laws.
(x * y) * z = x * (y * z)
x * (y + z) = x * y + x * z -- Distributive Laws.
(x + y) * z = x * z + y * z
I. HASKELL EQUATIONAL REASONING EXAMPLES
A. FUNCTION RECEIVES LIST RETURNS NUMBER
1. LIST LENGTH
"Copy, Paste" the following program into your text editor and "File, Save As" eqRes1.hs in your working directory.
eqRes1 :: [a] -> Int
eqRes1 [] = 0
eqRes1 (x:xs) = 1 + eqRes1 xs
Load the eqRes1 program into GHCi and call the function eqRes1 with the list [1,2,3].
GHCi, version 9.8.1: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude>
Prelude> :load eqRes1
[1 of 1] Compiling Main ( eqRes1.hs, interpreted )
Ok, modules loaded: Main.
Prelude>
Prelude> eqRes1 [1,2,3]
3
Prelude>
[1,2,3] is shorthand notation for 1 : (2 : (3 : [])).
Equational reasoning is replacing equals with equals; i.e., proving one expression is equal to another.
eqRes1 [1,2,3] -- Total integers in list 1 + 1 + 1 + 0 = 3.
= 1 + eqRes1 [2,3]
= 1 + (1 + eqRes1 [3])
= 1 + (1 + (1 + eqRes1 []))
= 1 + (1 + (1 + 0))
= 3
2. LIST SUM
"Copy, Paste" the following program into your text editor and "File, Save As" eqRes2.hs in your working directory.
eqRes2 [] = 0
eqRes2 (x:xs) = x + eqRes2 xs
Load the eqRes2 program into GHCi and call the function eqRes2 with the list [1,2,3].
Prelude> :load eqRes2
[1 of 1] Compiling Main ( eqRes2.hs, interpreted )
Ok, modules loaded: Main.
Prelude>
Prelude> eqRes2 [1,2,3]
6
Prelude>
eqRes2 [1,2,3] -- List sum 1 + 2 + 3 + 0 = 6.
= 1 + eqRes2 [2,3]
= 1 + (2 + eqRes2 [3])
= 1 + (2 + (3 + eqRes2 []))
= 1 + (2 + (3 + 0))
= 6
B. FUNCTION RECEIVES TWO LISTS RETURNS ONE LIST
1. APPEND
"Copy, Paste" the following program into your text editor and "File, Save As" eqRes3.hs in your working directory.
(++) :: [a] -> [a] -> [a]
[] ++ ys = ys
(x:xs) ++ ys = x : (xs ++ ys)
Load the eqRes3 program into GHCi and call the function (++) with the lists [1,2,3] [4,5,6].
Prelude> :load eqRes3
[1 of 1] Compiling Main ( eqRes3.hs, interpreted )
Ok, modules loaded: Main.
Prelude>
Prelude> (++) [1,2,3] [4,5,6]
[1,2,3,4,5,6]
Prelude>
[1,2,3] ++ [4,5,6]
= 1 : ([2,3] ++ [4,5,6])
= 1 : (2 : ([3] ++ [4,5,6]))
= 1 : (2 : (3 : ([] ++ [4,5,6])))
= 1 : (2 : (3 : [4,5,6]))
= 1 : (2 : [3,4,5,6])
= 1 : [2,3,4,5,6]
= [1,2,3,4,5,6]
2. ZIP
"Copy, Paste" the following program into your text editor and "File, Save As" eqRes4.hs in your working directory.
import qualified Prelude as P
zip :: [a] -> [b] -> [(a,b)]
zip [] ys = []
zip xs [] = []
zip (x:xs) (y:ys) = (x,y) : zip xs ys
Load the eqRes4 program into GHCi and call the function zip with the lists [1,2,3] [4,5,6,7].
Prelude> :load eqRes4
[1 of 1] Compiling Main ( eqRes4.hs, interpreted )
Ok, modules loaded: Main.
Prelude>
Prelude> zip [1,2,3] [4,5,6,7]
[(1,4),(2,5),(3,6)]
Prelude>
zip [1,2,3] [4,5,6,7] -- Notice, lists are of different lengths.
= (1,4) : zip [2,3] [5,6,7]
= (1,4) : ((2,5) : zip [3] [6,7])
= (1,4) : ((2,5) : ((3,6) : zip [] [7])) -- zip stops at first empty list.
= (1,4) : ((2,5) : ((3,6) : []))
= (1,4) : ((2,5) : [(3,6)])
= (1,4) : [(2,5), (3,6)]
= [(1,4), (2,5), (3,6)] -- Output list length is shortest input list.
II. CONCLUSION
In this tutorial you have been introduced to Haskell Equational Reasoning.
III. REFERENCES
Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.
Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.
Goerzen, J. & O'Sullivan, B. & Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.
Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.
Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.
Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.
