Changes between Version 8 and Version 9 of FlexibleInstances


Ignore:
Timestamp:
Mar 1, 2006 12:11:16 AM (10 years ago)
Author:
ross@…
Comment:

re=organize, adding non-local conditions

Legend:

Unmodified
Added
Removed
Modified
  • FlexibleInstances

    v8 v9  
    44== Brief Explanation ==
    55
    6 In Haskell 98,
    7  * an instance head must have the form C (T u,,1,, ... u,,k,,), where T is a type constructor defined by a `data` or `newtype` declaration (see TypeSynonymInstances) and the u,,i,, are distinct type variables, and
    8  * each assertion in the context must have the form C' v, where v is one of the u,,i,,.
    9 
    10 
    11 Without restrictions on the form of instances, constraint checking is undecidable (see UndecidableInstances).
    12 A conservative rule (used by GHC with `-fglasgow-exts`) that ensures termination is:
    13  * at least one of the type arguments of the instance head must be a non-variable type, and
    14  * each assertion in the context must have the form C v,,1,, ... v,,n,,, where the v,,i,, are distinct type variables.
    15 The distinctness requirement prohibits non-terminating instances like
    16 {{{
    17 instance C b b => C (Maybe a) b
    18 }}}
    19 Note that repeated type variables are permitted in the instance head, e.g.
     6Especially with MultiParamTypeClasses, we would like to write instances like
    207{{{
    218instance MArray (STArray s) e (ST s)
    229}}}
     10However without some restrictions constraint checking is undecidable.
    2311
    24 With this extension, one can write instances like
     12This page lists alternative proposals for liberalizing the form of instances while retaining sufficient restrictions to guarantee termination.
     13Such restrictions are necessarily conservative: there will always be programs that are clearly safe but still rejected.
     14Restrictions on the form of instances also restrict the forms of datatype declarations that can use `deriving` clause (see [http://www.haskell.org/onlinereport/decls.html#sect4.5.3 Context reduction errors] in the Haskell 98 Report).
     15
     16Note that if FunctionalDependencies are present, additional restrictions are required.
     17
     18See UndecidableInstances for an alternative strategy using dynamic constraints on context reduction.
     19
     20If one can write instances like
    2521{{{
    2622instance C [Bool] where ...
    2723instance C [Char] where ...
    2824}}}
    29 and assertions like `C [a]` can be neither reduced nor rejected, so FlexibleContexts are also needed.
     25then assertions like `C [a]` can be neither reduced nor rejected, so FlexibleContexts are also needed.
    3026
    3127== References ==
     
    3733[[TicketQuery(description~=FlexibleInstances)]]
    3834
    39 == Pros ==
    40  * Such instances often arise with MultiParamTypeClasses.
     35== Local termination conditions ==
    4136
    42 == Cons ==
    43  * The above restrictions rule out some useful instances, e.g. derived instances like:
    44    {{{
    45 data Sized s a = N Int (s a)
    46         deriving (Show)
     37The idea here is to impose restrictions on the form of each instance in isolation, such that context reduction will be guaranteed to terminate.
     38
     39=== Haskell 98 ===
     40 * an instance head must have the form C (T u,,1,, ... u,,k,,), where T is a type constructor defined by a `data` or `newtype` declaration (see TypeSynonymInstances) and the u,,i,, are distinct type variables, and
     41 * each assertion in the context must have the form C' v, where v is one of the u,,i,,.
     42
     43=== GHC 6.4 and earlier ===
     44 * at least one of the type arguments of the instance head must be a non-variable type, and
     45 * each assertion in the context must have the form C v,,1,, ... v,,n,,, where the v,,i,, are distinct type variables.
     46The distinctness requirement prohibits non-terminating instances like
     47{{{
     48instance C b b => C (Maybe a) b
    4749}}}
    48    remain illegal, because the inferred instance has an illegal context:
    49    {{{
    50 instance Show (s a) => Show (Sized s a)
    51 }}}
    52    (see [http://www.haskell.org/onlinereport/decls.html#sect4.5.3 Context reduction errors] in the Haskell 98 Report). The following examples from the GHC User's Guide are also forbidden:
    53    {{{
    54 instance C a
    55 instance (C1 a, C2 a, C3 a) => C a
    56 }}}
    57    The second of these cannot be shown to terminate without considering other instances in the program.
    5850
    59 == Relaxed termination condition ==
    60 An alternative rule would be that each assertion in the context must satisfy
     51=== GHC 6.5 ===
     52Each assertion in the context must satisfy
    6153 * no variable has more occurrences in the assertion than in the head, and
    6254 * the assertion has fewer constructors and variables (taken together and counting repetitions) than the head.
    6355(These conditions ensure that under any ground substitution, the assertion contains fewer constructors than the head.)
    6456
    65 This rule would allow instances accepted by the GHC rule and more, including
     57This rule allows instances accepted by the previous rule and more, including
    6658{{{
    6759instance C a
     
    7264instance C a a => C [a] [a]
    7365}}}
     66It also allows derived instances like
     67{{{
     68instance Show (s a) => Show (Sized s a)
     69    deriving (Show)
     70}}}
     71because the derived instance (above) has the required form.
     72
     73== Non-local termination conditions ==
     74
     75No local criterion can accept a definition like
     76{{{
     77instance (C1 a, C2 a, C3 a) => C a
     78}}}
     79because termination depends on other instances in the program.
     80However this is clearly safe if none of the instances for `C1`, `C2` or `C3` contain a direct or indirect constraint using `C`.
     81
     82The proposal is that one of the above local restrictions be used, but only on cycles of instances.
     83
     84This is more complex than a local criterion: the instance the compiler complains about might not be the one the programmer just added (creating a cycle), or even in the same module.