Proposal: Strict types

[Edward Z. Yang]

Excerpts from Tyson Whitehead's message of Mon Feb 21 08:15:38 -0500 2011:
> Should something be done about this?  I can certainly see how it would be 
> useful information for the compiler wrt to optimization.
> 
> The non-deterministic semantics
> 
> ??? _|_ x -> possibly _|_ or x
> 
> are also pretty interesting.  Very reminiscent of what can happen with 
> rewrites in the presence of the other two.  Could there be something here 
> (i.e., this would allow you to have rewrites that still preserve the semantics 
> as the non-determinism would officially be part of the semantics)?

I don't have very much experience rewrite rules, so I've pushed my thoughts and
opinions to the end of the post.

  * The bog-easy way of pulling this off (from the implementation side) would just
    be "seq", but ignore that it exists when you're performing rewrite rules. [1]

  * You can probably do better if both arguments are guaranteed (by the user)
    to be non-bottom. [2]

There is one essential difference between seq and strict data structures, which
is that we want data going into strict data structures to be known so that
they can be stored unboxed; but if no storage is happening at all, it seems
plausible that in that case we ought not to evaluate them at all.

So it seems to me that once we decide that a structure ought to be unboxed
(strict), then there's no point in applying anymore rewrite rules: we
presumably want the unboxed structure because it's now going to be shipped to
the far ends of the earth, traversed in non-rewritable ways, etc.  So in this
sense, the failure of strict rewrite rules to make sense is sensible.  What we
might want to figure out is if we can make both unboxed and boxed versions of
data structures coexist (the boxed versions for further rewriting, unboxed for
representation), and think about an operator that says, "Yes, now I want this
structure to exist (efficiently) in memory" (and hope that the rewrite rules
up to that point allow GHC to fill out that table directly).  But non-uniform
representations like this could blow up code size and cause its own problems.

Cheers,
Edward

[1] But I don't feel very good about this, since it's basically equivalent to
"yeah, we don't have any semantics about this but it will either be this or
that, depending on what rules fire and which way the wind blows."  Not that
rewrite rules aren't already like that.

[2] But that is very unsafe, and although rewrite rules are
"unsafe", here we've pushed the unsafety in the land of client code.