TP | 2 Dec 23:07 2013
Picon

existential quantification

Hi everybody,

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

1/ I have just read the answer of yairchu at

http://stackoverflow.com/questions/3071136/what-does-the-forall-keyword-in-haskell-ghc-do

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
(Continue reading)

Brandon Allbery | 2 Dec 18:33 2013
Picon

Re: existential quantification

On Mon, Dec 2, 2013 at 5:07 PM, TP <paratribulations <at> free.fr> 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
allbery.b <at> gmail.com                                  ballbery <at> sinenomine.net
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
TP | 3 Dec 04:53 2013
Picon

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 
Haskell notes.

TP
MigMit | 2 Dec 18:47 2013
Picon

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
> 
> http://stackoverflow.com/questions/3071136/what-does-the-forall-keyword-in-haskell-ghc-do
> 
> 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 
> 
> 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.
> 
> Thanks in advance,
> 
> TP
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Andras Slemmer | 2 Dec 20:50 2013
Picon

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

http://stackoverflow.com/questions/3071136/what-does-the-forall-keyword-in-haskell-ghc-do

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

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.

Thanks in advance,

TP

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
TP | 3 Dec 05:10 2013
Picon

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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Andras Slemmer | 3 Dec 01:47 2013
Picon

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 <paratribulations <at> free.fr> 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


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Kim-Ee Yeoh | 3 Dec 07:36 2013

Re: existential quantification


On Tue, Dec 3, 2013 at 11:10 AM, TP <paratribulations <at> free.fr> 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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Carter Schonwald | 4 Dec 00:35 2013
Picon

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 <ky3 <at> atamo.com> wrote:

On Tue, Dec 3, 2013 at 11:10 AM, TP <paratribulations <at> free.fr> 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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Andras Slemmer | 8 Dec 10:23 2013
Picon

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 <paratribulations <at> free.fr> 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


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Timon Gehr | 2 Dec 21:30 2013
Picon
Picon

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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Picon

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
Página: http://marcotmarcot.googlepages.com/
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
 Prado 30410-370
 Belo Horizonte/MG Brasil
Jonathan Cast | 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.
> 
Derek Elkins | 14 Jul 01:28 2008
Picon

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.
Jonathan Cast | 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
Brandon S. Allbery KF8NH | 14 Jul 03:03 2008
Picon

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
Jonathan Cast | 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
Dan Doel | 10 Jul 20:19 2008
Picon

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
Ronald Guida | 10 Jul 20:39 2008
Picon

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}

See also http://www.haskell.org/haskellwiki/Existential_type

Gmane