2012/1/16 Yin Wang <yinwa...@gmail.com>: >>>> The typical example would be >>>> >>>> instance Eq a => Eq [a] where >>>> [] == [] = True >>>> (a : as) == (b : bs) = a == b && as == bs >>>> _ == _ = False >>> >>> It can handle this case, although it doesn't handle it as a parametric >>> instance. I suspect that we don't need the concept of "parameter >>> instances" at all. We just searches for instances recursively at the >>> call site: >> >> That seems like it could work, but typically, one would like >> termination guarantees for this search, to avoid the type-checker >> getting stuck... > > Good point. Currently I'm guessing that we need to keep a stack of the > traced calls. If a recursive call needs an implicit parameter X which > is matched by one of the functions in the stack, we back up from the > stack and resolve X to the function found on stack.
You may want to look at scala's approach for their implicit arguments. They use a certain to conservatively detect infinite loops during the instance search, but I don't remember the details off hand. While talking about related work, you may also want to take a look at Scala's implicit arguments, GHC implicit arguments and C++ concepts... > >>> foo x = >>> let overload bar (x:Int) = x + 1 >>> in \() -> bar x >>> >>> >>> baz = >>> in foo (1::Int) >>> >>> Even if we have only one definition of "bar" in the program, we should >>> not resolve it to the definition of "bar" inside foo. Because that >>> "bar" is not visible at the call site "foo (1::int)". We should report >>> an error in this case. Think of "bar" as a "typed dynamically scoped >>> variable" helps to justify this decision. >> >> So you're saying that any function that calls an overloaded function >> should always allow its own callers to provide this, even if a correct >> instance is in scope. Would that mean all instances have to be >> resolved from main? This also strikes me as strange, since I gather >> you would get something like "length :: Monoid Int => [a] -> Int", >> which would break if you happen to have a multiplicative monoid in >> scope at the call site? > > If you already have a correct instance in scope, then you should have > no way defining another instance with the same name and type in the > scope as the existing one. This is the case for Haskell. Yes, but different ones may be in scope at different places in the code, right? > But it may be useful to allow nested definitions (using let) to shadow > the existing instances in the outer scope of the overloaded call. I considered something like this for instance arguments in Agda, but it was hard to make the instance resolution deterministic when allowing such a form of prioritisation. The problem occurred if a shadower and shadowee instance had slightly different types, such that only the shadowee was actually type-valid for a certain instance argument. However, the type information which caused the shadower to become invalid only became available late in the type inference process. In such a case, it is necessary to somehow ascertain that the shadower instance is not chosen, but I did not manage to figure out how to get this right. Dominique _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe