Changes between Version 17 and Version 18 of ScopedTypeVariables

Sep 8, 2006 12:16:23 AM (11 years ago)

mention the promising GHC 6.6 story


  • ScopedTypeVariables

    v17 v18  
    1313Quantification of type variables over expressions is needed.
     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.
    1519== References ==
    16  * [ GHC documentation] and [ a recent revision]
    1720 * [ Hugs documentation]
     21 * [ GHC 6.4 documentation]
     22 * [ GHC 6.6 documentation]
    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 ===
    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)
     67   That is, the type variables are rigid (universally quantified).
     69'''GHC 6.4''' provides three extensions that bind type variables:
    5671 * Explicit `forall`s in type signature declarations.
    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.
     98'''GHC 6.6''' allows binding via:
     99 * Explicit `forall`s in type signature declarations, as above.
     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.
     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)
     110f (forall s. MkAccum state add extr) = ...
     112   (''Mutatis mutandi'' for other variants of ExistentialQuantification syntax.)
    85114== Pros ==
    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:
    104134    A rule like ExplicitQuantification might be needed if these were put into the standard.
    106 == Alternative proposal 1 ==
     136== Alternative proposal ==
    108138Both let-bound and lambda-bound type variables are in scope in the
    121151(perhaps this text can be cleaned up further? what is a better term for expression type signature?)
    123 == Alternative proposal 2 ==
    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.