[Haskell-cafe] Robert Harper on monads and laziness

[Dominique Devriese]

2011/5/3 Manuel M T Chakravarty <chak at cse.unsw.edu.au>:
> Interestingly, today (at least the academic fraction of) the Haskell
> community appears to hold the purity of the language in higher
> regard than its laziness.

I find Greg Morissett's comment on Lennart Augustsson's article pro
lazy evaluation very interesting:

  http://augustss.blogspot.com/2011/05/more-points-for-lazy-evaluation-in.html#c7969361694724090315

What I find interesting is that he considers (non-)termination an
effect, which Haskell does not manage to control like it does other
types of effects. Dependently typed purely functional languages like
Coq (or Agda if you prefer ;)) do manage to control this (at the cost
of replacing general recursion with structural recursion) and require
you to model non-termination in a monad (or Applicative functor) like
in YNot or Agda's partiality monad (written _⊥) which models just
non-termination.

I have the impression that this separation of the partiality effect
provides a certain independence of evaluation order which neither ML
(because of side-effects) nor Haskell (because of non-strict
semantics) manage to provide. Such an independence seems very useful
for optimization and parallel purposes.

Dominique