On Thu, May 2, 2013 at 6:30 PM, Johan Tibell
<johan.tibell@gmail.com> wrote:
- implementing strictness annotations at the type level in Haskell itself*.
* I think this could be one of the most important changes in a long time to help Haskell in the "real world". It gives us a better way to talk about strictness than we have today, reducing time spent on chasing down space leaks. One we have strictness annotations in type, we could experiment with a Strict language pragma to make a whole module call-by-value.
FWIW, have you done any thinking about the "strictness types" part of the whole thing? Has anyone? I'd be quite interested in it if so. I mean "Haskell has problems keeping track of strictness/laziness, Haskell has a great type system => let's put strictness in the type system" seems logical enough, but does it actually work out?
The basic idea -- stick a ! on a type to get a strict version of it -- looks simple, but after trying to think it through further, it doesn't seem as simple as it seems. The main questions/issues I've encountered in my undereducated speculation:
- If `!a` and `a` are completely separate types, you would have to put explicit conversions everywhere, which is unpleasant. If `!a` and `a` are the same type, the compiler can't prevent them from getting mixed up, which is useless. So I think you would want `!a` to be a subtype of `a`: `a` is inhabited by both evaluated and unevaluated values, `!a` only by evaluated ones. Where `a` is expected, `!a` is also accepted. But GHC's type system doesn't have subtyping, for (I'm told) good reasons. Could it, for this specific case?
- As a consequence of the subtype relationship, you would also have to track the co/contra/invariance of type parameters, in order to determine whether `f !a` is a subtype of `f a`, or vice versa.
- If you try to pass an `a` where an `!a` is expected, should it be a type error, or should the compiler automatically insert code to evaluate it? What about `f a` and `f !a`? How could the compiler possibly know how to evaluate the `a`s inside of a structure?
- Strict types in the return type position don't make any sense. This makes taking a value, evaluating it somehow, and then having that fact show up in its type difficult.
- As far as I can tell, "strict types" and "unlifted types" are the same thing. The former is guaranteed to be in WHNF, while the latter is guaranteed not to be bottom. I don't see a difference there. Perhaps the second formulation has seen more research?
Or would it be a different kind of scheme that doesn't rest on `!a` being a subtype of `a`? (Especially the thing with the return types makes me think it might not be the best idea.) But how would it look?