Version 9 (modified by ross@…, 9 years ago) (diff) |
---|

# 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_{1}... t_{n}), 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.

g :: (C [a], D (a -> b)) => [a] -> b

(Similar relaxation of `instance` declarations leads to UndecidableInstances.
Contexts on `newtype` and `data` declarations are RemovalCandidates.)

## References

- Syntax of Class Assertions and Contexts in the Haskell 98 Report
- Type classes: exploring the design space by Simon Peyton Jones, Mark Jones and Erik Meijer, Haskell Workshop 1997.
- Type signatures in the GHC User's Guide

## Tickets

- #31
- add Flexible Contexts

## 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

module M where class C a where c_method :: a -> Bool foo xs = c_method (tail xs)

the context of the inferred type

foo :: C [a] => [a] -> Bool

is neither allowed nor reducible, so a missing instance `C [a]` is reported.

When contexts are unrestricted, context reduction is forced only by explicit signatures and the type of `main`.
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:

module Main where import M instance C [a] where c_method = null main :: IO () main = print (foo "abc")

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
- is required by OverlappingInstances

In GHC and Hugs, the contexts of derived instances are fully reduced, so the following instance is allowed only if the instance `Eq Bar` is in scope:

data Foo = K Bar deriving Eq

## Pros

- useful with FlexibleInstances

## Cons

- complicated context reduction story
- deferred error checking (FunctionalDependencies can ameliorate this)