Does GHC use dynamic dispatch with existential types?

Question

Does the following bit of code use dynamic dispatch as it's understood in C++ or Java?

As I understand, at the last line, compiler cannot possibly know at compile time which implementation of (==) to call, yet the code compiles and produces correct results. Can someone please explain, what kind of implementation (vptr, for example) lies behind this?

{-# LANGUAGE ExistentialQuantification #-}

data Value = A Int

data ForallFunc = forall a. Eq a => Forall (Value -> a) 

unpackA (A int) = int

equalityTest :: Value -> Value -> ForallFunc -> Bool            
equalityTest arg1 arg2 (Forall unpacker) =
  let a1 = unpacker arg1
      a2 = unpacker arg2 in
    a1 == a2

Handyman

Answer 1

Roughly, yes.

When you use a bounded existential quantification, i.e. when the quantified type variable is restricted by some constraint C a => ... then GHC will store some pointer(s) inside the constructor, remembering the methods of C a so that they can be accessed later on, when you pattern match on that constructor.

Usually a single pointer is used, much like a vptr to a vtable in many OOP implementations. The compiler could also instead store the pointers to the methods directly, avoiding the indirection. I think this is done by GHC when there's only one method in the type class. It might also be used when there are very few, say two, methods -- this would make the memory footprint of each value larger, but faster to access.

So, compiling your code is rouhgly done as if the constraint is replaced with an Eq dictionary, listing its methods. That is:

data EqDict a = EqDict
   { eq  :: a->a->Bool
   , neq :: a->a->Bool }

data ForallFunc = forall a. Forall (EqDict a) (Value -> a) 

unpackA (A int) = int

equalityTest :: Value -> Value -> ForallFunc -> Bool            
equalityTest arg1 arg2 (Forall eqDict unpacker) =
  let a1 = unpacker arg1
      a2 = unpacker arg2 in
    eq eqDict a1 a2

Of course, compiling a constructor call Forall someFunction is compiled, roughly, by providing the implementation for the needed ==, /= functions, on their specific type which will be abstracted away by the existential quantification.

Styrene

Is there maybe some link to an article or a blogpost on this matter you could provide? – Handyman

@Handyman I can't find anything, sorry. What I wrote comes from folk lore. You should be able to find material on the dictionary-based implementation of type classes, by googling a bit. Seeing how dependently typed languages (Coq, Idris, Agda) work with existential types also helps: there, the type argument is (by default) explicit, instead of implicit like in Haskell. – Styrene

Answer 2

Yes, ghc uses a form of dynamic dispatch. The Eq a constraint means that the representation for ForallFunc will contain a dictionary (corresponds to a vtable) which is used at runtime to call the right equality function.

Intravenous