[Haskell-cafe] decoupling type classes

[Yin Wang]

On Sat, Jan 14, 2012 at 2:38 PM, Dominique Devriese
<dominique.devriese at cs.kuleuven.be> wrote:
>> I may or may not have thought about it. Maybe you can give an example
>> of parametric instances where there could be problems, so that I can
>> figure out whether my system works on the example or not.
>
> 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:

1. If "g" has an implicit parameter "f", search for values which
matches the name and instantiated type in the current scope.

2. If a value is found, use it as the argument.

3. Check if the value is a function with implicit parameters, if so,
search for values that matches the name and type of the implicit
parameters.

4. Do this recursively until no more arguments contain implicit parameters.


> This coupling you talk about is not actually there for instance
> arguments. Instance arguments are perfectly usable without records.
> There is some special support for automatically constructing record
> projections with instance arguments though.

Cool. So it seems to be close to what I had in mind.


> I am not sure about the exact workings of your system, but I want to
> point out that alternative choices can be made about the workings of
> inferencing and resolving type-class instances such that local
> instances can be allowed. For example, in Agda, we do not infer
> instance arguments and we give an error in case of ambiguity, but
> because of this, we can allow local instances...

Certainly it should report error when there are ambiguities, but
sometimes it should report an error even there is only one value that
matches the name and type. For example,

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.