Lambda the Ultimate

A brief question about effect types, which we are now looking at for BitC in the context of initializers.

My understanding (which could certainly be wrong) is that the experience with effect types in ML (and comparably with region types in Cyclone) was mixed to negative. In ML, Tofte's effect type annotations were confusing enough to users that the value restriction was adopted instead. In Cyclone, it seems clear that users cannot keep track of complicated region annotations. Our hypothesis is that both annotations failed because they were general, and this made them syntactically invasive.

Our main goal in BitC is to be able to distinguish between pure and non-pure expressions in the type system, where "pure" means "expression does not mutate (but can reference) anything that might be reachable from global bindings". This is, in effect, a two-valued effect system in which constraints are defined by MAX. Because the constraints are defined by MAX, it appears to us that we may not need to make effect type variables visible to naive users. In particular, it looks like we end up with two function types:

• Function whose effects we do not care about, because it is not applied in the expression. The type of this can be expressed as (fn (args) result)
• Function whose effects DO matter, because it is applied. The type of this can be expressed as (pure-fn (args) result)

The effect variable is actually being encoded here in the keyword, but we think that representing it this way will not induce the confusion of previous, more general effect type systems.

Further, it looks like we can extend this to cover confinement without undue syntactic complication (confinement: function can mutate its closure, but not things globally reachable), again because the only constraints the emerge in practice are "unconstrained" or "input constraint must not exceed output constraint" and we have pure < deeply-non-mutating < mutating.

Does this seem plausible, or is there some subtyping issue here that will force us to expose the effect variables to the user? If so, we are not seeing it, and I don't want to go jumping off of any cliffs at this point.