I don't know any way to make a compositional story about nested ! annotations in types. As various of you have pointed out, it looks attractive and then runs out of steam.
Putting !'s on data constructor arguments works because it's not really part of the type at all; rather, it just says "give this contstructor a wrapper that makes it strict". I think one could make a similar story for functions in general, so that
f :: !a -> a -> ![a] -> Int
f a b c = e
would mean "add a wrapper to f that makes it strict"; thus
f a b c = a `seq` c `seq` e
But it's not at all clear that this is worth the fuss.
Strict Core is another matter. As the paper says, it's an intermediate language that exposes more about what is evaluated and what is not, and how functions are curried. As I said in an earlier reply, it would certainly be an interesting experiment to make GHC's intermediate language be Strict Core, but it would not be a routine exercise. Fun to be had!
Simon
From: Johan Tibell [mailto:johan.tibell@gmail.com]
Sent: 07 May 2013 21:33
To: Gábor Lehel
Cc: Simon Peyton-Jones; Max Bolingbroke; ghc-devs@haskell.org
Subject: Re: Implementing Strict Core
On Tue, May 7, 2013 at 1:00 PM, Gábor Lehel mailto:illissius@gmail.com> wrote:
On Tue, May 7, 2013 at 6:38 PM, Johan Tibell mailto: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 using466http://stackoverflow.com/a/6297466
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
