I want to play with some options here. I think we may feel better about
purity typing if we look at the syntax more carefully.
Consider the effect-annotated type of map:
map: (forall (('%e1 <= '%e2))
(%e2 fn ((%e1 fn ('a) 'b) (list 'a)) (list 'b)))
This is horrible, god-awful, unreadable mess, and it only has one effect
property! But I'm beginning to think that the real problem here is
mostly the syntax of FN types, and not so much the syntax of effect type
variables. Let's play some games here:
1. Re-syntax (%e fn ('a 'b) 'c) as (%e fn 'a 'b -> 'c):
map: (forall (('%e1 <= %e2))
(%e2 fn (%e1 fn 'a -> 'b) (list 'a) -> (list 'b)))
2. Re-introduce names (optionally) into function types that let us hang
labels on parameter and return types:
map: (forall (('%e1 <= %e2))
(%e2 fn f:(%e1 fn 'a -> 'b) ls:(list 'a) -> (list 'b)))
3. Remove the effect variables:
Notice that the effect variables, where they appear, are now entirely
redundant. They can be subsumed by stating that "%x is the effect
variable associated with the parameter named x":
map: (forall ((%f <= %map))
(fn f:(fn 'a -> 'b) ls:(list 'a) -> (list 'b)))
this may be clearer if the overall function label is moved inside the
forall:
(forall ((%f <= %map))
map: (fn f:(fn 'a -> 'b) ls:(list 'a) -> (list 'b))
this also nests, because if f in turn has a procedure argument g, we
can label that one "f.g"
The win here is that we have converted very confusing variable names
whose relevance is not immediately apparent (the effect variables)
into names.
And finally, we can generalize this over effects other than purity by
attaching a label to the constraint set:
(forall ((purity %f <= %map)
(noalloc %f <= %map))
map: (fn f:(fn 'a -> 'b) ls:(list 'a) -> (list 'b))
Please note that I'm not proposing to re-inject NOALLOC analysis here.
I'm merely pointing out that we didn't lose any ability to generalize to
multiple properties by this re-syntaxing.
I personally believe that this rewrite is very nearly as readable as any
other function type constraint.
What do people think?
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
