On 29 July 2013 18:06, Jonathan S. Shapiro <[email protected]> wrote: > 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.
The most obvious way, it seemed, to talk formally about the signature was to use a common language to represent working with typeclasses. If that is System F_c (which seemed a good choice) then any time you've got parametric types or constraints you've got type-level arguments. > At run time, you'll actually be calling a specialization of sort that takes > a single argument: the array. And possibly the OrdDict if you haven't specialised for the particular 'a? > 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. Ok, well now I see where you're coming from. I'll have to see what I can find on the subject (because obviously what I want is not to care about your instance of Ord R). I /don't/ think there is anything interesting about the idea of a default instance. Intuitively, inferring the instance lexically feels like generic functions (in the lisp, not the cli, sense) or extension methods; but I don't think it would be a huge burden to always name them. (Maybe this is just a side-effect of having to write C# and Java for many years?) > 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[] Failures of eta-reduction are a useful litmus test for language features, but there are enough things that break them now that people seem to be ok with it. Several languages have "constructors", or allocation models that violate it. The only such feature I'm slightly comfortable with is codata, because it's a difficult enough problem. > 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. It would be important if you were trying to prove functional correctness - for example, that sortedR really did return an array containing exactly the same integer values in sorted order. It would be dangerous if the sort implementation memo table was keyed on type rather than on the instance, and so you got sortR when you called `sort` with some other instance, inferred or otherwise. >> > 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. I guess that wanting to treat 'a as some uncountable ring is a bit far-fetched, especially if 'a represents some native value. Many operations are not invertible, and there are two additive floating 'identities', to start with. -- 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
