Can type classes at the type level be simulated with higher-rank types?

Question

I have a pluggable runtime type checker that supports parametric but no ad-hoc polymorphism, because there is no compiling step and type information are erased as soon as the type checker is deactivated.

Now I recently came up with the idea to reify type classes with an explicit type, so that I gain some of their advantages without having to fully incorporate the underlying mechanism into the type checker:

data Functor f = Functor {fmap :: forall a b. (a -> b) -> f a -> f b}

mapList = Functor map
fmap (mapList) (+1) [1,2,3]

It seems as if type classes can be simulated with rank-2 types, at least at the type level, since, of course, there is still no static dispatching.

Is my assumption right and since I am a Haskell rookie, does my explicit functor type involves any advantages over just using map directly?

Continual

Answer 1

The idea of representing a class by a data type is basically a dictionary, which is in fact pretty much how GHC implements type classes anyway: a constrained-polymorphic function/value

f :: Functor f => Y

is at runtime represented by a function

_f_ :: FunctorDict f -> Y

where FunctorDict is essentially your Functor Rank2-ADT (or GADT).

The main thing that's special about actual type classes is that these dictionaries have the singleton property: for every type constructor F, there can only ever be exactly one instance Functor F, whereas you can in principle have multiple different FunctorDict F values. That can at times actually be an an advantage, but often it's just a burden because you need to explicitly carry those dictionaries around (GHC can just pick them automatically, because the choice is unambiguous), and it's harder to state laws.

Kronstadt

Having just one available dictionary has another advantage besides "the compiler can infer it for you": consider Data.Set, for which most operations demand an Ord dictionary. Having just one dictionary possible means you can't introduce bugs by matching up dictionaries and sets in the wrong way. And storing the dictionary in the set doesn't really help much, either, because there are operations that take two sets as arguments, and you really want them to have been constructed using the same dictionary. – Seeder

Oh, and to comment on the last question: "are there any advantages to explicit dictionaries?". Yes, definitely; in particular, it can often be convenient to have different instances of a given class for a given type. A standard example in the Haskell hierarchy are the Product and Sum newtypes, which exist solely to give two different Monoid instances to a single type. With explicit dictionaries, you could just have two dictionaries and not introduce the newtypes. – Seeder

Another advantage of explicit dictionaries is that you can construct instances at runtime. So you can eg express arithmetic modulo p when you don’t know p at compile time. This can actually be done in Haskell by using reflect which essentially allows one to create instances at runtime using some horrific GHC internals magic. – Perloff