[Haskell-cafe] decoupling type classes

[Dominique Devriese]

2012/1/16 Yin Wang <yinwang0 at 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