Skip to content

Changes

Page history
Fix names of language exnteions pages authored by Ben Gamari's avatar Ben Gamari
Hide whitespace changes
Inline Side-by-side
ExplicitForall.md 0 → 100644
View page @ d5606db0
# Proposal: [ExplicitForall](explicit-forall)
<table><tr><th> Ticket </th>
<th> [\#133](https://gitlab.haskell.org//haskell/prime/issues/133)
</th></tr>
<tr><th> Dependencies </th>
<th>
</th></tr>
<tr><th> Related </th>
<th> Rank2Types, RankNTypes, [LiberalTypeSynonyms](liberal-type-synonyms), [PolymorphicComponents](polymorphic-components), [ScopedTypeVariables](scoped-type-variables)
</th></tr></table>
## Compiler support
<table><tr><th> GHC </th>
<th> mostly (ExplicitForAll; still allows forall as an expression id; allows superfluous vars to be quantified)
</th></tr>
<tr><th> nhc98 </th>
<th> none
</th></tr>
<tr><th> Hugs </th>
<th> mostly (+98; still allows forall as an expression id; doesn't allow 0 tyvars to be quantified)
</th></tr>
<tr><th> UHC </th>
<th> mostly (none; still allows forall as an expression id; allows superfluous vars to be quantified; doesn't allow 0 tyvars to be quantified)
</th></tr>
<tr><th> JHC </th>
<th> none
</th></tr>
<tr><th> LHC </th>
<th> none
</th></tr></table>
## Description
ExplicitForAll enables the use of the keyword 'forall' to explicitly state that a type is polymorphic in its free type variables.
It does not allow any types to be written that cannot already be written; it just allows the programmer to explicitly state the (currently implicit) quantification.
## 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
- Programs using `forall` as a type or expression variable will break.
- A small and incremental extension with little value of its own, only serving as a stepping stone for the various semantic extensions.
## Report Delta
Changes relative to H2010 report.
Two versions are given. The first makes `forall` a keyword, while the second only makes it a keyword in a type. The committee may choose which they prefer.
### Report Delta, with `forall` as a keyword
In [ Section 2.4](http://www.haskell.org/onlinereport/haskell2010/haskellch2.html#x7-180002.4):
Replace:
```
| foreign | if | import | in | infix | infixl
```
with:
```
| forall | foreign | if | import | in | infix | infixl
```
---
In [ Section 3](http://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-220003):
Replace:
```
exp → infixexp :: [context =>] type (expression type signature)
```
with:
```
exp → infixexp :: [forall tyvar1 … tyvark .] [context =>] type (expression type signature, k ≥ 0)
```
---
In [ Section 3.16](http://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-560003.16):
Replace:
```
exp → exp :: [context =>] type
Expression type-signatures have the form e :: t, where e is an expression and t is a type (Section 4.1.2);
they are used to type an expression explicitly and may be used to resolve ambiguous typings due to
overloading (see Section 4.3.4). The value of the expression is just that of exp. As with normal type
signatures (see Section 4.4.1), the declared type may be more specific than the principal type derivable from
exp, but it is an error to give a type that is more general than, or not comparable to, the principal type.
```
with:
```
exp → exp :: [forall tyvar1 … tyvark .] [context =>] type (k ≥ 0)
Expression type-signatures have the form e :: t, where e is an expression and t is a type (Section 4.1.2);
they are used to type an expression explicitly and may be used to resolve ambiguous typings due to
overloading (see Section 4.3.4). The value of the expression is just that of exp. As with normal type
signatures (see Section 4.4.1), the declared type may be more specific than the principal type derivable from
exp, but it is an error to give a type that is more general than, or not comparable to, the principal type.
The quantification [forall tyvar1 … tyvark .] is optional, but if given it must quantify exactly the set of
type variables used in [context =>] type (with one exception: that of the distinguished type variable in a
class declaration (Section 4.3.1), which must not be quantified).
```
Note: See also [\#140](https://gitlab.haskell.org//haskell/prime/issues/140).
---
In [ Section 4](http://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-620004):
Replace:
```
gendecl → vars :: [context =>] type (type signature)
```
with:
```
gendecl → vars :: [forall tyvar1 … tyvark .] [context =>] type (type signature, k ≥ 0)
```
---
In [ Section 4.1.2](http://www.haskell.org/onlinereport/haskell2010/haskellch4.html#dx10-65031):
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. For convenience, we
write forall vs . t even if there is no forall vs ..
```
---
In [ Section 4.1.4](http://www.haskell.org/onlinereport/haskell2010/haskellch4.html#verbatim-27):
Replace:
```
(Eq a, Show a, Eq b) => [a] -> [b] -> String
```
with:
```
forall a b . (Eq a, Show a, Eq b) => [a] -> [b] -> String
```
---
In [ Section 4.3.1](http://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-760004.3.1):
Replace:
```
for which there is an explicit type signature vi :: cxi => ti in cdecls.
```
with:
```
for which there is an explicit type signature vi :: forall vs . cxi => ti in cdecls.
```
---
In [ Section 4.4.4](http://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-810004.4.1):
Replace:
```
gendecl → vars :: [context =>] type
```
with:
```
gendecl → vars :: [forall tyvar1 … tyvark .] [context =>] type (k ≥ 0)
```
Replace:
```
A type signature specifies types for variables, possibly with respect to a context. A type signature has the
form: v1, …, vn :: cx => t which is equivalent to asserting vi :: cx => t for each i from 1 to n.
```
with:
```
A type signature specifies types for variables, possibly with respect to a context. A type signature has the
form: v1, …, vn :: forall vs . cx => t which is equivalent to asserting vi :: cx => t for each i from 1 to n.
```
---
In [ Section 8.4](http://www.haskell.org/onlinereport/haskell2010/haskellch8.html#x15-1540008.4):
Replace:
```
fdecl → import callconv [safety] impent var :: ftype (define variable)
| export callconv expent var :: ftype (expose variable)
```
with:
```
fdecl → import callconv [safety] impent var :: [forall tyvar1 … tyvark .] ftype (define variable, k ≥ 0)
| export callconv expent var :: [forall tyvar1 … tyvark .] ftype (expose variable, k ≥ 0)
```
Replace:
```
It implies that the arity of the external entity is n.
```
with:
```
It implies that the arity of the external entity is n. If a universal quantifier is given, it must quantify
exactly the set of type variables used in the type.
```
---
In [ Section 10.2](http://www.haskell.org/onlinereport/haskell2010/haskellch10.html#TBL-103-4-):
Replace:
```
| foreign | if | import | in | infix | infixl
```
with:
```
| forall | foreign | if | import | in | infix | infixl
```
---
In [ Section 10.5](http://www.haskell.org/onlinereport/haskell2010/haskellch10.html#TBL-105-60-2):
Replace:
```
gendecl → vars :: [context =>] type (type signature)
```
with:
```
gendecl → vars :: [forall tyvar1 … tyvark .] [context =>] type (type signature, k ≥ 0)
```
---
In [ Section 10.5](http://www.haskell.org/onlinereport/haskell2010/haskellch10.html#TBL-105-118-):
Replace:
```
fdecl → import callconv [safety] impent var :: ftype (define variable)
| export callconv expent var :: ftype (expose variable)
```
with:
```
fdecl → import callconv [safety] impent var :: [forall tyvar1 … tyvark .] ftype (define variable, k ≥ 0)
| export callconv expent var :: [forall tyvar1 … tyvark .] ftype (expose variable, k ≥ 0)
```
---
In [ Section 10.5](http://www.haskell.org/onlinereport/haskell2010/haskellch10.html#TBL-105-153-):
Replace:
```
exp → infixexp :: [context =>] type (expression type signature)
```
with:
```
exp → infixexp :: [forall tyvar1 … tyvark .] [context =>] type (expression type signature, k ≥ 0)
```
### Report Delta, with `forall` as a keyword in types only
In [ Section 2.4](http://www.haskell.org/onlinereport/haskell2010/haskellch2.html#x7-180002.4):
In opening block, add:
```
tyvar -> varid<reservedtypeid>
```
after `varid` and add:
```
reservedtypeid -> forall
```
after `reservedid`.
Replace:
```
tyvar -> varid (type variables)
```
with:
```
tyvar -> varid<reservedtypeid> (type variables)
```
---
In [ Section 3](http://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-220003):
Replace:
```
exp → infixexp :: [context =>] type (expression type signature)
```
with:
```
exp → infixexp :: [forall tyvar1 … tyvark .] [context =>] type (expression type signature, k ≥ 0)
```
---
In [ Section 3.16](http://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-560003.16):
Replace:
```
exp → exp :: [context =>] type
Expression type-signatures have the form e :: t, where e is an expression and t is a type (Section 4.1.2);
they are used to type an expression explicitly and may be used to resolve ambiguous typings due to
overloading (see Section 4.3.4). The value of the expression is just that of exp. As with normal type
signatures (see Section 4.4.1), the declared type may be more specific than the principal type derivable from
exp, but it is an error to give a type that is more general than, or not comparable to, the principal type.
```
with:
```
exp → exp :: [forall tyvar1 … tyvark .] [context =>] type (k ≥ 0)
Expression type-signatures have the form e :: t, where e is an expression and t is a type (Section 4.1.2);
they are used to type an expression explicitly and may be used to resolve ambiguous typings due to
overloading (see Section 4.3.4). The value of the expression is just that of exp. As with normal type
signatures (see Section 4.4.1), the declared type may be more specific than the principal type derivable from
exp, but it is an error to give a type that is more general than, or not comparable to, the principal type.
The quantification [forall tyvar1 … tyvark .] is optional, but if given it must quantify exactly the set of
type variables used in [context =>] type (with one exception: that of the distinguished type variable in a
class declaration (Section 4.3.1), which must not be quantified).
```
Note: See also [\#140](https://gitlab.haskell.org//haskell/prime/issues/140).
---
In [ Section 4](http://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-620004):
Replace:
```
gendecl → vars :: [context =>] type (type signature)
```
with:
```
gendecl → vars :: [forall tyvar1 … tyvark .] [context =>] type (type signature, k ≥ 0)
```
---
In [ Section 4.1.2](http://www.haskell.org/onlinereport/haskell2010/haskellch4.html#dx10-65031):
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. For convenience, we
write forall vs . t even if there is no forall vs ..
```
---
In [ Section 4.1.3](http://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-660004.1.3):
Replace:
```
tyvar -> varid
```
with:
```
tyvar -> varid<reservedtypeid>
reservedtypeid -> forall
```
---
In [ Section 4.1.4](http://www.haskell.org/onlinereport/haskell2010/haskellch4.html#verbatim-27):
Replace:
```
(Eq a, Show a, Eq b) => [a] -> [b] -> String
```
with:
```
forall a b . (Eq a, Show a, Eq b) => [a] -> [b] -> String
```
---
In [ Section 4.3.1](http://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-760004.3.1):
Replace:
```
for which there is an explicit type signature vi :: cxi => ti in cdecls.
```
with:
```
for which there is an explicit type signature vi :: forall vs . cxi => ti in cdecls.
```
---
In [ Section 4.4.4](http://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-810004.4.1):
Replace:
```
gendecl → vars :: [context =>] type
```
with:
```
gendecl → vars :: [forall tyvar1 … tyvark .] [context =>] type (k ≥ 0)
```
Replace:
```
A type signature specifies types for variables, possibly with respect to a context. A type signature has the
form: v1, …, vn :: cx => t which is equivalent to asserting vi :: cx => t for each i from 1 to n.
```
with:
```
A type signature specifies types for variables, possibly with respect to a context. A type signature has the
form: v1, …, vn :: forall vs . cx => t which is equivalent to asserting vi :: cx => t for each i from 1 to n.
```
---
In [ Section 8.4](http://www.haskell.org/onlinereport/haskell2010/haskellch8.html#x15-1540008.4):
Replace:
```
fdecl → import callconv [safety] impent var :: ftype (define variable)
| export callconv expent var :: ftype (expose variable)
```
with:
```
fdecl → import callconv [safety] impent var :: [forall tyvar1 … tyvark .] ftype (define variable, k ≥ 0)
| export callconv expent var :: [forall tyvar1 … tyvark .] ftype (expose variable, k ≥ 0)
```
Replace:
```
It implies that the arity of the external entity is n.
```
with:
```
It implies that the arity of the external entity is n. If a universal quantifier is given, it must quantify
exactly the set of type variables used in the type.
```
---
In [ Section 10.2](http://www.haskell.org/onlinereport/haskell2010/haskellch10.html#TBL-103-16-1):
Replace:
```
tyvar -> varid (type variables)
```
with:
```
tyvar -> varid<reservedtypeid> (type variables)
reservedtypeid -> forall
```
---
In [ Section 10.5](http://www.haskell.org/onlinereport/haskell2010/haskellch10.html#TBL-105-60-2):
Replace:
```
gendecl → vars :: [context =>] type (type signature)
```
with:
```
gendecl → vars :: [forall tyvar1 … tyvark .] [context =>] type (type signature, k ≥ 0)
```
---
In [ Section 10.5](http://www.haskell.org/onlinereport/haskell2010/haskellch10.html#TBL-105-118-):
Replace:
```
fdecl → import callconv [safety] impent var :: ftype (define variable)
| export callconv expent var :: ftype (expose variable)
```
with:
```
fdecl → import callconv [safety] impent var :: [forall tyvar1 … tyvark .] ftype (define variable, k ≥ 0)
| export callconv expent var :: [forall tyvar1 … tyvark .] ftype (expose variable, k ≥ 0)
```
---
In [ Section 10.5](http://www.haskell.org/onlinereport/haskell2010/haskellch10.html#TBL-105-153-):
Replace:
```
exp → infixexp :: [context =>] type (expression type signature)
```
with:
```
exp → infixexp :: [forall tyvar1 … tyvark .] [context =>] type (expression type signature, k ≥ 0)
```
## References
[ http://www.haskell.org/pipermail/haskell-prime/2009-June/002786.html](http://www.haskell.org/pipermail/haskell-prime/2009-June/002786.html)