Search code examples
haskellforall

What's the utility of forall if not using type class constraint?


I've finished reading the Existential Types Wikibook, and it compares using forall with using lowercase letters for defining generic types. It then says that the true usefulness of forall is when you use it with a type class. That is, forall make your function work with lots of types that adhere to some type class.

Example:

 data ShowBox = forall s. Show s => SB s

Well, I found a real worl usage:

spock :: forall conn sess st. SpockCfg conn sess st -> 
                               SpockM conn sess st () -> IO Middleware
<Source>

and you can see here, in the source that it uses forall but with no type class constraint:

spock :: forall conn sess st. SpockCfg conn sess st -> 
                               SpockM conn sess st () -> IO Wai.Middleware
spock spockCfg spockAppl =
    do connectionPool <-
           case poolOrConn of
             PCNoDatabase ->
             {- ... -}

I'm very new to Haskell and trying to understand forall.


Solution

  • First, forget about existentials. They're a bit of a bodge – I personally never use that extension, only the strictly more general -XGADTs when needed.
    Also, allow me to use the symbol for universal quantification, which I find much more readable. (Note that it looks a bit like the \ lambda, which is the value-level analogue of .) This requires -XUnicodeSyntax.

    So, the signature

    spock :: ∀ conn sess st. SpockCfg conn sess st -> SpockM conn sess st () -> IO Middleware
    

    is, for all outside purposes, exactly the same as

    spock :: SpockCfg conn sess st -> SpockM conn sess st () -> IO Middleware
    

    or

    spock :: SpockCfg c s t -> SpockM c s t () -> IO Middleware
    

    When you see such a signature with explicit , the reason usually doesn't have anything to do with either -XExistentialQuantification or -XRankNTypes. Rather, they either simply found it clearer to explicitly say what are the type variables, or the definition may make use of -XScopedTypeVariables. For example, these two definitions are actually different:

    {-# LANGUAGE ScopedTypeVariables, UnicodeSyntax #-}
    
    foo :: a -> a
    foo x = xAgain
     where xAgain :: a
           xAgain = x
    
    foo' :: ∀ a . a -> a
    foo' x = xAgain
     where xAgain :: a
           xAgain = x
    

    foo doesn't compile, because both the global as well as the local signature is interpreted as implicitly quantified, i.e. as

    foo :: ∀ a . a -> a
    foo x = xAgain
     where xAgain :: ∀ α . α
           xAgain = x
    

    But that doesn't work, because now xAgain would have to have a polymorphic type independent of the type of x you passed in. By contrast, in foo' we only quantise once, and than the a from the global definition is also the type use in the local one.

    In the example of spock, they don't even use a scoped type variable, but I suspect they did during debugging and then just left the there.