A Question Concerning Effect Types

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.

For first-order programs...

...this will work fine. However, the absence of effect polymorphism will get highly annoying when you start looking at higher order functions. map illustrates this well:

  val map : (a -> b) -> (list a -> list b)

  fun map f []        = []
    | map f (x :: xs) = (f x) :: (map f xs)

Now, in this program, if the f argument is pure, then the returned function value is pure, and if f is impure, then the return function value is impure.

So if you want to seriously use higher-order functions, you'll need some effect polymorphism:

  (* Let -> be the pure arrow, and ~> be the impure arrow. *)

  (* map's type quantifies over the function space constructor *)

  map : forall => : arrow. (a => b) -> (list a => list b)

  ...

This ought to be fairly straightforward to typecheck, since you only have two kinds of function arrow, and so quantification is just a matter of typing the body under both possibilities. I don't know if it's too complex for your application, though.

By neelk at Tue, 2008-08-05 21:18 | login or register to post comments

My post wasn't clear.

We clearly need effect polymorphism, and I agree that there is no difficulty in type checking any of this. My question concerns the syntactic complexity of representing those types to the human user. Our provisional belief is that because the effect is two-valued and determined by MAX we don't appear to need the syntax of explicitly written effect variables in either input or output. Translating your example into BitC, MAP types as:

map: (pure-fn ((pure-fn 'a 'b) (list 'a)) (list 'b))

with the meaning: "map is a pure function exactly if its argument function is a pure function".

A procedure not-map that accepts and applies a first function and accepts but does not apply a second function types as:

not-map: (pure-fn (first:(pure-fn ('a) 'b) second:(fn ('a) 'b)) ret-type)

with the meaning: "not-map is a pure function if its first function parameter is pure, and does not care whether its second function is pure".

The effect types are here. They simply aren't rendered explicitly at the user interface because the MAX-nature of the constraint means that no new information can be presented to the user by naming the effect variables explicitly.

Hopefully the question is now clearer: can we get away with this simplification at the user interface without any important loss of information?

By shap at Tue, 2008-08-05 21:50 | login or register to post comments

Counterexample?

foo :: (Int->Int) -> ((Int->Int) -> Int, (Int->Int) -> Int)
foo f = (g, h) where
   g i = i 2 -- g is a pure function
   h i = f (i 2) -- h is a pure function if f was

How would you type this?

By Matt M at Tue, 2008-08-05 23:37 | login or register to post comments

Distilled

f: pure-fn (pure-fn int int) (pure-fn int int)

If you supply an impure function to f, which of the following happens?
- Side effects are produced, and the result is pure
- Side effects are produced, and the result is impure
- No side effects are produced, and the result is impure

The scheme doesn't seem to be able to distinguish these cases, since it doesn't link the pure modifier on the parameter to which of the other pure modifiers rely on it.

By Matt M at Wed, 2008-08-06 02:37 | login or register to post comments

Good counterexample

Excellent counter-example. The issue here is not whether foo is pure, but whether the purity of f gets lost. We don't actually need to apply f here. The following is also sufficient and in some ways more problematic:

(define (foo f)

  (g i)

  (pair g f))

Without explicit effect variables, we can determine that foo is pure exactly if g is, but we cannot determine whether the purity of (foo f) depends on the purity of f. Your counter-example seems to be saying the same thing. I think that my syntactic simplification is still okay when the return value effects are all independent of the argument effects, but at that point it's a special enough case to not be worthwhile.

Thank you. As I said, the purpose of the question was to avoid a potential rat hole, and you just helped us avoid it. I really should have seen this one coming.

By shap at Wed, 2008-08-06 15:01 | login or register to post comments

Lambda the Ultimate

User login

Navigation