Axion

Haskell

Type-Safe Runtime Dispatch in Haskell

A practical explanation of Typeable, TypeRep, propositional equality, and runtime type-safe dispatch in GHC Haskell.

Can Haskell reflect?

Like most mainstream compiled languages, such as C#, Java, or C++, Haskell compiles to type erased binary. Moreover, GHC translates Haskell to machine code - no JIT, no VM. Yet, GHC Haskell can store and compare type information at runtime.

In this code example, we check if the term x is an integer (Integer) or not. If it is, we treat it as though it has always been an integer - no casting.

import Data.Type.Equality (testEquality)
import Type.Reflection (typeOf, pattern TypeRep, (:~:) (Refl))

printInteger :: Integer -> IO ()
printInteger = print

let x = _
-- (part of a function body)
-- Suppose x has a statically indeterminate type.
case typeOf x `testEquality` TypeRep @Integer of
  Just Refl -> printInteger x -- no casting to make `x` an Integer.
  Nothing -> pure () -- `x` is not an Integer.

When the type test succeeds, GHC proves x is an Integer, letting you pass it directly to printInteger. Let’s see how this works. I’ll discuss this in three parts:

  • The magical Typeable class and its associated type TypeRep _.
  • The type equality constraint ~, and its proof object type :~:, and its only constructor Refl.
  • The testEquality member function (of the TestEquality class, which TypeRep implements).

Prerequisites#

I’ll assume you’re familiar with intermediate-level Haskell, including GADTs and existential types. Essentially, existential types allow hiding their specific types until the program runs. The syntax is:

data E = forall t. (Constraint t) => E t

Typeable and TypeRep#

GHC Haskell has a runtime type representation (TypeRep _). For every type, GHC automatically implements Typeable, the type class that gives you the type representation.

To find the type representation given a type, use the TypeRep pattern synonym, and to find the type representation for a term, use the typeOf function.

tyInt :: TypeRep Int
tyInt = TypeRep @Int

tyChar :: TypeRep Char
tyChar = typeOf 'a'

Type equality#

GHC allows you to express type equality that may be learned (or refined). We don’t need casting after runtime type checking because of this feature.

The pseudocode below illustrates this. Function f has an argument x whose type is unknown but will be determined after the type is tested.

-- Existential data type.
data X = forall x. (Typeable x, Show x) => X x

f :: X -> IO ()
f (X (x :: c)) = do
  -- We don't know what type x has, only that it has
  -- a `Show` instance.
  print x
  -- We can test for its type. Notice how some parts
  -- of f know more about the type than others.
  case typeOf x of
    t | Just Refl <- t `testEquality` TypeRep @Int
      -> _ -- x has type Int
    t | Just Refl <- t `testEquality` TypeRep @Char
      -> _ -- x has type Char
    _ -> _ -- x has unknown type

In typical Haskell code, our knowledge about the type of a term stays throughout an expression. The code example above is different. The testEquality test gives us type information that wasn’t statically available.

First, the notation. Normally, when we bind two type variables, we can’t know if they are the same or different types. Adding the constraint a ~ b, we can express the idea that a and b should refer to the same type.

To pass the constraint a ~ b, Haskell uses a technique called reification. Sharing terms is simpler than sharing constraints. So, Haskell has dedicated a data type (named :~:) to encoding ~.

The data type a :~: b has one constructor, Refl. Refl carries no runtime data - the type is isomorphic to the unit type (()).

Here’s the trick: when the term Refl :: a :~: b is visible, we have a ~ b. Conversely, given a ~ b, we can build Refl with matching type. If this is confusing, let’s consult its definition:

https://hackage.haskell.org/package/base-4.21.0.0/docs/Data-Type-Equality.html#t::-126-:
-- | Propositional equality. If @a :~: b@ is inhabited by some terminating
-- value, then the type @a@ is the same as the type @b@. To use this equality
-- in practice, pattern-match on the @a :~: b@ to get out the @Refl@ constructor;
-- in the body of the pattern-match, the compiler knows that @a ~ b@.
--
-- @since base-4.7.0.0
data a :~: b where  -- See Note [The equality types story] in GHC.Builtin.Types.Prim
  Refl :: a :~: a

Because Refl has types a :~: b and a :~: a, we deduce a ~ b. Awesome!

In short, Refl proves a ~ b, and constructing Refl requires having proved a ~ b. That can sound pointless, but GHC can invoke its magic and smuggle a ~ b using runtime type information (TypeRep).

Note: TypeRep carries the real data, unlike Refl, which has no runtime representation, being a “proof object.”

testEquality and TypeRep#

During execution, two terms’ (or a term and type’s) TypeRep might match or differ. If it matches, Refl can be constructed, but if it doesn’t, it can’t. This surely sounds like the textbook use case of Maybe.

testEquality (member function of the class TestEquality) takes two type representations and then returns Maybe (a :~: b). It calls out to GHC machinery to test if two type representations are equal, and if so, it constructs a Just Refl term - the proof object for a ~ b. So, in the Just Refl branch, we have a ~ b, but in the other branch, we don’t.

The TestEquality type class is implemented by TypeRep, but also by a handful of other types, where equality of types can be decided from the values in terms.

Putting this all together#

I will show you an example of using a heterogeneous list and processing items differently based on their actual types. A heterogeneous or mixed-type collection in Haskell is possible, thanks to existential data types. In existential data types, the type of the inner term (we’ll see) is not known statically; type information is bundled when the term is constructed.

-- tested on GHC 9.6.7 and 9.12.2.

{-# LANGUAGE GADTs, PatternSynonyms #-}

-- All modules in this code snippet are
-- available in the `base` package.
import Data.Type.Equality (testEquality)
import Type.Reflection
  ( Typeable, TypeRep, pattern TypeRep
  , (:~:) (Refl), typeOf
  )

-- (For demo)
import Text.Printf (printf)

-- | Existential data type - we break parametricity,
-- so GHC will record the type of its arguments in the constructor,
-- as well as any dictionaries for the constraints.
-- This is how we implement dynamic typing in Haskell.
data E = forall t. (Typeable t, Show t) => E t

hi :: String
hi = "Hi there, "

-- | Dynamically dispatch actions based on the type. Use
-- functions that can only be used against specific types
-- without casting them and creating new references.
process :: E -> IO ()
process (E e) = case typeOf e of
  t | Just Refl <- t `testEquality` TypeRep @Int
                -> printf "e (%v) is an int.\n" e
  t | Just Refl <- t `testEquality` typeOf hi
                -> printf "e (%s) is a string. %s!\n" e (hi ++ e)
  t -> printf "e (%s) has type %s.\n" (show e) (show t)

-- | Test if two terms have the same type without naming
-- the type in code.
equality :: (E, E) -> IO ()
equality (E e, E f)
  | Just Refl <- typeOf e `testEquality` typeOf f
    = printf "Found a pair: %s and %s have the same type (%s).\n"
        (show e) (show f) (show (typeOf e))
  | otherwise
    = pure ()

-- | Helper.
--
-- @
-- [1,2,3] -> [(1,2),(1,3),(2,3)]
-- [1,2,3,4] -> [(1,2),(1,3),(1,4),(2,3),(2,4),(3,4)]
-- @
triangle :: [a] -> [(a, a)]
triangle [] = []
triangle (x : xs) = ((x,) <$> xs) ++ triangle xs

main :: IO ()
main = do
  let xs =
        [ E (1 :: Int)
        , E "buster"
        , E (-3.6 :: Double)
        , E (4 :: Int)
        , E "ocean"
        , E (6 :: Int)
        , E ()
        ]
  putStrLn "(1). Type-aware processing\n"
  mapM_ process xs
  putStrLn "\n(2). Type equality between two terms\n"
  mapM_ equality (triangle xs)

Result:

(1). Type-aware processing

e (1) is an int.
e (buster) is a string. Hi there, buster!
e (-3.6) has type Double.
e (4) is an int.
e (ocean) is a string. Hi there, ocean!
e (6) is an int.
e (()) has type ().

(2). Type equality between two terms

Found a pair: 1 and 4 have the same type (Int).
Found a pair: 1 and 6 have the same type (Int).
Found a pair: "buster" and "ocean" have the same type ([Char]).
Found a pair: 4 and 6 have the same type (Int).

Overhead?#

Haskell’s Typeable has a different cost model than traditional runtime type systems:

  • Zero cost: If your code doesn’t use Typeable constraints, there’s no runtime overhead. Type information is only included when functions or constructors specifically need it.
  • Shared type representations: TypeRep values are shared across all instances of the same type, not stored per-value. A million Int values share the same TypeRep Int.
  • Fast comparisons: Equality checks are fast; they mainly compare type fingerprints (a few pointer or hash checks).
  • Dictionary passing: With Typeable constraints, GHC passes type dictionaries as hidden parameters in functions. This is like other type class overhead in Haskell.

GHC generates a Typeable dictionary and metadata, and embeds them in compiled Haskell code. But the dictionary is passed only to places that require it, and the metadata is stored separately from the data definition.

Using Typeable constraints may add a tiny performance cost to function calls (a pointer to the Typeable dictionary). But for most applications, this overhead is negligible compared to the flexibility gained.

(For information about how GHC arranges data, consult “Heap Objects” from the GHC Wiki.)

Summary#

Using TypeRep, :~:, and testEquality, we can test for type equality at runtime and dispatch to type-specific behavior. When the equality test succeeds, GHC provides the type information needed to use the values safely without explicit casting.

Use this for diverse data, flexible libraries, or when you need type-based runtime choices while keeping type safety.