|
|
|
|
|
|
|
|
|
|
|
# Flexible Contexts
|
|
|
|
|
|
|
|
|
## Brief Explanation
|
|
|
|
|
|
|
|
|
|
|
|
In Haskell 98,
|
|
|
|
|
|
|
|
|
- contexts of type signatures, `newtype` and `data` declarations consist of assertions of the form C v or C (v t<sub>1</sub> … t<sub>n</sub>), where v is a type variable.
|
|
|
- contexts of `instance` and `class` declarations consist of assertions of the form C v, where v is a type variable.
|
|
|
|
|
|
|
|
|
The proposal is that class arguments in contexts of type signatures and `class` declarations may be arbitrary types, e.g.
|
|
|
|
|
|
|
|
|
```wiki
|
|
|
g :: (C [a], D (a -> b)) => [a] -> b
|
|
|
```
|
|
|
|
|
|
|
|
|
(Similar relaxation of `instance` declarations leads to [UndecidableInstances](undecidable-instances).
|
|
|
Contexts on `newtype` and `data` declarations are [RemovalCandidates](removal-candidates).)
|
|
|
|
|
|
|
|
|
## References
|
|
|
|
|
|
|
|
|
- [ Syntax of Class Assertions and Contexts](http://www.haskell.org/onlinereport/decls.html#sect4.1.3) in the Haskell 98 Report
|
|
|
- [ Type classes: exploring the design space](http://research.microsoft.com/Users/simonpj/Papers/type-class-design-space/) by Simon Peyton Jones, Mark Jones and Erik Meijer, Haskell Workshop 1997.
|
|
|
- [ Type signatures](http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#type-restrictions) in the GHC User's Guide
|
|
|
|
|
|
## Tickets
|
|
|
|
|
|
|
|
|
|
|
|
<table><tr><th>[\#31](https://gitlab.haskell.org//haskell/prime/issues/31)</th>
|
|
|
<td>add Flexible Contexts</td></tr></table>
|
|
|
|
|
|
|
|
|
|
|
|
## Variations
|
|
|
|
|
|
|
|
|
- Hugs requires that type signatures be unambiguous (taking into account [FunctionalDependencies](functional-dependencies)).
|
|
|
GHC requires only that type variables in the context be connected (by a chain of assertions) with type variables that occur in the head, so that it accepts
|
|
|
|
|
|
```wiki
|
|
|
foo :: (C a b, C b c) => c -> Bool
|
|
|
```
|
|
|
|
|
|
even though such functions cannot be used without ambiguity.
|
|
|
|
|
|
- GHC (but not Hugs) requires that the context contain at least one type variables that is universally quantified at that point.
|
|
|
This is consistent with rejecting inferred types containing irreducible ground assertions (like `Num Char`, see below), which both GHC and Hugs do.
|
|
|
|
|
|
## Context reduction
|
|
|
|
|
|
|
|
|
|
|
|
Haskell computes a type for each variable bound by `let` or `where`,
|
|
|
and then generalizes this type.
|
|
|
In Haskell 98, the allowed contexts are restricted, so contexts are reduced using `instance` declarations (and duplicate assertions and those implied by `class` contexts are removed) until either they are in the allowed form or no instance is applicable, in which case an error is reported. For example, in the following
|
|
|
|
|
|
|
|
|
```wiki
|
|
|
module M where
|
|
|
class C a where c_method :: a -> Bool
|
|
|
foo xs = c_method (tail xs)
|
|
|
```
|
|
|
|
|
|
|
|
|
the context of the inferred type
|
|
|
|
|
|
|
|
|
```wiki
|
|
|
foo :: C [a] => [a] -> Bool
|
|
|
```
|
|
|
|
|
|
|
|
|
is neither allowed nor reducible, so a missing instance `C [a]` is reported.
|
|
|
|
|
|
|
|
|
|
|
|
When restrictions on the form of contexts are removed, context reduction is forced only by
|
|
|
|
|
|
|
|
|
- explicit signatures
|
|
|
- the type of `main`
|
|
|
- the [MonomorphismRestriction](monomorphism-restriction)
|
|
|
- the no-escape restriction on [ExistentialQuantification](existential-quantification)
|
|
|
- the few remaining restrictions on contexts
|
|
|
|
|
|
|
|
|
The above example becomes legal; if a matching instance is in scope when context reduction is forced on uses of `foo`, they will also typecheck:
|
|
|
|
|
|
|
|
|
```wiki
|
|
|
module Main where
|
|
|
|
|
|
import M
|
|
|
|
|
|
instance C [a] where c_method = null
|
|
|
|
|
|
main :: IO ()
|
|
|
main = print (foo "abc")
|
|
|
```
|
|
|
|
|
|
|
|
|
The exceptions in GHC and Hugs are:
|
|
|
|
|
|
|
|
|
- contexts of derived instances are fully reduced, so the following instance is allowed only if the instance `Eq Bar` is in scope:
|
|
|
|
|
|
```wiki
|
|
|
data Foo = K Bar deriving Eq
|
|
|
```
|
|
|
- ground assertions are fully reduced, so that the following remains illegal:
|
|
|
|
|
|
```wiki
|
|
|
foo x = x + 'a'
|
|
|
```
|
|
|
|
|
|
|
|
|
Delaying context reduction:
|
|
|
|
|
|
|
|
|
- can leave contexts more complex (could interact with the Monomorphism Restriction)
|
|
|
- delays (and sometimes avoids) type errors
|
|
|
- sometimes avoids nontermination of context reduction for [UndecidableInstances](undecidable-instances)
|
|
|
- is required by [OverlappingInstances](overlapping-instances)
|
|
|
|
|
|
## Pros
|
|
|
|
|
|
|
|
|
- useful with [FlexibleInstances](flexible-instances)
|
|
|
|
|
|
## Cons
|
|
|
|
|
|
|
|
|
- complicated context reduction story
|
|
|
- deferred error checking ([FunctionalDependencies](functional-dependencies) can ameliorate this) |