[Haskell-cafe] Fwd: Increasing Haskell modularity

[Bertram Felgenhauer]

Gesh wrote:
> On 10/1/2014 10:49 PM, David Menendez wrote:
> >How is that neither here nor there? Haskell says that types belong to
> >classes, and each (type) instance of a class has a specific
> >implementation. The fact that GHC implements this using dictionaries is
> >irrelevant. It’s perfectly valid to implement type classes with partial
> >evaluation, or matching on type parameters, or even C++-style templates.
>
> How is this point relevant? As far as I understand typeclasses enjoy
> three properties: confluence, coherence and global uniqueness.
>
> These are defined as follows:
> * Confluence: Constraint-solving always terminates with the same sets
>               of constraints on terms.
> * Coherence:  The same instance is always chosen for terms.
> * Global uniqueness: For any type and typeclass, there exists at most
>                      one instance of the typeclass for the type.
> 
> What I suggested was to weaken global uniqueness to local uniqueness,
> defined as:
> * Local uniqueness: For any type and typeclass, in any scope there
>                     exists at most one instance of the typeclass for
>                     the type.
> And a scope is a set of parallel bindings, introduced by a module
> declaration, let expression or where clause.
> 
> Since this only affects global uniqueness, I fail to see how concerns
> about coherence being lost are relevant.

I think there are different possible interpretations of coherence in the
absence of global uniqueness. To me, correctness of Data.Set (which your
proposal would break) relies solely on coherence, on the fact that the
comparisons in its various functions always go the same way for any two
given values. Global or local uniqueness should not matter; after all,
the locations of those comparisons do not change. (Actually, ghc falls
short of this ideal, see [1].) Put differently, I view global uniqueness
as an ingredient for ensuring coherence in the case that instance
selection is deferred to the caller.

You seem to take the relaxed view that coherence is already satisfied if
instance selection is deferred to the caller, even if different callers
may select different instances for the same types.

(-1 on the proposal from me.)

Cheers,

Bertram

[1] https://ghc.haskell.org/trac/ghc/ticket/2356