Changes between Version 17 and Version 18 of ScopedTypeVariables


Ignore:
Timestamp:
Sep 8, 2006 12:16:23 AM (8 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.