[Haskell-cafe] existential quantification
Timon Gehr
timon.gehr at gmx.ch
Mon Dec 2 20:30:23 UTC 2013
On 12/02/2013 11:07 PM, TP wrote:
> ...
> So I thought that by using existential quantification, the first example
> could work:
>
> ---------------
> {-# LANGUAGE ExistentialQuantification #-}
>
> test :: forall s . Show s => s
> test = "asd"
> ---------------
>
> But I obtain the same error, why?
>
This still says that 'test' is a value of type 's' for all 's' with a
'Show' instance.
Basically, 'test' gets a type 's', an instance 'Show s' and we get a
value of type 's'.
> 2/
> Is the notion of existential type related in some way to the classical
> mathematical quantifier "∃" (Unicode symbol U+2203: "There exists")?
> If yes, then why using "forall" for an "existential type"?
>
> At the following address
>
> http://www.haskell.org/ghc/docs/6.12.1/html/users_guide/data-type-extensions.html#existential
>
> we read
>
> """
> 7.4.4.1. Why existential?
>
> What has this to do with existential quantification? Simply that MkFoo has
> the (nearly) isomorphic type
>
> MkFoo :: (exists a . (a, a -> Bool)) -> Foo
>
> But Haskell programmers can safely think of the ordinary universally
> quantified type given above, thereby avoiding adding a new existential
> quantification construct.
> """
>
> But I don't understand the explanation.
>
Generally speaking, a typing judgement
x :: A
can be interpreted as a proof that type 'A' is inhabited, or in other
words, there exists a value of type 'A'. (Of course in Haskell this fact
alone is trivial due to 'undefined', but additional reasoning could
render it meaningful. For the remainder I'll just ignore the issue of
lifting.)
This is somewhat related to classical existential quantification, but it
is stronger in a sense, since it says that we know how to construct such
a value. (The classical version in general just says that the assumption
that there is no such value leads to a contradiction.)
Pattern matching allows one to get back the original constructor and the
arguments used to construct a value of some ADT type. A universal
quantifier over a type states that we can provide any type and obtain a
value of the type provided in the body where all instances of the bound
variable are replaced by our type. I.e. you can interpret forall a.
(...) as stating that a value of that type takes an additional implicit
argument 'a' at type level.
Now MkFoo is declared as follows:
data Foo = forall a. MkFoo a (a -> Bool)
| Nil
Which gives it the type:
MkFoo :: forall a. a -> (a -> Bool) -> Foo
I.e. it gets a type 'a' a value of that type and a decidable predicate
ranging over that type and constructs a value of type 'Foo'. Pattern
matching (roughly speaking) does the opposite: It gets you back a type,
a value of that type and the predicate.
The type is called nearly isomorphic to the explicit existential type,
because using some rounds of pattern matching one would also recover the
same kinds of objects.
I.e. existential quantification can be thought of as being left implicit
in the typing judgement, but 'forall' is needed in order to make
explicit the scope of the type variable, which otherwise would range
over the entire data declaration instead of just a single constructor.
-XExistentialQuantification enables uses of 'forall' necessary for using
existential quantification.
More information about the Haskell-Cafe
mailing list