Resolving a Function Call in an Existential Type

Question

Upon reading this page on existentials in Haskell, I was compelled to test the limits of this behavior, so I wrote the following code snippet:

{-# LANGUAGE ExistentialQuantification #-}

data Showable = forall a. Show a => MkShowable a

pack :: Show a => a -> Showable
pack = MkShowable

instance Show Showable where
    show (MkShowable x) = show x

The Showable type is very similar to the ShowBox type created in the aforementioned link. Then I created this contrived example to illustrate my question.

showSomething :: Bool -> Showable
showSomething True = pack 1
showSomething False = pack "ABC"

main :: IO ()
main = do
  x <- getLine
  let y = read x
  print $ showSomething y

This code (which works fine) asks the user for input (which should be 'True' or 'False'), and then prints out 1 if it is True or "ABC" if it is False.

But I'm failing to fully understand how the system does this. Mathematically, it makes perfect sense. But I don't see how the computer is able to resolve it. To me, it looks like the system makes a decision at runtime concerning whether to call Int's show instance or String's show function, but that would imply the existence of a something like C++'s vtables, which I don't believe Haskell has a concept of.

My question is: how does it resolve that? The system can't know in advance whether I'm going to input true or false, so it can't know which show to call at compile-time, yet it clearly works in both cases.

Answer 1

One way how to implement type classes is passing a dictionary of functions that implement a type class under the hood. For example a function with signature

f :: Show a => T

would be translated into

f' :: (a -> String) -> T

by the compiler and whenever show is used inside f, it's replaced by the additional argument (in reality there would be more functions, all that are declared in Show).

Similarly the data type

forall a . Show a => MkShowable a

would be translated into

forall a . MkShowable' (a -> String) a

So the transformed code might look like this:

{-# LANGUAGE ExistentialQuantification #-}

data Showable' = forall a . MkShowable' (a -> String) a

pack' :: Show a => a -> Showable'
pack' = MkShowable' show

instance Show Showable' where
    show (MkShowable' f x) = f x

showSomething :: Bool -> Showable'
showSomething True = pack' 1
showSomething False = pack' "ABC"

When pack is called, the show implementation is passed to the constructor as well so that it's available when needed.

Answer 2

Yep. A bunch of language features (most of them extensions) in Haskell can be viewed as basically implementing many of the concepts that are bundled up in the complex monolith of a "class" in OO-programming, but individually as separate features. Existential types with type class constraints basically are vtables!

In order for show (MkShowable x) to work without any other constraints, MkShowable x has to contain enough information to know how to show x. So that's exactly what it does; even though it only has one field, it actually contains additional information.

This is essentially the same as how a function foo :: Show a => a; foo x = show x seems to only have one parameter, but actually has to receive enough additional information to know how show x; it can't be "hard-wired" in because foo is likely used at several different types. But where foo requires its caller to pass that information in from the outside (and the type system enforces this), a Showable value contains exactly the same information, in order to be able to extract it for passing to functions like foo.

So now with this facility, unlike without ExistentialQuantification the problem of knowing which show instance to call is just selecting between two values of the same type (which contains a Show instance for some unknown type together with a value of that same type), which is easy to do; no compile-time knowledge of which one it is is needed.