Changes between Version 17 and Version 18 of ScopedTypeVariables


Ignore:
Timestamp:
Sep 8, 2006 12:16:23 AM (9 years ago)
Author:
ross@…
Comment:

mention the promising GHC 6.6 story

Legend:

Unmodified
Added
Removed
Modified
  • ScopedTypeVariables

    v17 v18  
    1313Quantification of type variables over expressions is needed.
    1414
     15Proposal (see below for details):
     16 * extend the scope of type variables in `class` and `instance` heads.
     17 * allow bindings of type variables in type annotations, as in GHC 6.6, but with existential types handled by something other than pattern type signatures.
     18
    1519== References ==
    16  * [http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#scoped-type-variables GHC documentation] and [http://www.haskell.org/pipermail/glasgow-haskell-users/2006-January/009565.html a recent revision]
    1720 * [http://cvs.haskell.org/Hugs/pages/users_guide/type-annotations.html Hugs documentation]
     21 * [http://www.haskell.org/ghc/docs/6.4-latest/html/users_guide/type-extensions.html#scoped-type-variables GHC 6.4 documentation]
     22 * [http://www.haskell.org/ghc/dist/current/docs/users_guide/type-extensions.html#scoped-type-variables GHC 6.6 documentation]
    1823
    1924Note that although GHC and Hugs use the same syntax, the meaning of type variables is quite different, and there are other differences too.
     
    5257=== Type annotations ===
    5358
    54 GHC provides three extensions that bind type variables:
     59'''Hugs''' provides only one mechanism for binding type variables:
     60 * Pattern type signatures.
     61   Free variables in the type stand for distinct new type variables in the scope of the pattern, e.g.
     62   {{{
     63sortImage (f::a->b) = sortBy cmp
     64  where cmp :: a -> a -> Ordering
     65        cmp x y = compare (f x) (f y)
     66}}}
     67   That is, the type variables are rigid (universally quantified).
     68
     69'''GHC 6.4''' provides three extensions that bind type variables:
    5570
    5671 * Explicit `forall`s in type signature declarations.
     
    8095}}}
    8196In the latter two cases, the variable can stand for any type, not necessarily a type variable as in these examples, i.e. the variable is existentially quantified.
    82 In future versions of GHC, type variables will be rigid (universally quantified).
    83 Hugs supports only pattern type signatures, with rigid type variables.
     97
     98'''GHC 6.6''' allows binding via:
     99 * Explicit `forall`s in type signature declarations, as above.
     100
     101 * A mechanism to name type variables in [wiki:ExistentialQuantification existentially quantified types], currently by a version of pattern type signature; no other type variables in pattern type signatures produce bindings.
     102   This is sufficient if we assume MonomorphicPatternBindings.
     103
     104''Notes'':
     105 * If there were a special syntax for binding type variables in existentials, pattern type signatures would be independent of type variable binding (and thus a separate design choice).
     106 * If the language does not include [wiki:GADTs], such type variables could be bound with a new pattern syntax mimicking the `data` declaration, e.g.
     107   {{{
     108data Accum a = forall s. MkAccum s (a -> s -> s) (s -> a)
     109
     110f (forall s. MkAccum state add extr) = ...
     111}}}
     112   (''Mutatis mutandi'' for other variants of ExistentialQuantification syntax.)
    84113
    85114== Pros ==
     
    88117
    89118== Cons ==
    90   * Many different forms of scoped type variables in GHC makes them hard to reason about.
     119These apply to the GHC 6.4 version:
     120  * Many different forms of scoped type variables makes them hard to reason about.
    91121    For example:
    92122{{{
     
    104134    A rule like ExplicitQuantification might be needed if these were put into the standard.
    105135 
    106 == Alternative proposal 1 ==
     136== Alternative proposal ==
    107137
    108138Both let-bound and lambda-bound type variables are in scope in the
     
    120150
    121151(perhaps this text can be cleaned up further? what is a better term for expression type signature?)
    122 
    123 == Alternative proposal 2 ==
    124 
    125 Restrict the above extensions to:
    126  * for function bindings, optional explicit `forall`s in type signatures.
    127  * for pattern bindings, result type signatures.
    128    Explicit universal quantification might be made mandatory.
    129 plus binding of type variables in class and instance heads.