<br><br><div class="gmail_quote">On Thu, May 2, 2013 at 6:30 PM, Johan Tibell <span dir="ltr"><<a href="mailto:johan.tibell@gmail.com" target="_blank">johan.tibell@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr"><div><ul><li>implementing strictness annotations at the type level in Haskell itself*.</li></ul><div><br></div><div>* 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.</div>
<div><br></div></div></div></blockquote><div><br></div><div>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?</div>
<div><br></div><div>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:</div>
<div><br></div><div>- 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?</div>
<div><br></div><div> - 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. </div>
<div><br></div><div>- 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?</div>
<div><br></div><div>- 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.</div><div><br></div><div>
- 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?</div>
<div><br></div><div>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?</div>
<div><br></div></div>-- <br>Your ship was destroyed in a monadic eruption.