class Eq a where
(==), (/=) :: a -> a -> Bool
x /= y = not (x == y)
x == y = not (x /= y)
data Tree a = Leaf a | Branch (Tree a) (Tree a)
instance Eq a => Eq (Tree a) where
Leaf a == Leaf b = a == b
Branch l1 r1 == Branch l2 r2 = l1 == l2 && r1 == r2
_ == _ = False
(A) Prove that the instance of Tree in the class Eq satisfies the laws of its class.
Law #1: (x/=y) = not (x==y)
Since we do not redefine the operator (/=), it takes its default method, which defined just like the law to prove.
Law #2: (x==y) && (y==z) ====> (x==z)
(x == y):
Leaf xa == Leaf ya = xa == ya
Branch xl xr == Branch yl yr = xl == yl && xr == yr
_ == _ = False
(y == z):
Leaf ya == Leaf za = ya == za
Branch yl yr == Branch zl zr = yl == zl && yr == zr
_ == _ = False
so (x == z):
Leaf xa == Leaf za ====> (xa == ya) && (ya == za) ====> (xa == za) ====> True
Branch xl xr == Branch zl zr ====> xl == yl && xr == yr && yl == zl && yr == zr
====> xl == zl && xr == zr
====> True
_ == _ = False =====> True
(B) Also prove that the modified instance of Tree in
the class Ord satisfies the laws of its class.
Skip ... (maybe come back later to do it)
This entry was posted
on Saturday, June 30th, 2007 at 2:56 pm and is filed under Haskell - SOE.
You can follow any responses to this entry through the RSS 2.0 feed.
You can leave a response, or trackback from your own site.