2 Dec 23:07 2013

## existential quantification

Hi everybody,

I try to understand existential quantification. I have two questions.

1/ I have just read the answer of yairchu at

He writes:

"""
So with Existential-Quantification, foralls in data definitions mean that,
the value contained *can* be of *any* suitable type, not that it *must* be
of *all* suitable types.
"""

This made me think to an error I obtained with the code:
---------------
test :: Show s => s
test = "foobar"
---------------

The error is:

Could not deduce (s ~ [Char])
from the context (Show s)
bound by the type signature for test :: Show s => s
[...]
s' is a rigid type variable bound by
the type signature for test :: Show s => s


2 Dec 18:33 2013

### Re: existential quantification

On Mon, Dec 2, 2013 at 5:07 PM, TP wrote:
---------------
test :: Show s => s
test = "foobar"
---------------

The error is:

Could not deduce (s ~ [Char])
from the context (Show s)
bound by the type signature for test :: Show s => s
[...]
s' is a rigid type variable bound by
the type signature for test :: Show s => s

Indeed, test :: Show s => s means "for any type s which is an instance of
Show, test is a value of that type s". But for example "foobar" can't be an
Int that is an instance of Show, so it yields an error.
(...)
So I thought that by using existential quantification, the first example
could work:

---------------
{-# LANGUAGE ExistentialQuantification #-}

test :: forall s . Show s => s
test = "asd"
---------------

This is actually the same as the first one; top level type variables (that is, outside of parentheses) are always forall.

And just tossing a forall in there does not mean you can claim to be any type and then force a String down the caller's throat.

Which brings us to what is *really* going on. When you write

test :: Show s => s

you are saying exactly and only this:

Any function that calls me can request *any* type that has an instance of Show, and I will give them *that type*.

It still means that if you add an explicit forall.

It does not, nor can it be forced to mean, that you will only ever give them a String. Likewise, it does not, nor can it be forced to mean, that you can pick a different type based on (the value of a function parameter, the value of an environment variable, the phase of the moon).

Haskell does not use an OO type system; there is no java.lang.Object that can be every possible type, and forall does not create one. You cannot represent in Haskell the kind of type that you are trying to write. (There is something you can do that is almost the same, but requires a constraint and can only represent monomorphic types. And *still* does not give you java.lang.Object; it gives you a thing which has a specific type and "contains" a thing with another specific type, but can be queried about what that type is and can be extracted *only* in a context that requires that type.)

When forall is useful is inside parentheses in a type. I am not sure that I can provide a useful example that I can explain meaningfully until you understand the above. (But others here probably can....)

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"?

Because "there exists" and "for all" are related by DeMorgan's rule (think about it), and "for all" is easier to represent in GHC's type machinery. I believe UHC provides an "exists" type quantifier as well as "forall".

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.

"You don't have to keep two different kinds of quantification in mind, or figure out how they interact with each other and non-quantified types, since you can write one in terms of the other."

--
brandon s allbery kf8nh                               sine nomine associates
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net
_______________________________________________

3 Dec 04:53 2013

### Re: existential quantification

Brandon Allbery wrote:

> Which brings us to what is *really* going on. When you write
>
> test :: Show s => s
>
> you are saying exactly and only this:
>
> Any function that calls me can request *any* type that has an instance
> of Show, and I will give them *that type*.

Thanks Brandon for this interpretation. I have carefully written it in my

TP

2 Dec 18:47 2013

### Re: existential quantification

There is just one place where "forall" means "any suitable type", and that's in "data" (or "newtype")
declaration, BEFORE the data constructor. Like this:

newtype T = forall s. Show s => T s

Then you can have

test :: T
test = T "foobar".

If "forall" is AFTER the data constructor, it means that the value should have ALL suitable types
simultaniously. Like this:

data T = T (forall s. Show s => s).

Then you CAN'T have

test = T "foobar"

because "foobar" has only one type, String; it's not polymorphic. On the other hand, if you happen to have a
value of type T, you can treat the value inside it as a value of any suitable type, like this:

baz :: T -> String
baz (T s) = s

Same thing happens if you use "forall" without defining a new type, like

test :: forall s => Show s => s

It differs from the previous example just by one level of indirection, that's all.

On 03 Dec 2013, at 02:07, TP <paratribulations <at> free.fr> wrote:

> Hi everybody,
>
>
> I try to understand existential quantification. I have two questions.
>
> 1/ I have just read the answer of yairchu at
>
>
> He writes:
>
> """
> So with Existential-Quantification, foralls in data definitions mean that,
> the value contained *can* be of *any* suitable type, not that it *must* be
> of *all* suitable types.
> """
>
> This made me think to an error I obtained with the code:
> ---------------
> test :: Show s => s
> test = "foobar"
> ---------------
>
> The error is:
>
> Could not deduce (s ~ [Char])
> from the context (Show s)
> bound by the type signature for test :: Show s => s
> [...]
> s' is a rigid type variable bound by
> the type signature for test :: Show s => s
>
> Indeed, test :: Show s => s means "for any type s which is an instance of
> Show, test is a value of that type s". But for example "foobar" can't be an
> Int that is an instance of Show, so it yields an error.
> By comparison,
>
> ---------------
> test :: Num a => a
> test = 42
> ---------------
>
> works because 42 can be a value of type Int or Integer or Float or anything
> else that is an instance of Num.
> 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?
>
> 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
>
>
>
> """
> 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.
>
> Thanks in advance,
>
> TP
>
> _______________________________________________
> Haskell-Cafe mailing list

_______________________________________________

2 Dec 20:50 2013

### Re: existential quantification

Just expanding on Brandon's answer: DeMorgan's law he's referring to goes like this:
∀a.P(a) === ¬∃a.¬P(a) where 'a' is a sentence, so P is second order
A special case of this is this:
∀a.(R(a) -> Q) === ¬∃a.¬(R(a) -> Q) === ¬∃a.(R(a)∧¬Q) === ¬((∃a.R(a))∧¬Q) === (∃a.R(a)) -> Q   (i added extra parantheses for emphasis)
So what does this mean in terms of haskell? R(a) is your data definition's "body", and Q is the type you are defining. On the lhs the universally quantified version gives you the type of the constuctor you're defining, and on the rhs the existential tells you what you're constructing the type with.
Or in other words the universal version says: For any 'a' give me an R(a) and i'll give you back a Q.
The existential version says: If you have some 'a' for which R(a) i'll give you back a Q. (It's hard to phrase the difference without sounding stupid, they are equivalent after all).

There are of course other considerations, for example introducing 'exists' would mean another keyword in the syntax.

Having said that I think that the choice of 'forall' for -XExistentialQuantification is wrong, as the data body defines the type you're constructing with, not the type of the whole constructor. HOWEVER for -XGADTs forall makes perfect sense. Compare the following:

data AnyType = forall a. AnyType a
data AnyType where
AnyType :: forall a. a -> AnyType

These two definitions are operationally identical, but I think the GADT way is the one that actually corresponds to the DeMorgan law.

On 2 December 2013 22:07, TP wrote:
Hi everybody,

I try to understand existential quantification. I have two questions.

1/ I have just read the answer of yairchu at

He writes:

"""
So with Existential-Quantification, foralls in data definitions mean that,
the value contained *can* be of *any* suitable type, not that it *must* be
of *all* suitable types.
"""

This made me think to an error I obtained with the code:
---------------
test :: Show s => s
test = "foobar"
---------------

The error is:

Could not deduce (s ~ [Char])
from the context (Show s)
bound by the type signature for test :: Show s => s
[...]
s' is a rigid type variable bound by
the type signature for test :: Show s => s

Indeed, test :: Show s => s means "for any type s which is an instance of
Show, test is a value of that type s". But for example "foobar" can't be an
Int that is an instance of Show, so it yields an error.
By comparison,

---------------
test :: Num a => a
test = 42
---------------

works because 42 can be a value of type Int or Integer or Float or anything
else that is an instance of Num.
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?

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

"""
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.

TP

_______________________________________________

_______________________________________________

3 Dec 05:10 2013

### Re: existential quantification

Andras Slemmer wrote:

> Just expanding on Brandon's answer: DeMorgan's law he's referring to goes
> like this:
> ∀a.P(a) === ¬∃a.¬P(a) where 'a' is a sentence, so P is second order
> A special case of this is this:
> ∀a.(R(a) -> Q) === ¬∃a.¬(R(a) -> Q) === ¬∃a.(R(a)∧¬Q) === ¬((∃a.R(a))∧¬Q)
> === (∃a.R(a)) -> Q   (i added extra parantheses for emphasis)
> So what does this mean in terms of haskell? R(a) is your data definition's
> "body", and Q is the type you are defining. On the lhs the universally
> quantified version gives you the type of the constuctor you're defining,
> and on the rhs the existential tells you what you're constructing the type
> with.
> Or in other words the universal version says: For any 'a' give me an R(a)
> and i'll give you back a Q.
> The existential version says: If you have some 'a' for which R(a) i'll
> give you back a Q. (It's hard to phrase the difference without sounding
> stupid, they are equivalent after all).
>
> There are of course other considerations, for example introducing 'exists'
> would mean another keyword in the syntax.

Thanks Andras, I have understood the developments up to that point. But
below I do not understand your reasoning.

>
> Having said that I think that the choice of 'forall' for
> -XExistentialQuantification is wrong, as the data body defines the type
> you're constructing with, not the type of the whole constructor. HOWEVER
> for -XGADTs forall makes perfect sense. Compare the following:
>
> data AnyType = forall a. AnyType a
> data AnyType where
>   AnyType :: forall a. a -> AnyType
>
> These two definitions are operationally identical, but I think the GADT
> way is the one that actually corresponds to the DeMorgan law.

And one more question: I had lectures on logic some years ago, but I never
studied type theory at university (I'm some sort of "electrical engineer").
Is there around a good textbook for "beginners", with full proofs, but only
the essential ones? I would like a good "entry point" in the textbook
literature. Not for experts.
Are the books of Robert Harper suitable, for example

http://www.amazon.com/Practical-Foundations-Programming-Languages-Professor/dp/1107029570

?

TP

_______________________________________________

3 Dec 01:47 2013

### Re: existential quantification

> But below I do not understand your reasoning.

Given a datatype

data D = D Int

I call Int the type you're constructing D with, however the type of the constructor itself is Int -> D

In ghc haskell there is another way of defining the same type using GADTs alongside the above "haskell98" way:

data D where
D :: Int -> D

Notice how here we are explicitly typing the constructor.

The haskell98 way defines what your datatype D is isomorphic to - here it is Int, whereas the GADT way defines how to construct a D.

The problem haskell developers faced was that in order to use the haskell98 way for existentials they would've had to introduce an 'exists' quantifier, which would mess up a boatload of things in the type theory. Instead they introduced this forall hack that doesn't define an isomorphic type, rather it indicates that we are defining a way of constructing an existential.
I find this ugly because it breaks the isomorphism that the = sign indicates in a haskell98 definition.

The GADT way on the other hand is defining ways of construction, so a definition like:
data D2 where
D2 :: a -> D2
makes perfect sense

> Is there around a good textbook for "beginners", with full proofs, but only the essential ones?

Types and Programming Languages from Benjamin Pierce is a good one. I also plan to upload a short video lecture series from Harper on type theory (it assumes minimal knowledge of logic), i'll send you a link when it's up.

On 3 December 2013 04:10, TP wrote:
Andras Slemmer wrote:

> Just expanding on Brandon's answer: DeMorgan's law he's referring to goes
> like this:
> ∀a.P(a) === ¬∃a.¬P(a) where 'a' is a sentence, so P is second order
> A special case of this is this:
> ∀a.(R(a) -> Q) === ¬∃a.¬(R(a) -> Q) === ¬∃a.(R(a)∧¬Q) === ¬((∃a.R(a))∧¬Q)
> === (∃a.R(a)) -> Q   (i added extra parantheses for emphasis)
> So what does this mean in terms of haskell? R(a) is your data definition's
> "body", and Q is the type you are defining. On the lhs the universally
> quantified version gives you the type of the constuctor you're defining,
> and on the rhs the existential tells you what you're constructing the type
> with.
> Or in other words the universal version says: For any 'a' give me an R(a)
> and i'll give you back a Q.
> The existential version says: If you have some 'a' for which R(a) i'll
> give you back a Q. (It's hard to phrase the difference without sounding
> stupid, they are equivalent after all).
>
> There are of course other considerations, for example introducing 'exists'
> would mean another keyword in the syntax.

Thanks Andras, I have understood the developments up to that point. But
below I do not understand your reasoning.

>
> Having said that I think that the choice of 'forall' for
> -XExistentialQuantification is wrong, as the data body defines the type
> you're constructing with, not the type of the whole constructor. HOWEVER
> for -XGADTs forall makes perfect sense. Compare the following:
>
> data AnyType = forall a. AnyType a
> data AnyType where
>   AnyType :: forall a. a -> AnyType
>
> These two definitions are operationally identical, but I think the GADT
> way is the one that actually corresponds to the DeMorgan law.

And one more question: I had lectures on logic some years ago, but I never
studied type theory at university (I'm some sort of "electrical engineer").
Is there around a good textbook for "beginners", with full proofs, but only
the essential ones? I would like a good "entry point" in the textbook
literature. Not for experts.
Are the books of Robert Harper suitable, for example

http://www.amazon.com/Practical-Foundations-Programming-Languages-Professor/dp/1107029570

?

TP

_______________________________________________

_______________________________________________

3 Dec 07:36 2013

### Re: existential quantification

On Tue, Dec 3, 2013 at 11:10 AM, TP wrote:
I would like a good "entry point" in the textbook
literature. Not for experts.
Are the books of Robert Harper suitable, for example

http://www.amazon.com/Practical-Foundations-Programming-Languages-Professor/dp/1107029570

There's a draft copy on Harper's home page you can check out.

It's primarily a textbook for CS graduate students entering the specialization of PL.

-- Kim-Ee
_______________________________________________

4 Dec 00:35 2013

### Re: existential quantification

yeah, its not an introductory text, but it is a great grad level reference. (nb: i read a draft a few years ago, haven't read the published version... yet)

On Tue, Dec 3, 2013 at 1:36 AM, Kim-Ee Yeoh wrote:

On Tue, Dec 3, 2013 at 11:10 AM, TP wrote:
I would like a good "entry point" in the textbook
literature. Not for experts.
Are the books of Robert Harper suitable, for example

http://www.amazon.com/Practical-Foundations-Programming-Languages-Professor/dp/1107029570

There's a draft copy on Harper's home page you can check out.

It's primarily a textbook for CS graduate students entering the specialization of PL.

-- Kim-Ee

_______________________________________________

_______________________________________________

8 Dec 10:23 2013

### Re: existential quantification

I uploaded the Harper video series, here is a link to the first lecture: https://www.youtube.com/watch?v=ev7AYsLljxk&list=PL8Ky8lYL8-Oh7awp0sqa82o7Ggt4AGhyf&index=5
This is more of an introduction to dependent type theory, but it's worth a watch!

On 3 December 2013 04:10, TP wrote:
Andras Slemmer wrote:

> Just expanding on Brandon's answer: DeMorgan's law he's referring to goes
> like this:
> ∀a.P(a) === ¬∃a.¬P(a) where 'a' is a sentence, so P is second order
> A special case of this is this:
> ∀a.(R(a) -> Q) === ¬∃a.¬(R(a) -> Q) === ¬∃a.(R(a)∧¬Q) === ¬((∃a.R(a))∧¬Q)
> === (∃a.R(a)) -> Q   (i added extra parantheses for emphasis)
> So what does this mean in terms of haskell? R(a) is your data definition's
> "body", and Q is the type you are defining. On the lhs the universally
> quantified version gives you the type of the constuctor you're defining,
> and on the rhs the existential tells you what you're constructing the type
> with.
> Or in other words the universal version says: For any 'a' give me an R(a)
> and i'll give you back a Q.
> The existential version says: If you have some 'a' for which R(a) i'll
> give you back a Q. (It's hard to phrase the difference without sounding
> stupid, they are equivalent after all).
>
> There are of course other considerations, for example introducing 'exists'
> would mean another keyword in the syntax.

Thanks Andras, I have understood the developments up to that point. But
below I do not understand your reasoning.

>
> Having said that I think that the choice of 'forall' for
> -XExistentialQuantification is wrong, as the data body defines the type
> you're constructing with, not the type of the whole constructor. HOWEVER
> for -XGADTs forall makes perfect sense. Compare the following:
>
> data AnyType = forall a. AnyType a
> data AnyType where
>   AnyType :: forall a. a -> AnyType
>
> These two definitions are operationally identical, but I think the GADT
> way is the one that actually corresponds to the DeMorgan law.

And one more question: I had lectures on logic some years ago, but I never
studied type theory at university (I'm some sort of "electrical engineer").
Is there around a good textbook for "beginners", with full proofs, but only
the essential ones? I would like a good "entry point" in the textbook
literature. Not for experts.
Are the books of Robert Harper suitable, for example

http://www.amazon.com/Practical-Foundations-Programming-Languages-Professor/dp/1107029570

?

TP

_______________________________________________

_______________________________________________

2 Dec 21:30 2013

### Re: existential quantification

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
>
>
>
> """
> 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.

_______________________________________________

10 Jul 19:53 2008

### Existential quantification problem

Hello,

how do I unbox a existential quantificated data type?

> {-# LANGUAGE ExistentialQuantification #-}
> data L a = forall l. L (l a)
> unboxL (L l) = l

is giving me, in GHC:

Inferred type is less polymorphic than expected
Quantified type variable l' escapes
When checking an existential match that binds
l :: l t
The pattern(s) have type(s): L t
The body has type: l t
In the definition of unboxL': unboxL (L l) = l

Thanks.

--

--
﻿Marco Túlio Gontijo e Silva
Blog: http://marcotmarcot.blogspot.com/
Correio: marcot <at> riseup.net
XMPP: marcot <at> jabber.org
IRC: marcot <at> irc.freenode.net
Telefone: 25151920
Celular: 98116720
Endereço:
Rua Turfa, 639/701
Belo Horizonte/MG Brasil

10 Jul 19:59 2008

### Re: Existential quantification problem

On Thu, 2008-07-10 at 14:53 -0300, Marco Túlio Gontijo e Silva wrote:
> Hello,
>
> how do I unbox a existential quantificated data type?

You can't.  You have to use case analysis:

case foo of
L l -> <whatever you wanted to do>

where none of the information your case analysis discovers about the
actual type of l can be made available outside of the scope of the case
expression.  (It can't escape').  This is required for decidable static
typing, IIRC.

jcc

>
> > {-# LANGUAGE ExistentialQuantification #-}
> > data L a = forall l. L (l a)
> > unboxL (L l) = l
>
> is giving me, in GHC:
>
>     Inferred type is less polymorphic than expected
>       Quantified type variable l' escapes
>     When checking an existential match that binds
>         l :: l t
>     The pattern(s) have type(s): L t
>     The body has type: l t
>     In the definition of unboxL': unboxL (L l) = l
>
> Thanks.
>

14 Jul 01:28 2008

### Re: Existential quantification problem

On Thu, 2008-07-10 at 10:59 -0700, Jonathan Cast wrote:
> On Thu, 2008-07-10 at 14:53 -0300, Marco Túlio Gontijo e Silva wrote:
> > Hello,
> >
> > how do I unbox a existential quantificated data type?
>
> You can't.  You have to use case analysis:
>
>   case foo of
>     L l -> <whatever you wanted to do>
>
> where none of the information your case analysis discovers about the
> actual type of l can be made available outside of the scope of the case
> expression.  (It can't escape').  This is required for decidable static
> typing, IIRC.

It's not an extraneous requirement; it is part of the definition of
existential types.

14 Jul 01:50 2008

### Re: Existential quantification problem

On Sun, 2008-07-13 at 18:28 -0500, Derek Elkins wrote:
> On Thu, 2008-07-10 at 10:59 -0700, Jonathan Cast wrote:
> > On Thu, 2008-07-10 at 14:53 -0300, Marco Túlio Gontijo e Silva wrote:
> > > Hello,
> > >
> > > how do I unbox a existential quantificated data type?
> >
> > You can't.  You have to use case analysis:
> >
> >   case foo of
> >     L l -> <whatever you wanted to do>
> >
> > where none of the information your case analysis discovers about the
> > actual type of l can be made available outside of the scope of the case
> > expression.  (It can't escape').  This is required for decidable static
> > typing, IIRC.
>
> It's not an extraneous requirement; it is part of the definition of
> existential types.

I know that.  I didn't know implementing existential types was an end in itself, though.

jcc

14 Jul 03:03 2008

### Re: Existential quantification problem


On 2008 Jul 13, at 19:50, Jonathan Cast wrote:

> On Sun, 2008-07-13 at 18:28 -0500, Derek Elkins wrote:
>> On Thu, 2008-07-10 at 10:59 -0700, Jonathan Cast wrote:
>>> On Thu, 2008-07-10 at 14:53 -0300, Marco Túlio Gontijo e Silva
>>> wrote:
>>>> Hello,
>>>>
>>>> how do I unbox a existential quantificated data type?
>>>
>>> You can't.  You have to use case analysis:
>>>
>>>  case foo of
>>>    L l -> <whatever you wanted to do>
>>>
>>> where none of the information your case analysis discovers about the
>>> actual type of l can be made available outside of the scope of the
>>> case
>>> expression.  (It can't escape').  This is required for decidable
>>> static
>>> typing, IIRC.
>>
>> It's not an extraneous requirement; it is part of the definition of
>> existential types.
>
> I know that.  I didn't know implementing existential types was an
> end in itself, though.

No?  Consider ST.  Anytime you need to completely restrict access to
the innards of a datum, existential types are your friend.

--

--
brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery <at> kf8nh.com
system administrator [openafs,heimdal,too many hats] allbery <at> ece.cmu.edu
electrical and computer engineering, carnegie mellon university    KF8NH

14 Jul 03:16 2008

### Re: Existential quantification problem

On Sun, 2008-07-13 at 21:03 -0400, Brandon S. Allbery KF8NH wrote:
> On 2008 Jul 13, at 19:50, Jonathan Cast wrote:
>
> > On Sun, 2008-07-13 at 18:28 -0500, Derek Elkins wrote:
> >> On Thu, 2008-07-10 at 10:59 -0700, Jonathan Cast wrote:
> >>> On Thu, 2008-07-10 at 14:53 -0300, Marco Túlio Gontijo e Silva
> >>> wrote:
> >>>> Hello,
> >>>>
> >>>> how do I unbox a existential quantificated data type?
> >>>
> >>> You can't.  You have to use case analysis:
> >>>
> >>>  case foo of
> >>>    L l -> <whatever you wanted to do>
> >>>
> >>> where none of the information your case analysis discovers about the
> >>> actual type of l can be made available outside of the scope of the
> >>> case
> >>> expression.  (It can't escape').  This is required for decidable
> >>> static
> >>> typing, IIRC.
> >>
> >> It's not an extraneous requirement; it is part of the definition of
> >> existential types.
> >
> > I know that.  I didn't know implementing existential types was an
> > end in itself, though.
>
> No?  Consider ST.  Anytime you need to completely restrict access to
> the innards of a datum, existential types are your friend.

Right.  Mea culpa.

jcc

10 Jul 20:19 2008

### Re: Existential quantification problem

On Thursday 10 July 2008, Marco Túlio Gontijo e Silva wrote:
> Hello,
>
> how do I unbox a existential quantificated data type?
>
> > {-# LANGUAGE ExistentialQuantification #-}
> > data L a = forall l. L (l a)
> > unboxL (L l) = l
>
> is giving me, in GHC:
>
>     Inferred type is less polymorphic than expected
>       Quantified type variable l' escapes
>     When checking an existential match that binds
>         l :: l t
>     The pattern(s) have type(s): L t
>     The body has type: l t
>     In the definition of unboxL': unboxL (L l) = l

You don't. Or, at least, you don't do it that way. The point of an existential
is that the quantified type is 'forgotten', and there's no way to get it
back. That's good for abstraction, in that it restricts you to using some
provided interface that's guaranteed to work with the forgotten type, but it
means that you can't just take things out of the existential box.  Instead,
you have to use them in ways that make the forgotten type irrelevant (that
is, ways that are parametric in the corresponding type).

The type of the unboxL function in a type system with first-class existentials
is something like:

unboxL :: L a -> (exists l. l a)

Of course, GHC doesn't do first-class existentials, otherwise you'd probably
not be bothering with the datatype in the first place. :)

The proper way to eliminate an existential is (as mentioned above) with a
universal:

elim :: (exists l. l a) -> (forall l. l a -> r) -> r
elim e f = f e

Or, since existentials in GHC are restricted to data types:

elim :: L a -> (forall l. l a -> r) -> r
elim (L e) f = f e

Of course, as has already been noted,

elim foo (\l -> stuff)

is equivalent to:

case foo of
L l -> stuff

and doesn't need rank-2 polymorphism enabled, to boot. :)

-- Dan

10 Jul 20:39 2008

### Re: Existential quantification problem

On Thu, 10 July 2008, Marco Túlio Gontijo e Silva wrote:
> how do I unbox a existential quantificated data type?

Dan Doel wrote:
>    elim :: L a -> (forall l. l a -> r) -> r
>    elim (L e) f = f e

Just one catch: You can't actually write a function 'f' of type
(forall l. l a -> r) without knowing something about the forgotten
type of l.

One way to deal with this is by restricting the type of l in the data
declaration.  For example, you could restrict it to the typeclass
Foldable, and then you have access to the methods of that typeclass.

\begin{code}
{-# LANGUAGE ExistentialQuantification #-}

module Main
where

import qualified Data.Foldable as F

data L a = forall l. (F.Foldable l) => L (l a)

toList :: L a -> [a]
toList (L x) = F.foldr (:) [] x

main :: IO ()
main = do
let x = L [1..10]
print \$ toList x
\end{code}

`