Changes between Version 17 and Version 18 of ExistentialQuantification


Ignore:
Timestamp:
Feb 15, 2006 4:06:25 AM (10 years ago)
Author:
john@…
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • ExistentialQuantification

    v17 v18  
    6161}}}
    6262  Existentials are subsumed by [wiki:GADTs].
     63
     64 use ExistentialQuantifier::
     65
     66  if exists quantifiers are allowed in any type, existential data types are
     67simply a special case of this.
     68
     69  {{{
     70data Foo = Foo (exists a . a -> a)
     71}}}
     72
     73  and they may be declared via type synonym as well
     74
     75  {{{
     76type Any = exists a . Num a => a
     77data Foo = Foo Any
     78}}}
     79
     80  if you with the quantifier to scope over multiple components of a data type,
     81you pull it in front of the constructor:
     82
     83  {{{
     84data Accum a = exists s. MkAccum s (a -> s -> s) (s -> a)
     85}}}
     86
     87  Note that this is the same syntax one would use when using existential
     88quantifiers in type signatures with the exists coming before the constructor:
     89
     90  {{{
     91foo :: Int -> (exists a . Either (a -> Char) a) -> Char
     92foo = ...
     93}}}
     94
     95  This is the syntax supported by jhc.
    6396
    6497== Variations ==