LANGUAGE MultiParamTypeClasse TypeFamilies NoMonomorphismRestri ction

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, NoMonomorphismRestriction #-}
import Prelude hiding ((.),id)
import Control.Category
import Control.Monad
import Control.Monad.Identity
import Control.Arrow
import Data.List
data (Monad m) => Hoar m a b = Hoar {
action :: a -> m b,
preconds :: [a -> Bool],
postconds :: [b -> Bool] }
test :: [a -> Bool] -> a -> Bool
test fns x = all id $ ap fns [x]
hoar :: (Monad m) => Hoar m a b -> a -> m b
hoar h x = if test (preconds h) x
then do
y <- (action h) x
if test (postconds h) y
then return y
else fail "Postconditions failed"
else fail "Preconditions failed"
hid :: (Monad m) => Hoar m a a
hid = Hoar (return . id) [] []
instance (Monad m) => Category (Hoar m) where
id = hid
h1 . h2 = Hoar fg (preconds h2) (postconds h1)
where
fg = \x -> do
y <- hoar h2 x
hoar h1 y
instance (Monad m) => Arrow (Hoar m) where
arr f = Hoar (return.f) [] []
first (Hoar f p q) = Hoar f' p' q'
where f' (b,d) = do
y <- f b
return (y,d)
one f = fst.(first f)
p' = map one p
q' = map one q
-------------------------------------------------------------
sorted :: (Ord a) => [a] -> Bool
sorted lst = lst == sort lst
hoarSort :: (Monad m, Ord a) => Hoar m [a] [a]
hoarSort = Hoar {
action = return.sort,
-- action = return,
preconds = [],
postconds = [sorted]
}
main = do
res <- hoar hoarSort [3,2,5,12,1]
print res