It's hard to avoid the feeling that one ought to be able to say something useful about strictness in the types but it's swampy territory, and hard to get right.
Fortunately, it's easy to dry up the `swampy territory'. The type `Contract' below models strictness requirements. The function `assert' implements them (`assert c' is a so-called projection). Feel free to experiment with different designs ...
{-# OPTIONS -fglasgow-exts #-}
infixr :->
data Contract :: * -> * where Id :: Contract a (:->) :: Contract a -> Contract b -> Contract (a -> b) (:=>) :: Contract a -> Contract b -> Contract (a -> b) List :: Contract a -> Contract [a] SList :: Contract a -> Contract [a]
assert :: Contract a -> (a -> a) assert Id = id assert (c1 :-> c2) = \ f -> assert c2 . f . assert c1 assert (c1 :=> c2) = \ f x -> x `seq` (assert c2 . f . assert c1) x assert (List c) = map (assert c) assert (SList c) = \ xs -> eval xs `seq` map (assert c) xs
eval [] = [] eval (a : as) = a `seq` eval as
Some test data.
evens [] = [] evens [a] = [a] evens (a1 : a2 : as) = evens as
assert (Id :-> Id) (const 1) undefined assert (Id :=> Id) (const 1) undefined assert (Id :=> Id) (sum . evens) [1, undefined] assert (SList Id :=> Id) (sum . evens) [1, undefined] Cheers, Ralf PS: Just in case you wonder, the code has been adopted from a recent paper on contracts (see my homepage).