-- This file contains a Hugs implementation of the programs described in: -- -- Mark P. Jones, Computing with lattices: An application of type classes, -- Journal of Functional Programming, Volume 2, Number 4, Oct 1992. -- module Lattice where class Eq a => Lattice a where -- A type class representing lattices bottom, top :: a meet, join :: a -> a -> a lt :: a -> a -> Bool x `lt` y = (x `join` y) == y instance Lattice Bool where -- Simple instances of Lattice bottom = False top = True meet = (&&) join = (||) instance (Lattice a, Lattice b) => Lattice (a,b) where bottom = (bottom,bottom) top = (top,top) (x,y) `meet` (u,v) = (x `meet` u, y `meet` v) (x,y) `join` (u,v) = (x `join` u, y `join` v) -- Defining the least fixed point operator: fix f = firstRepeat (iterate f bottom) firstRepeat xs = head [ x | (x,y) <- zip xs (tail xs), x==y ] -- Maximum and minimum frontiers: data Minf a = Minf [a] data Maxf a = Maxf [a] instance Eq a => Eq (Minf a) where -- Equality on Frontiers (Minf xs) == (Minf ys) = setEquals xs ys instance Eq a => Eq (Maxf a) where (Maxf xs) == (Maxf ys) = setEquals xs ys xs `subset` ys = all (`elem` ys) xs setEquals xs ys = xs `subset` ys && ys `subset` xs instance Lattice a => Lattice (Minf a) where -- Lattice structure bottom = Minf [] top = Minf [bottom] (Minf xs) `meet` (Minf ys) = minimal [ x`join`y | x<-xs, y<-ys ] (Minf xs) `join` (Minf ys) = minimal (xs++ys) instance Lattice a => Lattice (Maxf a) where bottom = Maxf [] top = Maxf [top] (Maxf xs) `meet` (Maxf ys) = maximal [ x`meet`y | x<-xs, y<-ys ] (Maxf xs) `join` (Maxf ys) = maximal (xs++ys) -- Find maximal elements of a list xs with respect to partial order po: maximalWrt po = loop [] where loop xs [] = xs loop xs (y:ys) | any (po y) (xs++ys) = loop xs ys | otherwise = loop (y:xs) ys minimal :: Lattice a => [a] -> Minf a -- list to minimum frontier minimal = Minf . maximalWrt (flip lt) maximal :: Lattice a => [a] -> Maxf a -- list to maximum frontier maximal = Maxf . maximalWrt lt -- A representation for functions of type Lattice a => a -> Bool: data Fn a = Fn (Minf a) (Maxf a) instance Eq a => Eq (Fn a) where Fn f1 f0 == Fn g1 g0 = f1==g1 -- && f0==g0 instance Lattice a => Lattice (Fn a) where bottom = Fn bottom top top = Fn top bottom Fn u l `meet` Fn v m = Fn (u `meet` v) (l `join` m) Fn u l `join` Fn v m = Fn (u `join` v) (l `meet` m) -- Navigable lattices: class Lattice a => Navigable a where succs :: a -> Minf a preds :: a -> Maxf a maxComp :: Navigable a => [a] -> Maxf a -- implementation of complement maxComp = foldr meet top . map preds minComp :: Navigable a => [a] -> Minf a minComp = foldr meet top . map succs instance Navigable Bool where -- instances of Navigable succs False = Minf [True] succs True = Minf [] preds False = Maxf [] preds True = Maxf [False] minfOf (Minf xs) = xs maxfOf (Maxf xs) = xs instance (Navigable a, Navigable b) => Navigable (a,b) where succs (x,y) = Minf ([(sx,bottom) | sx <- minfOf (succs x)] ++ [(bottom,sy) | sy <- minfOf (succs y)]) preds (x,y) = Maxf ([(px,top) | px <- maxfOf (preds x)] ++ [(top,py) | py <- maxfOf (preds y)]) instance Navigable a => Navigable (Fn a) where succs (Fn f1 f0) = Minf [Fn (Minf [y]) (preds y) | y <- maxfOf f0] preds (Fn f1 f0) = Maxf [Fn (succs x) (Maxf [x]) | x <- minfOf f1] -- Upwards and downwards closure operators: upwards (Minf []) = [] upwards ts@(Minf (t:_)) = t : upwards (ts `meet` succs t) downwards (Maxf []) = [] downwards ts@(Maxf (t:_)) = t : downwards (ts `meet` preds t) elements :: Navigable a => [a] -- enumerate all elements in lattice elements = upwards top