RE: Strictness annotations on type parameters

It's not at all easy in general. Suppose we have f :: [!a] -> [a] f xs = xs Does f run down the list, behind the scenes, evaluating each element? That could be expensive. Would it make any difference if we wrote f :: [!a] -> [a], or f :: [a] -> [!a]? Or does the type mean that f *requires* a list with *already-evaluated* elements? 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. Meanwhile, you can easily define your own writeIORef: strictWriteIORef r x = x `seq` writeIORef r x No need to sprinkle seq's everywhere! Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Mario Blazevic | Sent: 06 December 2005 21:06 | To: glasgow-haskell-users@haskell.org | Subject: Strictness annotations on type parameters | | I spent several days last week trying to track a cause of a 100% | slowdown after some trivial changes I made. The profiler didn't show any | slowdown, presumably because it was dependent on optimizations, so I had | to revert to tweak-run-measure cycle. | | It turned out the slowdown was caused by some unevaluated thunks | that were kept around in long-lived IORefs. This is not the first time I | was bitten by too laziness, either. What made things worse this time is | that there is no way do declare the following: | | data Label = LabelRef {labelId:: !Unique, | reference:: (IORef !LabelState), -- illegal | origin:: Maybe !Label} -- illegal | | | No container data type can be annotated as strict. That means I have | to pepper my code with explicit evaluations to HNF before every | writeIORef (reference label): | | newState `seq` writeIORef (reference label) newState | | What is the reason for this restriction on where strictness | annotations can appear? Is it purely an implementation problem or is | there a reason emanating from Haskell design? If former, how hard would | it be to fix? | | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

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

Hello Ralf, Wednesday, December 07, 2005, 12:43:33 PM, you wrote:
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.
RH> Fortunately, it's easy to dry up the `swampy territory'. The type RH> `Contract' below models strictness requirements. The function RH> `assert' implements them (`assert c' is a so-called projection). RH> Feel free to experiment with different designs ... i don't understand anything in what you wrote :) but week or two ago there is a brief discussion in libraries maillist about need of creating strict and lazy variants of libraries, for example for monads and data structures (Maps, Trees and so on). can you say something about automatic generation of strict library from lazy one, or about generating them both from some template? -- Best regards, Bulat mailto:bulatz@HotPOP.com

It's not at all easy in general. Suppose we have
f :: [!a] -> [a] f xs = xs
Does f run down the list, behind the scenes, evaluating each element?
No, because what [!a] means is List !a = ([] | !a : List !a). It does not mean ([] | !(!a : List !a)). Since the Cons thunks are not forced to HNF, the argument type [!a] should mean a lazy list with strict elements. So you would pay the extra expense in a function like length :: [!a] -> Int length [] = 0 length (_:xs) = succ (length xs)
That could be expensive. Would it make any difference if we wrote f :: [!a] -> [a], or f :: [a] -> [!a]? Or does the type mean that f *requires* a list with *already-evaluated* elements?
I don't see it as expensive: the function would do exactly what it's supposed to do, given its declaration. If the declared and inferred types don't match on strictness, the compiler should emit a warning that the declared function type is too strict. As for f :: [a] -> [!a] I'm not sure if this kind of declaration should be treated as a guarantee or an obligation. That is, I'm not sure if the compiler should report an error if the function definition does not actually return a list of elements in HNF, or if it should insert code to force each element to HNF. But I'm mostly concerned about data declarations. See, what bugs me is that it's allowed to declare data Maybe' a = Nothing' | Just' !a data List' a = Nil | Cons' !a (List' a) and then use those to declare data MaybeList1 a = [Maybe' a] data MaybeList2 a = List' (Maybe' a) But now the containers are incompatible mutually and incompatible with [Maybe a]. If strictness annotations were allowed not only at the top level, then [Maybe a], [Maybe !a], [!(Maybe a)], and [!(Maybe !a)] would all be compatible types. And the libraries wouldn't need to provide different version of functions for lazy and strict containers of the same kind.
participants (4)
-
Bulat Ziganshin
-
Mario Blazevic
-
Ralf Hinze
-
Simon Peyton-Jones