DDC compiler and effects; better than Haskell? (was Re: [Haskell-cafe] unsafeDestructiveAssign?)

[Conor McBride]

Hi Dan

On 12 Aug 2009, at 22:28, Dan Doel wrote:

> On Wednesday 12 August 2009 10:12:14 am John A. De Goes wrote:
>> I think the point is that a functional language with a built-
>> in effect system that captures the nature of effects is pretty damn
>> cool and eliminates a lot of boilerplate.
>
> It's definitely an interesting direction (possibly even the right  
> one in the
> long run), but it's not without its faults currently (unless things  
> have
> changed since I looked at it).

 From what I've seen, I think we should applaud Ben for
kicking the open here.

Is Haskell over-committed to monads? Does Haskell make
a sufficient distinction between notions of value and
notions of computation in its type system?

> For instance: what effects does disciple support? Mutation and IO?  
> What if I
> want non-determinism, or continuations, etc.? How do I as a user add  
> those
> effects to the effect system, and specify how they should interact  
> with the
> other effects? As far as I know, there aren't yet any provisions for  
> this, so
> presumably you'll end up with effect system for effects supported by  
> the
> compiler, and monads for effects you're writing yourself.
>
> By contrast, monad transformers (for one) let you do the above  
> defining of new
> effects, and specifying how they interact (although they're  
> certainly neither
> perfect, nor completely satisfying theoretically).
>
> Someone will probably eventually create (or already has, and I don't  
> know
> about it) an extensible effect system that would put this objection  
> to rest.
> Until then, you're dealing in trade offs.

It's still very much on the drawing board, but I once
flew a kite called "Frank" which tried to do something
of the sort (http://cs.ioc.ee/efftt/mcbride-slides.pdf).

Frank distinguishes "value types" from "computation
types" very much in the manner of Paul Blain Levy's
call-by-push-value. You make a computation type from
a value type v by attaching a capabilty to it (a
possibly empty set of interfaces which must be
enabled) [i_1,..i_n]v. You make a value type from a
computation type c by suspending it {c}. Expressions
are typed with value components matched up in the usual
way and capabilities checked for inclusion in the ambient
capability. That is, you don't need idiom-brackets
because you're always in them: it's just a question
of which idiom, as tracked by type.

There's a construct to extend the ambient idiom by
providing a "listener" for an interface (subtly
disguised, a homomorphism from the free monad on the
interface to the outer notion of computation).
Listeners can transform the value type of the
computations they interpret: a listener might offer
the "throw" capability to a computation of type t,
and deliver a pure computation of type Maybe t. But
"[Throw]t" and "[]Maybe t" are distinguished, unlike
in Haskell. Moreover {[]t} and t are distinct: the
former is lazy, the latter strict, but there is no
reason why we should ever evaluate a pure thunk
more than once, even if it is forced repeatedly.

I agree with Oleg's remarks, elsewhere in this thread:
there is a middle ground to be found between ML and
Haskell. We should search with open minds.

All the best

Conor