Changes between Version 4 and Version 5 of ExistentialQuantification


Ignore:
Timestamp:
Dec 1, 2005 11:41:19 AM (8 years ago)
Author:
ross@…
Comment:

incorporate material from ExistentialsVsPolymorphicComponents?

Legend:

Unmodified
Added
Removed
Modified
  • ExistentialQuantification

    v4 v5  
    66== Brief Explanation == 
    77 
    8 Local existential quantification of type variables in a data constructor, 
    9 introduced with `forall` before the data constructor, e.g. 
     8Existential quantification hides a type variable within a data constructor. 
     9The current syntax uses a `forall` before the data constructor, as in the following example , which packs a value together with operations on that value: 
    1010{{{ 
    1111data Accum a = forall s. MkAccum s (a -> s -> s) (s -> a) 
    1212}}} 
    13 The `forall` is justified by the type of the data constructor: 
     13When a value of this type is constructed, `s` will be instantiated to some concrete type. When such a value is analysed, `s` is abstract. 
     14 
     15The `forall` hints at the polymorphic type of the data constructor: 
    1416{{{ 
    1517MkAccum :: s -> (a -> s -> s) -> (s -> a) -> Accum a 
    1618}}} 
    17 but [http://www.haskell.org/pipermail/haskell/2003-June/011995.html some have suggested] using `exists` instead to avoid confusion with PolymorphicComponents. 
     19but see below for alternatives. 
     20 
    1821== References == 
    1922 * [http://www.cs.luc.edu/users/laufer/papers/toplas94.pdf Polymorphic Type Inference and Abstract Data Types] by K. Läufer and M. Odersky, in TOPLAS, Sep 1994. 
    2023 * [http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#existential-quantification GHC documentation] 
    21  * ExistentialsVsPolymorphicComponents 
     24 * distinguish from PolymorphicComponents 
     25 
     26== Syntax of existentials == 
     27 
     28Several possibilities have been proposed: 
     29 
     30implicit quantification:: 
     31  {{{ 
     32data Accum a = MkAccum s (a -> s -> s) (s -> a) 
     33}}} 
     34  As the type variable `s` does not appear on the left hand side, it is considered to be existentially quantified. 
     35  The main counterargument is that one can easily introduce an existential type by forgetting an argument to the data type. Error messages might confuse the novice programmer. 
     36 
     37`forall` before the constructor:: 
     38  {{{ 
     39data Accum a = forall s. MkAccum s (a -> s -> s) (s -> a) 
     40}}} 
     41  This is the currently implemented syntax, motivated by the type of the data constructor, but it can be confused with PolymorphicComponents. 
     42 
     43`exists` before the constructor:: 
     44  {{{ 
     45data Accum a = exists s. MkAccum s (a -> s -> s) (s -> a) 
     46}}} 
     47  which reinforces the connection to existential types. When analysing such a value, you know only that there exists some type `s` such that the arguments have these types. 
     48Reserves an extra word. 
     49 
     50[wiki:GADTs GADT] syntax:: 
     51  {{{ 
     52data Accum :: * -> * where 
     53    MkAccum :: s -> (a -> s -> s) -> (s -> a) -> Accum a 
     54}}} 
     55  Existentials are subsumed by [wiki:GADTs]. 
    2256 
    2357== Variations == 
     
    4781}}} 
    4882 
     83 
     84 
     85 
     86 
    4987== Pros == 
    5088 * quite handy for representations that delay composition or application, e.g. objects, various parser combinator libraries from Utrecht.