Local evidence and type class instances

[Max Bolingbroke]

HI Antoine,

I didn't know UHC already had this - thanks for the pointer! It seems
they have read about implicit configurations too, as the example they
use is very similar to the paper.

In fact, they also have another extension to the concept that I was
intentionally avoiding mentioning - they ensure that the lexically
most closely bound instance is used to satisfy a demand for a type
class operation. This means that you can sensibly have local instances
that overlap global ones. I'm not sure how I feel about this feature,
though I certainly see the motivation.

On 16 October 2010 15:47, Antoine Latter <aslatter at gmail.com> wrote:
> Substituting f for f' in this example will change the meaning of the
> operation significantly, which is, in my mind, hard to explain and
> reason about.

That's the behaviour I had in mind. There is no doubt that local
instances are a big complexity increase, but IMHO this behaviour is
relatively easy to reason about as long as you know about the
dictionary passing translation. Indeed, it's practically mandatory to
use dictionary-passing to implement this behaviour. Local instances
would probably never get added to a compiler (like JHC) that doesn't
use that technique.

RE your later point:

> Along similar lines as my last post, would I be able to write the
> following type signature:
>
> myFunct :: Ord Int => Int -> (...)
>
> and have it always use the local instance for Ord Int? Is this the
> type that the type checker would infer for my function?

To my mind, if you have that signature, then myFunct would use
whatever Ord Int instance was available at the use site of myFunct
(i.e. wherever it was mentioned syntactically). It is certainly
interesting to note that adding a context like this might be useful if
you were using local instances.

Cheers,
Max