Changes between Version 18 and Version 19 of ScopedTypeVariables


Ignore:
Timestamp:
Sep 8, 2006 10:50:20 AM (9 years ago)
Author:
ross@…
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • ScopedTypeVariables

    v18 v19  
    103103
    104104''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).
     105 * [wiki:RankNTypes] allows function types like
     106   {{{
     107shallowTerm :: (forall a. Data a => Maybe a) -> (forall b. Data b => b)
     108}}}
     109   in which referring to the type variable `b` seems to require a binding in a result type signature.
     110   In this case the `forall` and context can be floated out, but not if they were buried in a type synonym.
     111 * If there were a special syntax for binding type variables in existentials, pattern type signatures would be independent of type variable binding (and thus an othogonal design choice).
    106112 * 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.
    107113   {{{
    108114data Accum a = forall s. MkAccum s (a -> s -> s) (s -> a)
    109115
    110 f (forall s. MkAccum state add extr) = ...
     116f (forall s. MkAccum st a e) = ...
    111117}}}
    112118   (''Mutatis mutandi'' for other variants of ExistentialQuantification syntax.)
     119   With [wiki:GADTs] one can define existential types without explicit quantification, so the order of multiple type variables wouldn't be clear.
    113120
    114121== Pros ==