@brandonchinn178

`forall`s in Data Types

July 23, 2021

This post contains a quick guide to using forall in a data type.

Universally quantified type

{-# LANGUAGE RankNTypes #-}

data Foo = Foo { traceFoo :: forall a. Show a => a -> IO a }

foo = Foo { traceFoo = \a -> print foo >> return a }

useFoo :: Foo -> IO ()
useFoo (Foo traceFoo) = do
  x <- traceFoo 1
  b <- traceFoo True
  print (x, b)

In this example, Foo contains a function that is itself parametrized by a. When defining a Foo value like foo, one MUST provide a function that works for any a. Then when consuming a Foo value in useFoo, the caller can call traceFoo on any arbitrary a (with a Show instance).

To go a bit more in-depth, think of forall as an additional argument to the function. So traceFoo actually has two arguments: the type of a (which must have a Show instance), and a value of type a. With this framework, it makes sense why the caller gets to use the same traceFoo function for multiple types; every time the caller calls traceFoo, it can provide a different “argument” for the type of a.

For more information, see: https://wiki.haskell.org/Rank-N_types

Existential type

{-# LANGUAGE ExistentialQuantification #-}

data Bar a = Bar { getBar :: a }

data SomeBar = forall a. Show a => SomeBar (Bar a)

In this example, maybe you want to collect a bunch of Bars in a list. But since lists must contain a single type in Haskell, you can’t have one Bar containing an Int and another containing a String. So we define a SomeBar type that wraps the Bar and hides the type parameter.

bars :: [SomeBar]
bars = [SomeBar (Bar 1), SomeBar (Bar True), SomeBar (Bar "hello")]

useBar :: SomeBar -> IO ()
useBar (SomeBar bar) = print $ getBar bar

When consuming a SomeBar value in useBar, the ONLY thing the caller knows is that bar contains some value of type a (which has a Show instance). In other words, bar already contains some value of some type a and useBar MUST work with that value, whatever it may be.

Typically, existential types are only useful when attaching a constraint on a. Without a constraint, the caller knows that bar contains some value of type a, but it can’t usefully use it in any way (because no function works on all types, except id). If you know about GADTs, existential types can also be useful when Bar is a GADT, where pattern matching on a constructor determines what a is.

To go more in-depth again: since the forall is outside the constructor, if we treat forall as an additional argument, the SomeBar constructor is the thing that has two arguments: the type of a and a value of type Bar a. So every time the provider calls the SomeBar constructor, it can provide a different “argument” for the type of a.

For more information, see: https://wiki.haskell.org/Existential_type

Recap

  Universally quantifed type Existential type
Who gets to decide a? Consumer Provider
The provider… MUST work with any a Wraps a specific a
The consumer… May use it with any a MUST work with any a