Changes between Version 4 and Version 5 of ExistentialQuantification
 Timestamp:
 Dec 1, 2005 11:41:19 AM (12 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

ExistentialQuantification
v4 v5 6 6 == Brief Explanation == 7 7 8 Local existential quantification of type variables in a data constructor, 9 introduced with `forall` before the data constructor, e.g. 8 Existential quantification hides a type variable within a data constructor. 9 The current syntax uses a `forall` before the data constructor, as in the following example , which packs a value together with operations on that value: 10 10 {{{ 11 11 data Accum a = forall s. MkAccum s (a > s > s) (s > a) 12 12 }}} 13 The `forall` is justified by the type of the data constructor: 13 When 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 15 The `forall` hints at the polymorphic type of the data constructor: 14 16 {{{ 15 17 MkAccum :: s > (a > s > s) > (s > a) > Accum a 16 18 }}} 17 but [http://www.haskell.org/pipermail/haskell/2003June/011995.html some have suggested] using `exists` instead to avoid confusion with PolymorphicComponents. 19 but see below for alternatives. 20 18 21 == References == 19 22 * [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. 20 23 * [http://www.haskell.org/ghc/docs/latest/html/users_guide/typeextensions.html#existentialquantification GHC documentation] 21 * ExistentialsVsPolymorphicComponents 24 * distinguish from PolymorphicComponents 25 26 == Syntax of existentials == 27 28 Several possibilities have been proposed: 29 30 implicit quantification:: 31 {{{ 32 data 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 {{{ 39 data 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 {{{ 45 data 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. 48 Reserves an extra word. 49 50 [wiki:GADTs GADT] syntax:: 51 {{{ 52 data Accum :: * > * where 53 MkAccum :: s > (a > s > s) > (s > a) > Accum a 54 }}} 55 Existentials are subsumed by [wiki:GADTs]. 22 56 23 57 == Variations == … … 47 81 }}} 48 82 83 84 85 86 49 87 == Pros == 50 88 * quite handy for representations that delay composition or application, e.g. objects, various parser combinator libraries from Utrecht.