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

user_5884503 0
Viewed 192

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.

forall haskell
3 Answers

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.

user_7459030

A type declaration like

f :: A a -> B b -> C

is implicitly universally quantified, i.e. means the same as

f :: forall a b . A a -> B b -> C

Both mean: f has a polymorphic type, where a and b can be anything (i.e. range over all types) . In this case the scope of the forall is the whole type expression, and it is usually left out, but it is always there, implicitly. In your example, it is written explicitly, maybe to neatly enumerate the type variables.

However, there are cases where you need the forall even without typeclasses: rank-N types, where the scope of the forall is not the whole type expression.

A well-known example is used in the ST monad where you see the function:

runST :: forall a. (forall s. ST s a) -> a

Note that the first forall can be omitted, as in the example above, but not the second. Note also that there are no typeclass constraints in the type of runST.

user_5485150

One immediate utility is with TypeApplications extension, where it allows us to explicitly choose the ordering of type variables:

 > foo :: forall a b. a -> b -> b ; foo x y = y
 > :t foo @ Int 1 2
foo @ Int 1 2 :: Num b => b    -- Int goes to the first argument

 > foo :: forall b a. a -> b -> b ; foo x y = y
 > :t foo @ Int 1 2
foo @ Int 1 2 :: Int           -- Int goes to the second argument

I couldn't find it mentioned specifically at the link, but the above interaction was tested in repl.it.

Well, actually, the general description at the link does apply: b appears first in forall b a. a -> b -> b, when it is read from left to right.

user_8498910
Related