Version 9 (modified by igloo, 5 years ago) (diff) |
---|

# Proposal: ExplicitForall

Ticket | #133 |

Dependencies | |

Related | Rank2Types, RankNTypes, LiberalTypeSynonyms, PolymorphicComponents, ScopedTypeVariables |

## Compiler support

GHC | mostly (ExplicitForAll; still allows forall as an expression id; allows superfluous vars to be quantified) |

nhc98 | none |

Hugs | mostly (+98; still allows forall as an expression id) |

UHC | mostly (none; still allows forall as an expression id; allows superfluous vars to be quantified) |

JHC | none |

LHC | none |

## Description

ExplicitForAll enables the use of the keyword 'forall' to make a type explicitly polymorphic. Syntactically, it would mean the following change to Haskell 98:

- forall becomes a reserved word.
- . (dot) becomes a special (not reserved) operator.
- The following syntactic rule changes:

*type* → forall *tyvars* . *type*

|context⇒type

|ftype

*ftype* → *btype* → *type*

|btype

*gendecl* → *vars* :: *type*

It does not allow the use of explicitly polymorphic types in any way not already allowed by Haskell 98 for implicitly polymorphic types.

## Report Delta

[incomplete]

Changes relative to H2010 report.

In Section 2.4:

Replace:

```
| foreign | if | import | in | infix | infixl
```

with:

```
| forall | foreign | if | import | in | infix | infixl
```

In Section 4.1.2:

Replace:

With one exception (that of the distinguished type variable in a class declaration (Section 4.3.1)), the type variables in a Haskell type expression are all assumed to be universally quantified; there is no explicit syntax for universal quantification [4]. For example, the type expression forall a . a -> a denotes the type ∀ a . a → a. For clarity, however, we often write quantification explicitly when discussing the types of Haskell programs. When we write an explicitly quantified type, the scope of the extends as far to the right as possible; for example, ∀ a . a → a means ∀ a . (a → a).

with:

The type variables in a type signature may be explicitly quantified with the forall keyword. All type variables used in the type must be quantified, with one exception (that of the distinguished type variable in a class declaration (Section 4.3.1), which must not be quantified). No additional type variables may be quantified. The scope of the quantifier extends as far to the right as possible. For example, the type expression a -> a denotes the type ∀ a . a → a. Quantifying the type variables is optional. For example, the type expression a -> a also denotes the type ∀ a . a → a.

In Section 4.1.4:

Replace:

```
(Eq a, Show a, Eq b) => [a] -> [b] -> String
```

with:

```
forall a b . (Eq a, Show a, Eq b) => [a] -> [b] -> String
```

## References

http://www.haskell.org/pipermail/haskell-prime/2009-June/002786.html

## Pros

- Small and simple syntactic extension.
- Simplifies the later inclusion of semantic extensions that depend on it, e.g. Rank2Types.
- Easy to implement in tools that don't yet support the semantic extensions.
- The Report already mentions types using the explicit forall-quantified form, so only the grammar changes above are needed.

## Cons

- A small and incremental extension with little value of its own, only serving as a stepping stone for the various semantic extensions.