Version 11 (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

## Variations

- Hugs requires that type signatures be unambiguous (taking into account FunctionalDependencies).
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
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

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 restrictions on the form of contexts are removed, context reduction is forced only by

- explicit signatures
- the type of
`main` - the MonomorphismRestriction
- the no-escape restriction on ExistentialQuantification
- 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:

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:data Foo = K Bar deriving Eq

- ground assertions are fully reduced, so that the following remains illegal:
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
- is required by OverlappingInstances

## Pros

- useful with FlexibleInstances

## Cons

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