Are there viable and type safe alternatives to the 1:1 type/type-class-instance relation?

Question

This question originally arose during my work on a dynamic JS type validator that relies on dictionary passing style as a rather simple type class mechanism, but I think it also applies to Haskell or other languages having a type class mechanism.

At first I figured it wouldn't be too big a problem to allow several type class instances per type in a setting with dictionary passing style, because I have full control of the type class resolution. But the actual issue seems to maintain type safety not type class resolution, as I am going to demonstrate using the type validator. Since the code is type annotated it is language agnostic to some extend.

// please assume `Number` to be a non-polymorphic `Int` type

Sum.Monoid                          // Monoid<Number>
Prod.Monoid                         // Monoid<Number>
Function.Monoid                     // Monoid<b> -> Monoid<(a -> b)>
Function.Monoid(Prod.Monoid)        // Monoid<(a -> Number)>
Function.Monoid(Prod.Monoid).append // (a -> Number) -> (a -> Number) -> a -> Number

When you apply these types type safety is compromized, because it is possible to just write the following contrieved expression without the validator complaining:

Function.Monoid(Prod.Monoid)
  .append(inc) (inc) (Sum.Monoid.empty); // yields 1 ((0 + 1) * (0 + 1)) instead of 4 ((1 + 1) * (1 + 1))

In Haskell each instance has its own distinct type to prevent such nonsensical expressions. But having to convert from one type-wrapper to another can be tedious.

Is there a viable, type-safe alternative or is this the very reason why Haskell's designers chose the distinct-type-per-class-instance simplification?

Answer 1

Perhaps one possibility would be to have some sort of scoped instance mechanism. Sort of half-baked, but imagine writing something like this:

with Prod.Monoid, Function.Monoid {
    append(inc)(inc)(empty)
}

(Say with X, Y, Z {e} is short for with X {with Y {with Z {e}}}.) Presumably it would then be an error to introduce a second instance for a given class/type pair within that scope:

with Prod.Monoid, Function.Monoid {
    -- error: conflicting instances for Number
    --     currently in scope: Prod.Monoid
    --     proposed additional instance: Sum.Monoid
    append(inc)(inc)(with Sum.Monoid {empty})
}

But using different instances in different scopes would be allowed:

with Prod.Monoid, Function.Monoid {
    append(inc)(inc)
}(with Sum.Monoid {empty})

Although the term you proposed would still be possible to write like this, at least it would be explicit about where abstraction boundaries lay.

Making such a feature work correctly in the presence of polymorphism and higher-order functions seems like it could be... exciting. Possibly publishable-research-level exciting. I'd be interested to find out whether a focused attempt can be pushed all the way through.

Answer 2

In some situations you can safely use a local explicit instance. In Haskell the reflection library can be used to create such a local instance. See the Reified Monoids for example.

There was also a paper about building that into the language and perhaps making it more usable and general, but I have not read it: Coherent Explicit Dictionary Application for Haskell by Thomas Winant and Dominique Devriese, here is a quote from their contributions section:

In this paper, we propose a new form of explicit dictionary instantiation that preserves coherence and that is safe with respect to global uniqueness of instances, but can be directly applied to common use cases.