Explicit `forall`

As of March 2020, School of Haskell has been switched to read-only mode.

These extensions allow finer-grained control over polymorphism.


Available in: GHC 6.12 and later

The ExplicitForAll extension allows you to explicitly specify the universal quantification in polymorphic type signatures. For example, this:

Just :: a -> Maybe a
Nothing :: Maybe a
reverse :: [a] -> [a]
map :: (a -> b) -> [a] -> [b]
show :: (Show a) => a -> String

becomes this:

Just :: forall a. a -> Maybe a
Nothing :: forall a. Maybe a
reverse :: forall a. [a] -> [a]
map :: forall a b. (a -> b) -> [a] -> [b]
show :: forall a. (Show a) => a -> String

GHC does this for you anyway, but while ExplicitForAll is not very useful on its own, the other extensions in this section depend on the ability to write out your foralls manually, to allow you to write them in places GHC normally wouldn't.

Although ExplicitForAll is important as a prerequisite for all of the other extensions in this section, it does not do anything on its own that could not be done in standard Haskell.


Available in: All recent GHC versions

The ScopedTypeVariables extension is perhaps the simplest of the actually useful forall-based extensions. It allows you to specify that the type variables in a definition's signature should be scoped over the body of that definition.

To give some motivation, consider the following function:

import Data.List

main = putStrLn "No errors."

-- show
myFunction :: Ord a => [a] -> [(a, a)]
myFunction inputList = zip sortedList nubbedList
    where sortedList = sort inputList
          nubbedList = nub inputList
-- /show

What happens if we try to give a type to sortedList or nubbedList? Let's see:

import Data.List

main = putStrLn "No errors."

-- show
myFunction :: Ord a => [a] -> [(a, a)]
myFunction inputList = zip sortedList nubbedList
    where sortedList :: [a]
          sortedList = sort inputList
          nubbedList :: [a]
          nubbedList = nub inputList
-- /show

We get some ugly errors telling us the the a's in our inner definitions are not the same as the a in our outer definition (the two inner a's aren't the same as each other, either). How can we fix this? We need a way to tell GHC that, inside the where clause, [a] does not mean forall a. [a], but instead closes over the a from the outer definition.

This is what ScopedTypeVariables is for. By enabling it, and by placing a forall in the outer definition's signature, that a becomes scoped over the whole body of the outer definition, including the where clause:

{-# LANGUAGE ScopedTypeVariables #-}
import Data.List

main = putStrLn "No errors."

-- show
myFunction :: forall a. Ord a => [a] -> [(a, a)]
myFunction inputList = zip sortedList nubbedList
    where sortedList :: [a]
          sortedList = sort inputList
          nubbedList :: [a]
          nubbedList = nub inputList
-- /show

Try it out!

{-# LANGUAGE ScopedTypeVariables #-}
import Data.List

main = print $ myFunction [1, 1, 3, 2]

myFunction :: forall a. Ord a => [a] -> [(Char, a, a)]
myFunction inputList = zip3 ['a'..'z'] sortedList nubbedList
    where sortedList :: [a]
          sortedList = sort inputList
          nubbedList :: [a]
          nubbedList = nub inputList


Available in: All recent GHC versions

In standard, unextended Haskell, type synonyms are fairly restricted. They must always be fully applied and they cannot contain type variables other than their parameters. The LiberalTypeSynonyms extension relaxes both of these limitations, as well as some others that only come into play when certain other extensions are used (the use of LiberalTypeSynonyms in combination with each other relevant extension is described in the section for that particular other extension).

When LiberalTypeSynonyms is enabled, GHC only type-checks a signature after all type synonyms have been expanded, outermost first. You can now partially apply a type synonym, as long as it's surrounded by another type synonym such that the obvious outermost-first expansion will cause the partially-applied synonym to become fully applied.

This means that the following partial application of type synonyms is now legal:

{-# LANGUAGE LiberalTypeSynonyms #-}
import Data.Char

main = putStrLn "No errors."

-- show
type Const a b = a

type Id a = a

type NatApp f g i = f i -> g i

myFunc :: NatApp Id (Const Int) Char
--     ~  Id Char -> Const Int Char
--     ~  Char    -> Int
myFunc = ord
-- /show

It's important to note that GHC will still kind-check type synonyms and their (possibly partial) applications, just not type-check them (until after full expansion). It will also still forbid any expansion that would be illegal for some other reason; i.e., LiberalTypeSynonyms alone will not allow type safety to be broken. Anything that would not type-check even after all type synonyms are expanded will still remain illegal with LiberalTypeSynonyms enabled.

While LiberalTypeSynonyms does not by itself use explicit foralls, it is often important when working with the rest of the extensions in this section, so its guide is placed here for convenience.

RankNTypes, Rank2Types, and PolymorphicComponents

Available in: All recent GHC versions

Basic Usage

The RankNTypes extension (as well as its deprecated synonyms Rank2Types and PolymorphicComponents) allows you to nest explicit foralls within function types and data definitions. For example, the following program requires RankNTypes:

{-# LANGUAGE RankNTypes #-}

-- show
main = print $ rankN (+1)

rankN :: (forall n. Num n => n -> n) -> (Int, Double)
rankN f = (f 1, f 1.0)
-- /show

The difference between the signature of rankN and the similar signature

forall n. Num n => (n -> n) -> (Int, Double)

is that, in the latter, n is chosen by the caller, but in the former, n is chosen by the callee; in both cases n may be chosen more than once! In other words, you could pass a function of type Int -> Int or Double -> Double as the first parameter of the latter signature, and the type system would be fine with it. However, the former signature forces its user to only pass in truly polymorphic functions: functions precisely of type forall n. Num n => n -> n or more general. (+1) is one such function, as are (6*), abs, and id; however, you could not pass in (/5) because that requires Fractional, even if some types with an instance of Num also have an instance of Fractional. The latter signature requires a function from n to n for some Num n; the former signature requires a function from n to n for every Num n.

Interaction with LiberalTypeSynonyms

With both RankNTypes and LiberalTypeSynonyms enabled, it becomes possible to:

  • use forall and/or constraints in type synonyms:

{-# LANGUAGE RankNTypes, LiberalTypeSynonyms #-}

main = putStrLn "No errors."

-- show
type Const a b = a

type Id a = a

type Indexed f g = forall i. f i -> g i

type ShowIndexed f g = forall i. (Show i) => f i -> g i

type ShowConstrained f a = (Show a) => f a

type FunctionTo a b = b -> a

myFunc1 :: Indexed Id (Const Int)
--      ~  forall i. Id i -> Const Int i
--      ~  forall i. i    -> Int
myFunc1 _ = 2

myFunc2 :: ShowIndexed Id (Const Int)
--      ~  forall i. (Show i) => Id i -> Const Int i
--      ~  forall i. (Show i) => i    -> Int
myFunc2 = length . show

myFunc3 :: forall a. ShowConstrained (FunctionTo Char) a
--      ~  forall a. (Show a) =>      FunctionTo Char  a
--      ~  forall a. (Show a) =>      a -> Char
myFunc3 = head . show
-- /show
  • apply (or even partially apply) a type synonym to a type containing forall and/or constraints:

{-# LANGUAGE RankNTypes, LiberalTypeSynonyms #-}

main = putStrLn "No errors."

-- show
type ShowConstrained f = forall a. (Show a) => f a

type EnumFunctionTo b a = (Enum a) => a -> b

myFunc :: ShowConstrained              (EnumFunctionTo Char)
--     ~  forall a. (Show a) =>         EnumFunctionTo Char a
--     ~  forall a. (Show a, Enum a) => a -> Char
myFunc = head . show . succ
-- /show

Use Case: The ST Monad

There is a place in the standard libraries where RankNTypes is used to great effect. That place is the Control.Monad.ST module in the base package (as well as its submodules), and RankNTypes is used there to allow local mutability while maintaining a pure interface.

Let's say we want to implement an algorithm in Haskell, but the algorithm we've chosen depends internally upon mutability. Nonetheless, we know that the algorithm is effectively pure. Take the following semi-contrived example (in C-like pseudocode), trying to demonstrate the Collatz conjecture:

Integer collatz(Integer n) {
    assert(n > 0, "n must be positive");
    Integer x = n;
    Integer count = 0;
    while (x != 1) {
        count = count+1;
        if (x % 2 == 0) {
            x = x/2;
        } else {
            x = 3*x+1;
    return count;

Let's say we want to implement this algorithm in Haskell, and we want it to be a pure function (because it effectively is), but we don't want to give up the efficiency that mutability affords us. Fortunately, the ST monad comes to our rescue. Here's how this example looks in Haskell:

import Control.Exception (evaluate)
import Control.Monad.ST
import Data.STRef
import System.IO

-- copied verbatim from:
-- monad-loops-
whileM_ :: (Monad m) => m Bool -> m a -> m ()
whileM_ p f = go
    where go = do x <- p
                  if x
                     then f >> go
                     else return ()

main = do putStrLn "Enter a positive integer:"
          ln <- getLine
          if null ln then hFlush stdout else
            do let x = collatz $ read ln
               evaluate x
               putStr $ "collatz " ++ ln ++ " = "
               print x

-- show
collatz :: Integer -> Integer
collatz n | n > 0 = runST $ do xRef <- newSTRef n
                               countRef <- newSTRef (0 :: Integer)
                               whileM_ (do x <- readSTRef xRef
                                           return $ x /= 1)
                                       (do modifySTRef countRef (+1)
                                           modifySTRef xRef (\x -> if even x
                                                                      then x `div` 2
                                                                      else 3*x+1))
                               readSTRef countRef
          | otherwise = error "n must be positive"
-- /show

What does this have to do with RankNTypes? Well, the signatures of the various ST functions we've used are as follows:

newSTRef :: forall s a. a -> ST s (STRef s a)
readSTRef :: forall s a. STRef s a -> ST s a
writeSTRef :: forall s a. STRef s a -> a -> ST s () -- not used in this example
modifySTRef :: forall s a. STRef s a -> (a -> a) -> ST s ()
runST :: forall a. (forall s. ST s a) -> a

Notice that the ST monad (as well as STRefs) carries around an extra type parameter s that runST forces to be completely polymorphic and not present in its result. If you try to pass a mutable variable out of the ST monad (e.g., if you call runST on a value of type ST s (STRef s a)), it will be a compile-time error. See what happens when we try to break referential transparency:

import Control.Monad.ST
import Data.STRef

main = putStrLn "No errors."

-- show
illegal = runST $ do xRef <- newSTRef (0 :: Integer)
                     modifySTRef xRef (+1)
                     return xRef
-- /show

We get a compile-time error that tells us that there is no possible valid type for illegal. Because of the use of RankNTypes in the signature of runST, it is statically guaranteed that the result of runST is pure, even if the computation uses mutability internally.

Use Case: lens

The lens library makes use of RankNTypes (and LiberalTypeSynonyms) to implement the very powerful notion of lenses, sometimes called “functional references”. The idea behind lenses is that we need a thing like a property accessor: something that, given a value of its source type, can produce a value of its target type, and that, given a value of its source type and a value of its target type, can produce a modified value of its source type:

type Lens' s a
view :: Lens' s a -> s -> a
set :: Lens' s a -> a -> s -> s

(Note that the actual types are a bit more general than this; see the lens package's documentation, linked above, for the exact types used).

For example, the lens package (in the Data.Complex.Lens module) conveniently provides a lens to get the real part of a complex number:

_realPart :: Lens' (Complex a) a

We can use view to feed this lens a complex number, and we will get back its real part; we can also use set to feed this lens a complex number and a new real part, and we will get back a complex number with the new real part and the original imaginary part:

import Data.Complex
import Control.Lens
import Data.Complex.Lens

main = do putStr "c  = "
          print   c
          putStr "r  = "
          print   r
          putStr "r' = "
          print   r'
          putStr "c' = "
          print   c'

-- show
c  :: Complex Double
c  =  1.0 :+ 2.5

r  :: Double
r  =  view _realPart c

r' :: Double
r' =  2.0

c' :: Complex Double
c' =  set _realPart r' c
-- /show

How is RankNTypes involved here? Well, it has to do with the implementation of the Lens' type alias (see the lens package documentation for the actual code involved):

type Lens' s a = forall f. (Functor f) => (a -> f a) -> (s -> f s)

While this is not the place for a full introduction to the van Laarhoven lens representation and its many and varied uses and extensions, suffice to say that RankNTypes plays a critical role in the core functionality of the lens package, and that much of that functionality is impossible to reproduce in any language without either higher-rank universal polymorphism or some equivalent capability.

comments powered by Disqus