I certainly think the semantics that you are describing are what I understand and what I feel is The Right Way, but I think that we've made it out to be more complicated than it really is. The first problem is that we're talking both about inferring the typeclass for a particular type, and to what extent a provided (or inferred) instance is used.
To show what I'm uncomfortable about, I'll use the signature you provided. I /think/ there are five arguments to the sort function, several of which are present only for typing. These are: 0. The element type. 1. The Ord instance that will operate on the element type. 2. The coercion (~) from the element type to the typeclass. 3. The length of the array. 4. The array itself. > sort :: Ord 'a => 'a[] -> 'a[] > sortR :: Ord R = OrphanedInstanceForR => R[] -> R[] How does this syntax desugar into System F_c? I read - perhaps incorrectly - that you've combined arguments 1 and 2 into a single coercion, between the applied typeclass and its instance. But constraints are type-level, and the instance passed is value-level, even if the function is specialised on that value. Now, I'm not trying to say that there is difficulty in dealing with such a representation, because you can either pattern match to get the instance out, or linearise the arguments. That much looks like a solved problem. But when we stop thinking about these as distinct arguments, we really do confuse two things. The constraint in the type of sortR looks like it serves two purposes. One is documentation: this named instantiation of sort is the one applied to this instance. Named or not, that is a useful thing to record somewhere. Maybe in some sort of memo table. The other one has to do with the specific mention that the instance is Orphaned, which seems like a hint that we're going to be talking about /inferring/ the class again, and this is a different subject. And so now we come to what I really want to discuss: On 27 July 2013 00:33, Jonathan S. Shapiro <[email protected]> wrote: > If a type instantiation doesn't cross an assembly boundary, then the type > and it's automatic instance resolution decisions are private decisions > within the assembly. The reason I emphasize "instantiation" in that sentence > is that your assembly and mine might use the same type and get different > resolutions. In the sortR example, the instantiation doesn't cross an assembly boundary, because by instantiating sort with a given type you've had to provide proof that the type has an instance of Ord by supplying that instance. The choice of instance needs to appear within the memo table, but what purpose does it serve in the type of sortR? Can I use sortR without any concern about what instances are floating around in my lexical environment, or will it fail to typecheck if I've defined my own ordR? What is in a name? > Now we're going to sum the elements, which are of type T. And I'm going to > be very careful about how I do it: > > let sum = a[0]; > for (i = 1; i < a.length; i++) > sum = sum + a[i]; > > > Note that sum does not initialize to zero! This is true because (a) the > array may not contain numbers, and (b) it avoids any type unification > between the element type 'a and the index type int. And just as a side note, > the fact that I have to be careful about how to write this illustrates how > obscure these cases are. You've ignored the case where the length may be zero (: if you've got an argument that names your instance, you can use methods without needing to provide a value: arraySum : {t : Type} → {{b : Arith t}} → {n : ℤ} → t[n] → t arraySum {{bruno}} xs = foldl (+) (bruno.zero) xs I think you can understand why I like keeping the argument telescope linear. -- William Leslie Notice: Likely much of this email is, by the nature of copyright, covered under copyright law. You absolutely may reproduce any part of it in accordance with the copyright law of the nation you are reading this in. Any attempt to deny you those rights would be illegal without prior contractual agreement. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
