Re: Local evidence and type class instances

On Sat, Oct 16, 2010 at 11:41 AM, Max Bolingbroke wrote:

On 16 October 2010 15:47, Antoine Latter 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.

From the point of view of the down-stream engineer, I feel that first class modules with a module algebra like OCaml would be a lot less mysterious. Once a thing is locally scoped, it's nicer if I can name it and abstract over it in a concrete and reliable way. Keep in mind

that I've never used OCaml's module system. Maybe that's just a lot harder to fit into GHC as it is today, though. But I feel like the problem you're solving has already been solved by first-class modules - type classes are for something else altogether. But maybe we need a better example to argue about :-) Antoine