On 29 July 2013 01:42, David Jeske <[email protected]> wrote: > On Sun, Jul 28, 2013 at 8:22 AM, William ML Leslie > <[email protected]> wrote: >> >> Ack. You were talking about module boundaries, which is not what I >> was talking about at all. I clearly no longer function at 1 AM. > > > Correct, we are talking about resolving ordR across module boundaries after > run-time late-binding.
You said: On 28 July 2013 14:13, David Jeske <[email protected]> wrote: > Looking at it in this explicit way, and thinking about Agda's implicit > instance arguments, I wonder about another possible approach.. > > Has there been any look at causing typeclass-instance selection to be > implicitly lexically scoped in the caller? > > Explained by way of mechanism... the declaration and use of the typeclass > including Ord could tell the compiler to implicitly add the trait-instance > as an argument to the function and all functions which call the function to > the module boundary. "Add the trait-instance as an argument ... to the module boundary". When I went back and read that (at the end), I thought you meant that a module that selects an instance for a given type should be parametrised by that instance, if the selection isn't local. Which is a very nice idea, I think. Having lots of parameters on your modules feels like E to me. And if you know how module parameters propagate to their functions in Agda, you can understand why I suddenly went "ok, I've completely missed your point." But I think I was almost right. I assumed that you meant that if a function is parametrised over a type and it (eventually) calls something that casts it to an instance, the function should be parametrised over the instance. (presumably, its caller will have to infer it and provide it.) But this is obvious, because there is nobody else who can infer it: for example, in Haskell implementations, the instance dict would be passed at every call that both touched 'a and expected to use it as an Ord. The base case is someone who has the concrete type and so can actually give you the instance. I don't think I know what the word 'including' means here, though. Anyway! I think that the module boundary is irrelevant except in the case that we've already discussed extensively: that calling the parametric sort only resolves to the sort with the orphan instance when the caller also provides (perhaps implicitly) that exact same instance, not the same concrete type. From the perspective of somebody calling into the module you're currently writing, if they give you a type variable for 'a then they also have to be parametric in the selected instance. There's no magic that can be done at the module level, and nothing to be gained by treating it specially. > "Most languages" with this interface concept require interfaces > implementations to be defined in the object implementation. Once we allow > orphaned instances of the interface to be defined outside the object and > apply to the object after-the-fact, we run into a collision problem where > there can be more than one instance of an interface. (more than one > implementation trait OrdR) > > In this situation, we need a clear mechanism for sortR to decide which OrdR > implementation to use, because object-instance->ord-trait is insufficient to > decide between them. Here are some options sortR can use: The moment you talk about orphaned instances, you're talking about inferring the instance. I was really talking about /who/ infers the instance: it has to be somebody who knows that the type has an instance, and they do this by providing the instance. How (indeed, if) they infer it is a different matter, but it still is an interesting problem. -- 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
