On Tue, May 7, 2013 at 1:00 PM, Gábor Lehel <illissius@gmail.com> wrote:
On Tue, May 7, 2013 at 6:38 PM, Johan Tibell <johan.tibell@gmail.com> wrote:
`a` and `!a` are compatible types. The compiler will insert the `seq`s where needed. I don't think this is useless.

First, it serves as good documentation. Documenting strictness properties, e.g. as we do in the container library today, is awkward. Strictness annotations on types would make the documentation precise and succinct.

Second, it's a bit more declarative than having put manually put bang patterns at the right places in the function definition and having to remember (and teach beginners) how to do that correctly..

Third, it might help use generate better code, especially if we also implement Strict Core.

Right. I completely agree. The idea is attractive to me for the same reasons. My questions basically relate to: how would you implement it?

A function:

    f :: !a -> ...

would be implemented as

    f !x = ...

i.e. the body of x would start with a `seq` of `x`.

I we had Strict Core we could do better and instead demand that the caller does the evaluation, removing cases of duplicate reevaluation and perhaps expose more unboxing.

 
Right now GHC's type checker works by solving type equality constraints. Type equality is symmetric, and implies that the two types are substitutable for each other in all contexts: there's no concept of "mixing them up", because there's nothing to get mixed up, they are the same. But `a` and `!a` aren't like that. You very much want to avoid mixing them up, so you can insert `seq`s in the right places. But how would that mesh with the present system?

I honestly don't know. Possibly we could just erase the strictness annotations after we have annotated `f` as being strict in its first argument.
 
Would you allow strictness annotations on type arguments in arbitrary positions ([!Int] and so forth)? That leads to the issues regarding "how could the compiler know how to strict-ify arbitrary types", and/or co/contra/invariance of type parameters.

My current thinking is that we would only allow `!` at the "top-level". Even if we defined a meaning for e.g. `f !a`, I don't know if it would be very useful as we wouldn't be able to say things about specific fields. For example, given

    data T a = C a a

should `T !a` mean that both fields are strict? What if we only want one to be strict? What if the type is opaque to the user, how is he/she supposed to know what `T !a` means without referring to implementation details? I believe Scala has the same restriction.

The only thing I would regret if `!` is only allowed at the top-level is that we couldn't reuse e.g. Haskell pairs for both lazy and strict pairs, which would be neat.
 
Looks like it's the reverse actually: http://stackoverflow.com/a/6297 using466

I might have used the word "analogous" incorrectly. I meant: similar to what Scala does, except that Scala is strict by-default and adds by-name parameters through annotations.

-- Johan