Implementing Strict Core

[Gábor Lehel]

On Thu, May 2, 2013 at 6:30 PM, Johan Tibell <johan.tibell at 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?

-- 
Your ship was destroyed in a monadic eruption.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130507/4b7440a7/attachment.htm>