[Haskell-cafe] DDC compiler and effects
oleg at okmij.org
oleg at okmij.org
Thu Aug 13 03:54:06 EDT 2009
Combining non-strict evaluation and even laziness (non-strictness plus
sharing) with effects is of course possible. That is the topic of the
ICFP09 paper of Sebastian Fischer et al., which describes the
combination of laziness with non-determinism. The ideas of the paper
have been implemented in a Hackage package and in the embedded
probabilistic DSL Hansei. In the presence of effects, call-by-name is
no longer observationally equivalent to call-by-need: one has to be
explicit what is shared. Curry's call-time-choice seems a good choice:
variables always denote values rather than computations and can be
shared at will (of the run-time system). The language is still
non-strict, and computations whose results are not demanded are not
evaluated and none of their effects are performed.
Since any computable effect can be modeled by delimited control,
call-by-name shift/reset calculi provide general treatment of effects
and non-strictness. Call-by-name delimited control calculi have
been developed by Herbelin (POPL08). A different call-by-name
shift/reset calculus (containing call-by-value calculus as a proper
subset) is described in
http://okmij.org/ftp/Computation/Continuations.html#cbn-shift
The latter, cbn-xi, calculus includes effect sub-typing, which is
common in effect calculi. A call-by-name function whose argument type
is effectful can always be applied to a pure term. A pure term can be
regarded as potentially having any effect. On the other hand, a
function whose argument type is pure can only be applied to a pure
term. The cbn-xi calculus also supports strict functions. Their
argument type is always a pure type and they can be applied to terms
regardless of their effect, because the effect will occur before the
application. Pure functions thus provide a measure of
effect-polymorphism. The cbn-xi and the other CBN calculi with
delimited control are deterministic.
The best application for the cbn-xi calculus I could find was in
linguistics. The calculus was used to represent various effects in
natural language: quantification, binding, raised and in-situ
wh-questions. Importantly, several effects -- several question words,
anaphora with quantification, superiority -- could be represented.
One may view ML and Haskell as occupying two ends of the extreme. ML
assumes any computation to be effectful and every function to have
side effects. Therefore, an ML compiler cannot do optimizations like
reordering (even apply commutative laws where exists), unless it can
examine the source code and prove that computations to reorder are
effect-free. That obviously all but precludes separate compilation;
the only aggressive optimizing ML compiler, MLton, is a whole-program
compiler.
Haskell, on the other hand, assumes every expression pure. Lots
algebraic properties become available and can be exploited, by
compilers and people. Alas, that precludes any effects. Hence monads
were introduced, bringing back control dependencies disguised as a
data dependency. Monadic language forms a restrictive subset of Haskell
(for example, we can't use monadic expressions in guards, `if' and
`case' statements). In the monadic sublanguage, Haskell swings to another
extreme and assumes, like ML, that everything is impure. Thus in an
expression,
do
x <- e1
y <- e2
...
the two binding cannot be commuted, even if e1 and e2 are both
'return'. If the compiler sees the source code of e1 and e2 and is
sufficiently smart to apply monadic laws, the compiler can determine
the two bindings can be reordered. However, if e1 and e2 are defined
in a separate module, I don't think that any existing compiler would
even think about reordering.
Hopefully a system like DDC will find the middle ground.
More information about the Haskell-Cafe
mailing list