Changes between Version 17 and Version 18 of ScopedTypeVariables
 Timestamp:
 Sep 8, 2006 12:16:23 AM (9 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

ScopedTypeVariables
v17 v18 13 13 Quantification of type variables over expressions is needed. 14 14 15 Proposal (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 15 19 == References == 16 * [http://www.haskell.org/ghc/docs/latest/html/users_guide/typeextensions.html#scopedtypevariables GHC documentation] and [http://www.haskell.org/pipermail/glasgowhaskellusers/2006January/009565.html a recent revision]17 20 * [http://cvs.haskell.org/Hugs/pages/users_guide/typeannotations.html Hugs documentation] 21 * [http://www.haskell.org/ghc/docs/6.4latest/html/users_guide/typeextensions.html#scopedtypevariables GHC 6.4 documentation] 22 * [http://www.haskell.org/ghc/dist/current/docs/users_guide/typeextensions.html#scopedtypevariables GHC 6.6 documentation] 18 23 19 24 Note that although GHC and Hugs use the same syntax, the meaning of type variables is quite different, and there are other differences too. … … 52 57 === Type annotations === 53 58 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 {{{ 63 sortImage (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: 55 70 56 71 * Explicit `forall`s in type signature declarations. … … 80 95 }}} 81 96 In 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 {{{ 108 data Accum a = forall s. MkAccum s (a > s > s) (s > a) 109 110 f (forall s. MkAccum state add extr) = ... 111 }}} 112 (''Mutatis mutandi'' for other variants of ExistentialQuantification syntax.) 84 113 85 114 == Pros == … … 88 117 89 118 == Cons == 90 * Many different forms of scoped type variables in GHC makes them hard to reason about. 119 These apply to the GHC 6.4 version: 120 * Many different forms of scoped type variables makes them hard to reason about. 91 121 For example: 92 122 {{{ … … 104 134 A rule like ExplicitQuantification might be needed if these were put into the standard. 105 135 106 == Alternative proposal 1==136 == Alternative proposal == 107 137 108 138 Both letbound and lambdabound type variables are in scope in the … … 120 150 121 151 (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.