My biggest weakness as a researcher is that I am terrible at formal math. I tend to think about implementation first and formalize second (if at all). One reason that I like working with Swaroop and Scott is that both of them are better formal mathematicians than I am, and both of them can occasionally reduce my gibberish to something formal that we can then look at.
In the post at: http://www.bitc-lang.org/pipermail/bitc-dev/2008-August/001190.html I set forth a set of ad-hoc informal rules for pure expressions and pure functions. What these rules actually accomplish (though I may not have gotten them right) is a special case of region and effect typing. Swaroop pointed this out to me, and (as he often does) forced me to re-think my biases. My original inclination was to strongly avoid effect typing, because it has been fairly troublesome in other languages. The annotations rapidly become cumbersome and unusable. In such systems generally, any expression e has two type-like attributes: its type an effect type describing the different regions that evaluating the expression will mutate. But it turns out that the *reason* this has been so troublesome in other languages is that other languages have attempted to do effect typing generally rather than effect typing for only the two regions {global, non-global}. If we reduce our scope of interest to global/non-global, things become much more user friendly. EFFECT TYPING FOR PURE EXPRESSIONS In this scheme, we are going to associate both a type and an "effect" with every expression "expr", so we will have: expr : {E T} I will use brackets here for illustrative purposes. We're going to be able to drop the E from the syntax later, so this will all eventually disappear. We will allow E to take on three possible values: 0: Evaluation of the expression DOES NOT modify global state. It *may* modify purely local state. 1: evaluation of the expression DOES modify global state `e: evaluation of the expression may or may not modify global state, depending on how `e gets computed. We will (temporarily) annotate function types as: (fn E (arg-types) return-type) where each function is decorated with an effect. The effect of a function F is the MAX of the effects of the expressions evaluated within its body. The effect of an application is the MAX of its constituent sub-expressions and the effect of the applied procedure. Thus in MAP: (define (map f l) (case tmp l (nil nil) (cons (cons (f tmp.car) (map f tmp.cdr))))) We would get an effect-annotated typing: (fn `e1 ( (fn `e2 ( 'a ) 'b) (list 'a) ) (list 'b)) `e1 == max(`e2) == `e2 So first, the effect algebra here all works out straightforwardly, and second, any effect variable that does not appear within the MAX is a "don't care". Because the effect variable system is two-valued, the max isn't actually very interesting. This lets us express this to humans as: map: (pure-fn ((pure-fn ('a) 'b) (list 'a)) (list 'b)) meaning "map is as pure as f is pure". The key observation here is that satisfying the "is-pure" predicate can only expose two restrictions on inputs. The first is "don't care", and the second is "must be pure". In consequence, it isn't necessary to write down the effect variables for user consumption. This is also enough to introduce a new form (PURE e) in which we state affirmatively that evaluation of e must not mutate global state. EFFECT TYPING FOR DEEPLY NON-MUTATING EXPRESSIONS One missing feature in BitC is E's notion of deeply non-mutating expressions. In abstract, we could extend the effect system above to a tri-valued system: 0: shallow local side-effects only 1: shallow side-effects on closure plus shallow local side effects 2: side-effects on global state or non-shallow side effects and we could once again introduce a form (DEEPLY-NON-MUTATING e). Once again, because of the way the constraints work out, it will not be necessary to expose the effect variables to the user. The reason is that we have a strict hierarchy here in which: All pure expressions are deeply non mutating expressions All deeply non mutating expressions are expressions Further, because the effect combination criteria is MAX, it is the case that max(`e1 .. `e2) <= x |= `e1 <= x AND `e2 <= x that is, we will never see a tighter input constraint than the output constraint. I am not convinced that we wish to implement the E-style "deeply non mutating" constraint. What I am trying to point out here is that if we wish to introduce it in the future, it will not cause a horrible syntax problem to do so. shap _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
