Strictness annotations on type parameters

[Mario Blazevic]

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