Can I discharge a constraint, if I know the class is solvable for all types of a kind?-CodePudding

This might seem like a stupid question, but let's say I have a Haskell type class C (a :: K) defined for some fixed kind K, and I know I have instances C a for all types a :: K. Let's furthermore assume I have T :: K -> * and a value t :: C A => T A, is there any way to eliminate the constraint? I feel like this should be possible, but I can't come up with anything.

I'm mainly interested in the case where K is a data kind.

CodePudding user response：

No.

The problem here is simple: foralls in Haskell are parametric polymorphism. This means that the same code must run no matter which type gets chosen. The thing I want to say next needs a way to pull out the C a => part of a type and talk about it in isolation, and there isn't really a way to do that in Haskell's syntax. But making up a type that's kinda like that is pretty standard:

data Dict c where Dict :: c => Dict c

Now the thing you are asking for, essentially, is:

magic :: forall a. Dict (C a)

Unfortunately, the code that you want this to represent -- the behaviors of the class methods -- is different for each type of the appropriate kind.

"Okay, okay," I hear you cry, "but when I write t :: C a => T a, isn't that running different code depending on the choice of a?". But no, it turns out, you aren't. There are two extant implementation schemes for typeclasses: dictionaries (alluded to above, and essentially the same as vtables if you're familiar with that from C ) and explicit type representations. In both cases, under the hood, <C> => <T> is actually a function -- taking the methods implementing the constraint <C> in the one case and a runtime representation of all the types mentioned in the constraint <C> in the other. And that function is the same function in all cases -- the dispatch to different code paths happens in the caller.

The type forall a. Dict (C a), on the other hand, has no such luxury: its type is not permitted to be a function under the hood, but must instead be a value of a specific data type.

CodePudding user response：

Consider this module:

data K = A | B

class C (t::K) where
  str :: String

instance C 'A where
  str = "A"

instance C 'B where
  str = "B"


type family F :: K

foo :: String
foo = str @F

Arguably, C t holds for all t::K, since we have the two instances. Then, however, we define a type family F::K which is, essentially, an unknown kind: it could be A, it could be B. Without a line such type instance F = ... defining F, it is impossible to define foo, since it could be "A" or "B".

Indeed, it is impossible to resolve this constraint.

Note that the type instance might even be defined in another module. Indeed, it is pretty common to define type families and type instances in distinct modules, like we do for type classes and their instances. It is impossible, however, to perform separate compilation when we have no information about the type instance.

The solution is, of course, deferring the constraint resolution by adding the constraint to foo:

foo :: C F => String
foo = str @F