Proposal: Strict types
twhitehead at gmail.com
Mon Feb 21 14:15:38 CET 2011
On February 21, 2011 06:07:19 Roman Leshchinskiy wrote:
> Yes, GHC won't rewrite in this case which is a big problem. The other big
> problem is that strict types have much uglier laws than lazy ones. For
> instance, fst (x,y) = x but strictFst (StrictPair x y) = y `seq` x. Strict
> types lead a lot of seqs which are often quite artificial, disrupt other
> optimisations because of the dependencies they introduce and prevent code
> from becoming dead. In general, there seems to be a big difference between
> "evaluate this now" (which is what strict types do), "it's ok to evaluate
> this now" (which is what's needed for unboxing) and "this is guaranteed to
> be evaluated at this point" (which strict types do, too, and which is
> quite useful).
The "theorems for free" literature does a fairly good job at clarifying how
easy it is for messing with evaluation to break laws (rewrites)
In any event, unless I'm missing something, I believe you've just pointed out
that we are missing one of our three horseman
pseq - "this is guaranteed to be evaluated at this point"
seq - "evaluate this now"
??? - "it's ok to evaluate this now"
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)?
 of the parametricity apocalypse
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Size: 490 bytes
Desc: This is a digitally signed message part.
More information about the Libraries