The counter-example provided by Matt M leads me to conclude that we need
a general effect typing system, and that this cannot be conveniently
hidden from the user. Without ensuring that initializing expressions are
pure, we cannot ensure causal initialization order, and without that we
don't know that programs are safe.
I think that we should stick with Swaroop's proposed two-valued effect
system, in which the possible concrete values of an effect type are
"pure" (meaning "does not mutate anything that is globally reachable")
and "impure" (meaning "may mutate something that is globally
reachable"). The only alternative that I can really see is to introduce
a full region typing system. That is both more than we need and more
than I think most users can handle. I'm already concerned that the
effect type syntax will prove to be too much.
SYNTAX
Proposed syntax is that we will extend syntax of (fn ...) to be:
([effect] fn ('argType0 .. 'argTypeN) 'returnType)
where "effect" may be:
the keyword "pure"
the keyword "impure"
an effect variable
missing, meaning presumptively impure
So in this system, the preferred typing of MAP and ID are:
map: ('e fn (('e fn ('a) 'b) (list 'a)) (list 'b))
id: (pure fn ('a) 'a)
while the following typings are conservatively correct, backwards
compatible, and clearly not preferred:
map: (fn ((fn ('a) 'b) (list 'a)) (list 'b))
id: (fn ('a) 'a)
QUESTION:
Because effect variables are positionally distinguished, it is not
strictly necessary for them to have a different syntax from type
variables. [Strictly speaking, the syntax wouldn't suffer if type
variables did not have a leading ' either].
It may be better for clarity purposes if we restrict type variables to
the non-extended identifier space (characters, _, and digits in the
usual way) and then state that an effect variable must be written as
something like:
'%e
where the "%" indicates an effect variable. This would give preferred
typings:
map: ('%e fn (('%e fn ('a) 'b) (list 'a)) (list 'b))
id: (pure fn ('a) 'a)
Do people think that something like this would be clearer? If so, is "%"
a good choice?
By the way: I note that we are clearly hitting the limits of the
LISP-style syntax here.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
