On Mon, Apr 16, 2012 at 4:23 PM, Jonathan S. Shapiro <[email protected]> wrote:
> Your second point reminds me of something that used to bug me about the
> scope of FORALL qualifiers.
>
> When doing something like a collection, you write a bunch of functions, each
> parametric. Each of those type variables ends up in a FORALL qualifier whose
> scope is the definition or declaration.
>
> But you frequently find that there are a bunch of procedures that all go
> together. In effect, these are defining a family of operations on some type.
> From the human perspective, it sometimes feels like we ought to be able to
> state a FORALL qualifier over a set of definitions.
>
> We get the right result without any multi-definition FORALLs; it's just
> sugar. It just struck me as a place where the scoping didn't quite
> correspond to the thing I was trying to "say" (in the sense of
> documentation) with the code.
That's funny, I have the same gripe.
Probably because you only need one quantifier (essentially) with
templates or Java generics.
In principle, you can deal with it without as much sugar by having the
the body of the quantifier be a tuple type, like:
someStuff : forall 'a, {onefn : 'a->'a & anotherfn : 'a->'a->bool & ...}
But for whatever reason, many functional languages don't have the nice
C-style member access operator that would make this convenient.
In a language like BitC, you'd need some way to say that the tuples
are not _actual_ tuples that exist at runtime, just meta-level tuples
for grouping code, just like the quantifier inhabitants are meta-level
(dependent) functions that specialize some code to a type.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
