CODEWITHSUNDEEP
haskelltypes
egdmitry
egdmitry

Reputation: 2151

When omitting "forall" are they really inserted before the statement automatically?

A lot of articles and books say that forall is explicitly added before the statement if it's not specified. For example

check :: (forall a. [a] -> Int) -> [b] -> [c] -> Bool

is actually

check :: forall b. forall c. (forall a. [a] -> Int) -> [b] -> [c] -> Bool

I have some problems with this because since Haskell uses currying I would imagine that the final signature would look like:

check :: (forall a. [a] -> Int) -> forall b. [b] -> forall c. [c] -> Bool

With added parens for clarity:

check :: (forall a. [a] -> Int) -> (forall b. [b] -> (forall c. [c] -> Bool))

And in this case the version with forall keywords before the expression seems to just be a shortcut for the convenience.

Am I right?

Upvotes: 9

Views: 209

Answers (2)

Stephen Diehl
Stephen Diehl

Reputation: 8419

The nice thing about Haskell is that you can actually look at the intermediate language with the quantifiers explicit by passing -ddump-simpl to the compiler. As Tarmil pointed out, in System Fc rearranging the outer universal quantifiers in this function are semantically identical.

-- surface language
check :: (forall a. [a] -> Int) -> [b] -> [c] -> Bool
check = undefined

app1 = check undefined
app2 = check undefined undefined
app3 = check undefined undefined undefined

Translates to:

-- core language
check :: forall b c. (forall a. [a] -> Int) -> [b] -> [c] -> Bool
check = \ (@ b) (@ c) -> (undefined)

app1 :: forall b c. [b] -> [c] -> Bool
app1 = \ (@ b) (@ c) -> check (\ (@ a) -> undefined)

app2 :: forall c. [c] -> Bool
app2 = \ (@ c) -> check (\ (@ a) -> undefined) (undefined)

app3 :: Bool
app3 = check (\ (@ a) -> undefined) (undefined) (undefined)

Upvotes: 9

Tarmil
Tarmil

Reputation: 11372

In fact, forall a. (T -> U a) is equivalent to T -> (forall a. U a). So both you and the articles are right. The reason people use the former is that it makes it more visually obvious that this is a rank-1 type.

Upvotes: 9

Related Questions