
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.
participants (1)
-
oleg@okmij.org