DDC (http://www.haskell.org/haskellwiki/DDC) uses a similar scheme,
where they optionally annotate the arrows:
For instance, the map function:
map :: (a -> b) -> [a] -> [b]
map f [] = []
map f (x : xs) = f x : map f xs
Gives the following complete type:
map :: forall a b %r0 %r1 !e0 $c0
. (a -(!e0 $c0)> b) -> List %r0 a -(!e1 $c1)> List %r1 b
:- !e1 = !{ !Read %r0; !e0 }
, $c1 = f : $c0
Here, !eN refers to the effect type and $cN refers to the closure
information.
PKE.
Sandro Magi wrote:
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
bitc-dev@coyotos.org
http://www.coyotos.org/mailman/listinfo/bitc-dev
_______________________________________________
bitc-dev mailing list
bitc-dev@coyotos.org
http://www.coyotos.org/mailman/listinfo/bitc-dev
--
Pål-Kristian Engstad ([EMAIL PROTECTED]),
Lead Graphics & Engine Programmer,
Naughty Dog, Inc., 1601 Cloverfield Blvd, 6000 North,
Santa Monica, CA 90404, USA. Ph.: (310) 633-9112.
"It is better to have 100 functions operate on one data structure
than 10 functions [each operate] on 10 data structures." -- NN
|
