Well if the two options are a) specify effect variables on all source,
or b) have the analysis in a separate tool, why not consider some middle
ground, like the ability to specify an effect signature separately from
the type signature.
For instance, leverage named function arguments in signatures to
associate region variables with each argument explicitly. Using
Swaroop's example:
define (f fn1 fn2 x)
(f1 x)
(fn2 x)
#t))
f: (forall (('a 'b 'c '%e '%e1 '%e2 ((<= '%e1 '%e) (<= '%e2 '%e)))
('%e (fn (('%e1 (fn ('a) 'b))
('%e2 (fn ('a) 'c))
'a) bool)))
Type signature using OCamlish labelled arguments (sorry, Lispy syntax is
not my forte):
f: fn1:('a -> 'b) -> fn2:('a -> 'c) -> bool
Effect signature specified elsewhere (or inferred if not specified):
effect-sig f%e fn1%e1 fn2%e2
where e1 <= e
where e2 <= e
The compiler obviously needs both to call f, but I'm assuming that the
effects can be fully inferred so most developers need not bother with
them unless they're interested in declaring some property.
Sandro
Jonathan S. Shapiro wrote:
> On Tue, 2008-10-07 at 11:22 -0400, Sandro Magi wrote:
>> I can see the usefulness of having it in the language, since it allows
>> code producers and consumers to state and verify invariants in a more
>> fine-grained manner than is possible via an external tool. Then again,
>> this allocate yes/no invariant is pretty coarse-grained, so that will
>> limit its usefulness.
>
> Exactly.
>
> The advantage of doing this in the type system is that it makes the
> check composable in the presence of separate compilation.
>
> The disadvantage of doing this (or any other effect check) in the type
> system is that it becomes a necessary part of every function type. If we
> put this in the type system, then every function type must now be
> written as:
>
> ('%e '%a fn from-type to-type)
>
> where '%e describes global effect and '%a describes heap effect. What is
> happening here is that a region typing scheme is being introduced one
> special case at a time.
>
> Now there is nothing wrong with that IF the cases are important enough
> to justify the added complication in the specification of function
> types. But the subjective evidence from other languages that *do* have
> effect types is that they very rapidly become an impediment to
> usability, and I am very concerned that this might happen in BitC.
>
> Effects *are* (unfortunately) necessary in order to write correctly
> initializable programs. If that were not true, I would not have included
> them in the type system.
>
> So the question is not whether this check is good and useful. The
> question is whether it is so *overridingly* useful that it should be
> done by the compiler and imposed on every programmer.
>
> One of my tacit assumptions in the design of BitC is that "source
> available" is winning in the world, which makes whole-program checking
> much more feasible. Where this is not true, property transition rules
> for opaque functions can be declared (which is a form of assertion). And
> it is very important to have a tool that can check such properties and
> test such assertions, but that tool may not need to be the everyday
> compiler.
>
> A corollary to this view is that *declaring* properties and their
> checking requirements within the source code is important even when
> those properties cannot be checked during separate compilation.
>
> shap
>
> _______________________________________________
> bitc-dev mailing list
> [email protected]
> http://www.coyotos.org/mailman/listinfo/bitc-dev
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
