On Sat, Jul 27, 2013 at 6:08 PM, William ML Leslie < [email protected]> wrote:
> 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. > I don't think so. Types are never arguments, automatic instances are never arguments, and the length of an array is part of its type, either by virtue of NAT kind or (in the case of vector) by virtue of the design of the type. And I'm not sure why there is any sort of coercion in here at all. At run time, you'll actually be calling a specialization of sort that takes a single argument: the array. > > > 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. > No instance is passed. The reason that the orphaned selection has to be documented at the type is that the sortR function has been pre-specialized to use that instance internally. Note that instances live in a funny place. Because they are compile-time constant, they can be viewed as literals, or they can be viewed as types where the type class is their kind. Which, I grant, is a very odd way to look at them, but I think it's relevant for the translation into System F_c that you are trying to perform. > 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. > Conceptually, the selection of instance should be documented in every case. But when the instance selected satisfies the "cT or cR or prologue" rule, everybody knows where to look for it, and we can say "in the absence of a named resolution, we understand it to mean that the type class was resolved using whatever instance was appropriate under the "cT or cR or prologue" rule. That is: we're dropping the annotation purely as a relief on the poor user's eyes. Logically it is still present. I have a memory that when two sides of a procedure call disagree about the default instance, soundness problems can arise. That is: the consequences of instance incoherence are worse than just awkwardness and incomprehensibility. This is why it is so important, when the two sides might disagree, to make it possible for them to check. Unfortunately I can't reconstruct the bad example, and I can't remember which paper raised the issue. > > 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? > I think you are saying that if I had written sortR as: function sortR ar : int[] is sort ar then we would get sortR :: int[] -> int[] as the type. Which is actually pretty unfortunate, because in the process we have lost the fact that sortR uses a "perverse" sorting operator. Because of the presence of the perverse resolution, I would actually prefer to have the requirement that the perverse resolution remain documented in the type. For intra-crate calls, it won't matter, because everyone is operating in the same instance environment and will necessarily get the same answer for the resolution. For cross-crate calls, however, I think it's important for the perverse resolution to remain attached to the type. But I also think that the ability to bind and pass instances explicitly becomes important here, and that the issue of documentation only applies to implicit resolutions. So if we had a function sortUsing that takes an explicit instance as an argument, and we then define // In this one, the perverse resolution rises into // the type, because it is implicitly resolved: function sortR ar : int[] is sortUsing (Ord int) ar // In this one it doesn't, because the resolution // is explicit: function sortR ar : int[] is sortUsing PerverseOrdInt ar 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? > If you defined your own ordR and made it an automatic resolution, and you make a call to sortR, it should fail to type check. The two names don't collide; of necessity they have different fully qualified names. > > > 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 (: Indeed I had. Nice catch. Except that I don't know how to define the sum of zero elements. Though you do raise an interesting point that perhaps Arith 'a should depend on Peano 'a, by virtue of which a notion of "zeroness" for 'a is required to be defined. But even if I had that I'm actually not sure how a sum of no elements should be defined. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
