Strictness annotations on type parameters

[Ralf Hinze]

> 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).