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
