Just some random thoughts on this... firstly a lot of those things can be inferred. As long as primitives express their effects, the effects of a function can be inferred. PureScript seems to have a good effect system. All it requires is the addition of row-types to the type system, and then the whole effect system just becomes a row-polymorphic monad.
I was thinking about linear types rather than region types, and would be interested in your thoughts on this. I haven't given much thought to mutability annotations, but is seems this should be reflected in the type. Locks probably should be an effect (they are essentially a unique resource, IE a resource that only one thread can hold at a time). As for complexity, the type system should be as simple as possible to give the required functionality. For me this means as few weird special cases as possible. For example treating effects as a row-polymorphic monad seems better than introducing a new mechanism for them. Keean. On 9 January 2015 at 07:33, Jonathan S. Shapiro <[email protected]> wrote: > On Thu, Jan 8, 2015 at 11:26 AM, Raoul Duke <[email protected]> wrote: > >> I appreciate type systems. I appreciate advanced type systems. But >> Scala's usability is just, in my mind, a complete indictment of the >> direction it has gone. I know this stuff is really hard to deal with >> and manage. Does anybody have a sense yet of where Bit-C will end up >> on the usability spectrum? :-) > > > Yes and no. > > For the most part, BitC v0 syntax felt (at least to me) pretty comparable > to Haskell. In my view it may even have been cleaner in one or two places, > but that probably reflects my personal sense of taste a lot more than > anything else, so others might very reasonably disagree. > > For the most part, I see no reason why BitC types should feel any more > syntactically burdened than Haskell types. We'll be adding some "core" > constraints that Haskell doesn't have (type equality, subtypes), but those > don't weigh heavily from the standpoint of notation. > > There are four things I am playing with that *will* add weight, and I > consider this somewhat unfortunate. The first is region types. The second > is effect types. The third is mutability annotation. The fourth is lock > label annotations. Let me take them in turn. > > *Region Types* > > The problem with region types from a usability standpoint is that the add > a lot of annotation burden, usually for little gain. > > *Local* (intra-procedural) region inference can be done without > annotations at all, and helps us in various ways, but because it can be > inferred it presents no annotation burden. The user is *free* to > annotate, but they are not *requred* to annotate. > > I expect that there will prove to be a body of programmers who would > prefer to treat BitC as a conventional GC'd language, who will choose to > ignore regions entirely. I provisionally believe that the defaulting policy > for regions that was adopted for Cyclone should work well for this. In the > absence of a region-annotated function signature, Cyclone proceeds as > follows: > > - each reference argument is given a fresh region variable > - returned references are assumed to be in the heap. > > All such procedures are region-polymorphic. We will undoubtedly discover > region constraints through inference in some cases that will want to be > added to the signature. > > The more complicated cases are the ones where a function returns a > reference to one of its arguments, and also the ones where a function is > specifically intended to allocate within a designated region. Though both > of these require annotation, the first is relatively rare and the second is > a case where the user is making intentional use of the region system. When > the use is intentional, I suspect the annotation required will not be > perceived as a burden. > > We'll also need to come up with a suitable default for by-reference > parameters, but I think that shouldn't be hard. > > So in general, I think the marginal burden of regions is likely to be > tolerable. > > *Effect Types* > > This has been discussed here before. For "binary" effects (alloc vs > noalloc), it usually turns out that the presence of an annotation indicates > the absence of some undesired behavior. This generally means that the > effect annotation can be omitted unless the user actually *cares* about > that effect. In situations where people care, yes, I think effect > annotations could well get out of hand for precisely the same reason that > explicit exception annotations get out of hand. > > Things get trickier if we permit user-defined effects, because it's hard > to know how lexical scoping should work for these. It may prove that we > need to restrict user-defined effects to binary effects precisely because > oblivious client code (i.e. written without knowledge of some effect) needs > to be able to call effect-aware code. > > I don't really think I understand this issue yet. I *do* think that for > the compiler-supported effects they should be completely inferable, and we > can imagine a tool to erase them and re-insert them correctly. > > Because users can write effect-oblivious code, I think this mainly becomes > an annotation burden at library boundaries, and probably not a bad one. The > effects we are mainly concerned with so far seem to be "pure" and "noalloc". > > I think that these can be handled with attribute annotations, provided we > adopt an attribute model that is somewhat richer than the one adopted for > CLI. I don't recall if the attributes themselves were insufficiently > expressive or if was merely that some things you needed to annotated > couldn't be. > > > *Mutability Annotations* > > I've talked briefly about the possibility that different sub-parts of a > data structure might have different mutability properties, and that it > might be useful for these to be parametric. To be perfectly honest, I'm not > sure that will turn out to be worth the bother. I think there is a pretty > clear case for immutable data structures, and I think there is a pretty > clear case for mutable data structures. > > I have made an argument for something like "readonly list of mutable > things", but the rationale for this mainly had to do with termination > arguments, and we don't have an immediate story for a proof system for > BitC. I'm thinking that there are several alternatives to consider on > grounds of simplicity: > > 1. Allow a readonly field annotation. That covers about 90% of the cases > of immediate interest. > 2. Allow types to be defined as "readonly" which means that it is > immutable except where it is parametric. This would certainly handle the > list length case. > 3. Allow types to be defined as "pure", which means that instances are > immutable and further requires that arguments to constructors must be pure. > 4. Introduce the notion that a *region* may be readonly or mutable, and > that the "stack" of regions is really a stack of region pairs (one > readonly, one readwrite). Allow a mutability annotation on region variables. > > The first option is orthogonal to the rest. The second option is really a > shorthand in which all fields are marked "readonly". The third option may > or may not be useful in practice - it becomes a question of idiom, and it > depends on whether we can infer that. The fourth option is perhaps the only > one that's really interesting, and it only needs to be used in the rare > cases where people care. > > It also strikes me that with the introduction of type-level computation > there are other ways to get termination concerns encoded. > > *Lock Label Anntations* > > Lock labeling is an underdeveloped idea I have for annotating which locks > go with which fields. The most common pattern for locks will very likely > remain "per object locks". Fields governed by that lock require no > annotation. Fields governed by some other lock *do* need annotations. But > this case is rare, and in the situation where you need it it really isn't > optional. > > The general idea is to make it possible for the compiler (or some tool) to > confirm that the lock or other exclusion mechanism you require has actually > been obtained before reading or writing a thing. > > I suspect this one could be handled with attribute annotations if we were > so inclined. > > > > So. I'm not at all sure that I have answered your question, but at least > this gives us a place to start. > > > 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
