On Wed, Dec 31, 2014 at 9:57 AM, Jonathan S. Shapiro <[email protected]> wrote: > One of the remarkable things about BitC is the number of times I come back > to an issue later and feel like I've missed something obvious. It is > flattering and humbling that so many of you have invested so much time, > effort, humor, and conversation to create these opportunities for me to slap > my forehead and think "Gosh, I'm an idiot!". :-) Thank you! > > I've been thinking about instance coherence again, and re-reading Bruno > Oliveira's paper, and I think I've missed something very basic in the > instance coherence discussion: coherence only matters some of the time. The > catch is to know when you are and are not assuming it. > > Keean Schupke sent me a note earlier today taking a very strong position. In > his view, multiple instances of a type class at a single type is wrong, > because (in his view) a type captures a set of operations. I think this is > consistent with the traditional Haskell view, but I think it has two > probems: > > 1. A type class isn't a type. It's a constraint on a type. It doesn't claim > that the methods are part of the type[s]. It merely says that > implementations of the methods exist that operate over instances of type[s]. > 2. From a purely practical perspective. it's a view that makes retroactive > extension difficult, because it drives us firmly into the instance coherence > checking problem. > > Coherence is good. Coherence lets us justify various forms of context > reduction. From a compilation perspective, it lets us do a whole bunch of > aggressive inlining easily, which is especially important at ground types > and unboxed types. Coherence is really good. > > Coherence is bad. There are useful cases of type classes that say "certain > laws must hold" without requiring that they must hold in a particular way. > E.g. (Ord 'a) captures the [unstated] intention that instances of orderings > be commutative. > > It may be that what *I* think I want shouldn't be called type classes. This > may all come down to lexicon. If I'm not contemplating type classes anymore, > what should these be called (description follows)? > > > So as I say, I've been reading Bruno Oliveira's paper, and I'm coming to > think that we've all had the foot in the wrong shoe for quite some time. I > still have misgivings about implicits as a mechanism for *general* > type-driven value selection, but I'm still chewing on that. The thing that > jumped out at me on this reading - and so far as I can find Bruno never > actually says this in the paper - is that coherence can be viewed as a > property of the *use* of a type class, not a property of a type class, and > that both views can co-exist. > > What I'm suggesting here is that there are two kinds of type constraint > use-occurrences that may appear on a definition: > > 1. Coherent constraint uses. These can only be satisfied by coherent > instances. Coherent instances have a single instantiation at a given type. > They observe the usual context reduction rules. They are known at static > compile time. They can only be resolved [I propose] from lexical contours > chosen to ensure that a failure of uniqueness is detected at static compile > time. Coherent instances may be named, but (by virtue of uniqueness) naming > is not a requirement for a successful language design. Coherent instances > are immodular, because it is required to check against collision. > > 2. Non-coherent constraint uses. These can be satisfied either by coherent > or non-coherent instances. A non-coherent instance may overlap or match a > coherent instance. Both non-coherent constraints and non-coherent instances > must be named. A non-coherent constraint is a named, optional parameter. > Non-coherent constraints are strictly modular. For human consumption, we > might refer to these as "named constraints". > > The proposal is that use of non-coherent constraints in a function is > signaled by a declaration that the constraint is named, which introduces a > formal parameter name. The formal parameter typically is not referenced > within the function. The effect of passing a non-coherent instance is that > its methods become bound in the lexical scope of the procedure. > > The place where this differs from Bruno's type-directed implicit values is > that I'm intentionally restricting these to instance resolution. Ultimately, > I think I could live with type-directed static term resolution (i.e. the > term is statically defined) as opposed to value resolution. I want > desperately to preserve term substitution here, because both coherent and > non-coherent instances are terms, and can therefore be polyinstantiated in > implementations where that is appropriate. But for the moment I'm only > considering this for named constraints. > > I'm not sure that what results here is still type classes, because in this > view (Ord int) can be viewed as a type having multiple possible > instantiations. > > Also, this isn't quite the same as Bruno's implicits, because Bruno's > requirement is only that a unique implicit at the desired type must exist in > the implicit environment. So far as I can tell, that is not enough to > guarantee coherence. > > Yes, for those watching the bouncing ball carefully, this is another > variation on the "literal kind" trick. The trick is readily extended to > [deep] constant terms generally, provided they are statically defined.
What are the types of compiler tricks you're thinking of doing that require coherence type classes? Are you imagining optimizations that are possible to do on a "sort" function that uses type classes but are impossible to do on a "sortBy" function that takes an ordering function explicitly? Most optimizations I can imagine work in both cases modulo heuristics for when partial evaluation should usefully be applied, though of course that's a huge "modulo". Specifically, if you can optimize "sort" for a given type by noticing that it has a coherent type class for Ord, you can also optimize sortBy if you can notice that people seem to pass in the same comparison function *most* of the time. Most is hard, but I'm curious if there are other optimization advantages of coherence that I'm missing. Geoffrey _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
