Data structure containing elements which are instances of the same type class

newer
Wanted: Haskell binding for libbdd...

oleg＠okmij.org

11 Aug 2012 11 Aug '12

4:14 a.m.

data A = A deriving Show data B = B deriving Show data C = C deriving Show

data Foo = forall a. Show a => MkFoo a (Int -> Bool)

instance Show Foo where show (MkFoo a f) = show a

I'd like to point out that the only operation we can do on the first argument of MkFoo is to show to it. This is all we can ever do: we have no idea of its type but we know we can show it and get a String. Why not to apply show to start with (it won't be evaluated until required anyway)? Therefore, the data type Foo above is in all respects equivalent to

...

data Foo = MkFoo String (Int -> Bool)

and no existentials are ever needed. The following article explains elimination of existentials in more detail, touching upon the original problem, of bringing different types into union. http://okmij.org/ftp/Computation/Existentials.html

Show replies by date

David Feuer

11 Aug 11 Aug

12:58 p.m.

Has anyone used existential types to represent items on a schedule in a scheduled lazy data structure? On Aug 11, 2012 4:15 AM, wrote:

...

...
data A = A deriving Show data B = B deriving Show data C = C deriving Show

data Foo = forall a. Show a => MkFoo a (Int -> Bool)

instance Show Foo where show (MkFoo a f) = show a

I'd like to point out that the only operation we can do on the first argument of MkFoo is to show to it. This is all we can ever do: we have no idea of its type but we know we can show it and get a String. Why not to apply show to start with (it won't be evaluated until required anyway)? Therefore, the data type Foo above is in all respects equivalent to

...
data Foo = MkFoo String (Int -> Bool)

and no existentials are ever needed. The following article explains elimination of existentials in more detail, touching upon the original problem, of bringing different types into union.

http://okmij.org/ftp/Computation/Existentials.html

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

Patrick Palka

1:33 p.m.

On Sat, Aug 11, 2012 at 4:14 AM, wrote:

...

I'd like to point out that the only operation we can do on the first argument of MkFoo is to show to it. This is all we can ever do: we have no idea of its type but we know we can show it and get a String.

That's not all you can do: you can also pass the first argument of MkFoo to a function that expects a Show a => a argument, like the function 'print'. Can you do that with just a String (that represents show x for some x)?

Antoine Latter

3:01 p.m.

It should be pretty easy to write an adapter function of type "String -> (Show a => a)". On Aug 11, 2012 12:34 PM, "Patrick Palka" wrote:

...

On Sat, Aug 11, 2012 at 4:14 AM, wrote:

...
I'd like to point out that the only operation we can do on the first argument of MkFoo is to show to it. This is all we can ever do: we have no idea of its type but we know we can show it and get a String.

That's not all you can do: you can also pass the first argument of MkFoo to a function that expects a Show a => a argument, like the function 'print'. Can you do that with just a String (that represents show x for some x)?

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

Alexander Solla

4:08 p.m.

On Sat, Aug 11, 2012 at 12:01 PM, Antoine Latter wrote:

...

It should be pretty easy to write an adapter function of type "String -> (Show a => a)".

Not with that type. Give it a try. Hint: what is the extension of the type variable 'a'? What do you know about it? How would you use that to write the function?

Heinrich Apfelmus

12 Aug 12 Aug

3:24 a.m.

Antoine Latter wrote:

...

It should be pretty easy to write an adapter function of type "String -> (Show a => a)".

The type needs to be String -> (exists a. Show a => a) which is equivalent to String -> (forall a. Show a => a -> c) -> c Here is the implementation of the adapter newtype ExistsShow = E { showE :: String } instance Show ExistsShow where show = showE withShow :: String -> (forall a. Show a => a -> c) -> c withShow s f = f (E s) Essentially, the point is that the types are equivalent ExistsShow == exists a. Show a => a Best regards, Heinrich Apfelmus -- http://apfelmus.nfshost.com

Daniel Trstenjak

4:34 a.m.

Hi Oleg, On Sat, Aug 11, 2012 at 08:14:47AM -0000, oleg@okmij.org wrote:

...

I'd like to point out that the only operation we can do on the first argument of MkFoo is to show to it. This is all we can ever do: we have no idea of its type but we know we can show it and get a String. Why not to apply show to start with (it won't be evaluated until required anyway)?

It's only a test case. The real thing is for a game and will be something like: class EntityT e where update :: e -> e render :: e -> IO () handleEvent :: e -> Event -> e getBound :: e -> Maybe Bound data Entity = forall e. (EntityT e) => Entity e data Level = Level { entities = [Entity], ... } Greetings, Daniel

Johan Holmquist

13 Aug 13 Aug

1:38 p.m.

That pattern looks so familiar. :) Existential types seem to fit in to the type system really well so I never got why it is not part of the standard. On Aug 12, 2012 10:36 AM, "Daniel Trstenjak" wrote:

...

Hi Oleg,

On Sat, Aug 11, 2012 at 08:14:47AM -0000, oleg@okmij.org wrote:

...
I'd like to point out that the only operation we can do on the first argument of MkFoo is to show to it. This is all we can ever do: we have no idea of its type but we know we can show it and get a String. Why not to apply show to start with (it won't be evaluated until required anyway)?

It's only a test case. The real thing is for a game and will be something like:

class EntityT e where update :: e -> e

render :: e -> IO ()

handleEvent :: e -> Event -> e

getBound :: e -> Maybe Bound

data Entity = forall e. (EntityT e) => Entity e

data Level = Level { entities = [Entity], ... }

Greetings, Daniel

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

Jay Sulzberger

3:30 p.m.

On Mon, 13 Aug 2012, Johan Holmquist wrote:

...

That pattern looks so familiar. :) Existential types seem to fit in to the type system really well so I never got why it is not part of the standard. On Aug 12, 2012 10:36 AM, "Daniel Trstenjak" wrote:

Does Haskell have a word for "existential type" declaration? I have the impression, and this must be wrong, that "forall" does double duty, that is, it declares a "for all" in some sense like the usual "for all" of the Lower Predicate Calculus, perhaps the "for all" of system F, or something near it. oo--JS.

...

...
Hi Oleg,

On Sat, Aug 11, 2012 at 08:14:47AM -0000, oleg@okmij.org wrote:

...
I'd like to point out that the only operation we can do on the first argument of MkFoo is to show to it. This is all we can ever do: we have no idea of its type but we know we can show it and get a String. Why not to apply show to start with (it won't be evaluated until required anyway)?

It's only a test case. The real thing is for a game and will be something like:

class EntityT e where update :: e -> e

render :: e -> IO ()

handleEvent :: e -> Event -> e

getBound :: e -> Maybe Bound

data Entity = forall e. (EntityT e) => Entity e

data Level = Level { entities = [Entity], ... }

Greetings, Daniel

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

Ryan Ingram

6:07 p.m.

On Mon, Aug 13, 2012 at 12:30 PM, Jay Sulzberger wrote:

...

Does Haskell have a word for "existential type" declaration? I have the impression, and this must be wrong, that "forall" does double duty, that is, it declares a "for all" in some sense like the usual "for all" of the Lower Predicate Calculus, perhaps the "for all" of system F, or something near it.

It's using the forall/exists duality: exsts a. P(a) <=> forall r. (forall a. P(a) -> r) -> r For example: (exists a. Show a => a) <=> forall r. (forall a. Show a => a -> r) -> r This also works when you look at the type of a constructor: data Showable = forall a. Show a => MkShowable a -- MkShowable :: forall a. Show a => a -> Showable caseShowable :: forall r. (forall a. Show a => a -> r) -> Showable -> r caseShowable k (MkShowable x) = k x testData :: Showable testData = MkShowable (1 :: Int) useData :: Int useData = case testData of (MkShowable x) -> length (show x) useData2 :: Int useData2 = caseShowable (length . show) testData Haskell doesn't currently have first class existentials; you need to wrap them in an existential type like this. Using 'case' to pattern match on the constructor unwraps the existential and makes any packed-up constraints available to the right-hand-side of the case. An example of existentials without using constraints directly: data Stream a = forall s. MkStream s (s -> Maybe (a,s)) viewStream :: Stream a -> Maybe (a, Stream a) viewStream (MkStream s k) = case k s of Nothing -> Nothing Just (a, s') -> Just (a, MkStream s' k) takeStream :: Int -> Stream a -> [a] takeStream 0 _ = [] takeStream n s = case viewStream s of Nothing -> [] Just (a, s') -> a : takeStream (n-1) s' fibStream :: Stream Integer fibStream = Stream (0,1) (\(x,y) -> Just (x, (y, x+y))) Here the 'constraint' made visible by pattern matching on MkStream (in viewStream) is that the "s" type stored in the stream matches the "s" type taken and returned by the 'get next element' function. This allows the construction of another stream with the same function but a new state -- MkStream s' k. It also allows the stream function in fibStream to be non-recursive which greatly aids the GHC optimizer in certain situations. -- ryan

Jay Sulzberger

9:25 p.m.

On Mon, 13 Aug 2012, Ryan Ingram wrote:

...

On Mon, Aug 13, 2012 at 12:30 PM, Jay Sulzberger wrote:

...
Does Haskell have a word for "existential type" declaration? I have the impression, and this must be wrong, that "forall" does double duty, that is, it declares a "for all" in some sense like the usual "for all" of the Lower Predicate Calculus, perhaps the "for all" of system F, or something near it.

It's using the forall/exists duality: exsts a. P(a) <=> forall r. (forall a. P(a) -> r) -> r

;) This is, I think, a good joke. It has taken me a while, but I now understand that one of the most attractive things about Haskell is its sense of humor, which is unfailing. I will try to think about this, after trying your examples. I did suspect that, in some sense, "constraints" in combination with "forall" could give the quantifier "exists". Thanks, ryan! oo--JS.

...

For example: (exists a. Show a => a) <=> forall r. (forall a. Show a => a -> r) -> r

This also works when you look at the type of a constructor:

data Showable = forall a. Show a => MkShowable a -- MkShowable :: forall a. Show a => a -> Showable

caseShowable :: forall r. (forall a. Show a => a -> r) -> Showable -> r caseShowable k (MkShowable x) = k x

testData :: Showable testData = MkShowable (1 :: Int)

useData :: Int useData = case testData of (MkShowable x) -> length (show x)

useData2 :: Int useData2 = caseShowable (length . show) testData

Haskell doesn't currently have first class existentials; you need to wrap them in an existential type like this. Using 'case' to pattern match on the constructor unwraps the existential and makes any packed-up constraints available to the right-hand-side of the case.

An example of existentials without using constraints directly:

data Stream a = forall s. MkStream s (s -> Maybe (a,s))

viewStream :: Stream a -> Maybe (a, Stream a) viewStream (MkStream s k) = case k s of Nothing -> Nothing Just (a, s') -> Just (a, MkStream s' k)

takeStream :: Int -> Stream a -> [a] takeStream 0 _ = [] takeStream n s = case viewStream s of Nothing -> [] Just (a, s') -> a : takeStream (n-1) s'

fibStream :: Stream Integer fibStream = Stream (0,1) (\(x,y) -> Just (x, (y, x+y)))

Here the 'constraint' made visible by pattern matching on MkStream (in viewStream) is that the "s" type stored in the stream matches the "s" type taken and returned by the 'get next element' function. This allows the construction of another stream with the same function but a new state -- MkStream s' k.

It also allows the stream function in fibStream to be non-recursive which greatly aids the GHC optimizer in certain situations.

-- ryan

Alexander Solla

9:53 p.m.

On Mon, Aug 13, 2012 at 6:25 PM, Jay Sulzberger wrote:

...

On Mon, 13 Aug 2012, Ryan Ingram wrote:

On Mon, Aug 13, 2012 at 12:30 PM, Jay Sulzberger wrote:

...
Does Haskell have a word for "existential type" declaration? I

...
have the impression, and this must be wrong, that "forall" does double duty, that is, it declares a "for all" in some sense like the usual "for all" of the Lower Predicate Calculus, perhaps the "for all" of system F, or something near it.

It's using the forall/exists duality: exsts a. P(a) <=> forall r. (forall a. P(a) -> r) -> r

;)

This is, I think, a good joke. It has taken me a while, but I now understand that one of the most attractive things about Haskell is its sense of humor, which is unfailing.

I will try to think about this, after trying your examples.

I did suspect that, in some sense, "constraints" in combination with "forall" could give the quantifier "exists".

In a classical logic, the duality is expressed by !E! = A, and !A! = E, where E and A are backwards/upsidedown and ! represents negation. In particular, for a proposition P, Ex Px <=> !Ax! Px (not all x's are not P) and Ax Px <=> !Ex! Px (there does not exist an x which is not P) Negation is relatively tricky to represent in a constructive logic -- hence the use of functions/implications and bottoms/contradictions. The type ConcreteType -> b represents the negation of ConcreteType, because it shows that ConcreteType "implies the contradiction". Put these ideas together, and you will recover the duality as expressed earlier.

...

...
For example: (exists a. Show a => a) <=> forall r. (forall a. Show a => a -> r) -> r

This also works when you look at the type of a constructor:

data Showable = forall a. Show a => MkShowable a -- MkShowable :: forall a. Show a => a -> Showable

caseShowable :: forall r. (forall a. Show a => a -> r) -> Showable -> r caseShowable k (MkShowable x) = k x

testData :: Showable testData = MkShowable (1 :: Int)

useData :: Int useData = case testData of (MkShowable x) -> length (show x)

useData2 :: Int useData2 = caseShowable (length . show) testData

Haskell doesn't currently have first class existentials; you need to wrap them in an existential type like this. Using 'case' to pattern match on the constructor unwraps the existential and makes any packed-up constraints available to the right-hand-side of the case.

An example of existentials without using constraints directly:

data Stream a = forall s. MkStream s (s -> Maybe (a,s))

viewStream :: Stream a -> Maybe (a, Stream a) viewStream (MkStream s k) = case k s of Nothing -> Nothing Just (a, s') -> Just (a, MkStream s' k)

takeStream :: Int -> Stream a -> [a] takeStream 0 _ = [] takeStream n s = case viewStream s of Nothing -> [] Just (a, s') -> a : takeStream (n-1) s'

fibStream :: Stream Integer fibStream = Stream (0,1) (\(x,y) -> Just (x, (y, x+y)))

Here the 'constraint' made visible by pattern matching on MkStream (in viewStream) is that the "s" type stored in the stream matches the "s" type taken and returned by the 'get next element' function. This allows the construction of another stream with the same function but a new state -- MkStream s' k.

It also allows the stream function in fibStream to be non-recursive which greatly aids the GHC optimizer in certain situations.

-- ryan

______________________________**_________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/**mailman/listinfo/haskell-cafe http://www.haskell.org/mailman/listinfo/haskell-cafe

Jay Sulzberger

10:25 p.m.

On Mon, 13 Aug 2012, Alexander Solla wrote:

...

On Mon, Aug 13, 2012 at 6:25 PM, Jay Sulzberger wrote:

...
On Mon, 13 Aug 2012, Ryan Ingram wrote:

On Mon, Aug 13, 2012 at 12:30 PM, Jay Sulzberger wrote:

...
Does Haskell have a word for "existential type" declaration? I

...
have the impression, and this must be wrong, that "forall" does double duty, that is, it declares a "for all" in some sense like the usual "for all" of the Lower Predicate Calculus, perhaps the "for all" of system F, or something near it.

It's using the forall/exists duality: exsts a. P(a) <=> forall r. (forall a. P(a) -> r) -> r

;)

This is, I think, a good joke. It has taken me a while, but I now understand that one of the most attractive things about Haskell is its sense of humor, which is unfailing.

I will try to think about this, after trying your examples.

I did suspect that, in some sense, "constraints" in combination with "forall" could give the quantifier "exists".

In a classical logic, the duality is expressed by !E! = A, and !A! = E, where E and A are backwards/upsidedown and ! represents negation. In particular, for a proposition P,

Ex Px <=> !Ax! Px (not all x's are not P) and Ax Px <=> !Ex! Px (there does not exist an x which is not P)

Yes.

...

Negation is relatively tricky to represent in a constructive logic -- hence the use of functions/implications and bottoms/contradictions. The type ConcreteType -> b represents the negation of ConcreteType, because it shows that ConcreteType "implies the contradiction".

I am becoming sensitized to this distinction. I now, I think, feel the impulse toward "constructivism", that is, the assumption/delusion^Waspiration that all functions from the reals to the reals are continuous. One argument that helped me goes: The reals between 0 and 1 are functions from the integers to say {0, 1}. They are attained as limits of functions f: iota(n) -> {0, 1}, as n becomes larger and larger and ... , where iota(n) is a set with n elements, n a finite integer. So, our objects, the reals, are attained as limits. And the process of proceeding toward the limit is "natural", "functorial" in the sense of category theory. Thus so also our morphisms, that is functions from the reals to the reals, must be produced functorially as limits of maps between objects f: iota(n) -> {0, 1}.

...

Put these ideas together, and you will recover the duality as expressed earlier.

Thanks! I am reading some blog posts and I was impressed by the buffalo hair here: http://existentialtype.wordpress.com/2012/08/11/extensionality-intensionalit... oo--JS.

...

...
...
For example: (exists a. Show a => a) <=> forall r. (forall a. Show a => a -> r) -> r

This also works when you look at the type of a constructor:

data Showable = forall a. Show a => MkShowable a -- MkShowable :: forall a. Show a => a -> Showable

caseShowable :: forall r. (forall a. Show a => a -> r) -> Showable -> r caseShowable k (MkShowable x) = k x

testData :: Showable testData = MkShowable (1 :: Int)

useData :: Int useData = case testData of (MkShowable x) -> length (show x)

useData2 :: Int useData2 = caseShowable (length . show) testData

Haskell doesn't currently have first class existentials; you need to wrap them in an existential type like this. Using 'case' to pattern match on the constructor unwraps the existential and makes any packed-up constraints available to the right-hand-side of the case.

An example of existentials without using constraints directly:

data Stream a = forall s. MkStream s (s -> Maybe (a,s))

viewStream :: Stream a -> Maybe (a, Stream a) viewStream (MkStream s k) = case k s of Nothing -> Nothing Just (a, s') -> Just (a, MkStream s' k)

takeStream :: Int -> Stream a -> [a] takeStream 0 _ = [] takeStream n s = case viewStream s of Nothing -> [] Just (a, s') -> a : takeStream (n-1) s'

fibStream :: Stream Integer fibStream = Stream (0,1) (\(x,y) -> Just (x, (y, x+y)))

Here the 'constraint' made visible by pattern matching on MkStream (in viewStream) is that the "s" type stored in the stream matches the "s" type taken and returned by the 'get next element' function. This allows the construction of another stream with the same function but a new state -- MkStream s' k.

It also allows the stream function in fibStream to be non-recursive which greatly aids the GHC optimizer in certain situations.

-- ryan

______________________________**_________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/**mailman/listinfo/haskell-cafe http://www.haskell.org/mailman/listinfo/haskell-cafe

Ryan Ingram

14 Aug 14 Aug

7:40 a.m.

On Mon, Aug 13, 2012 at 6:53 PM, Alexander Solla wrote:

...

In a classical logic, the duality is expressed by !E! = A, and !A! = E, where E and A are backwards/upsidedown and ! represents negation. In particular, for a proposition P,

Ex Px <=> !Ax! Px (not all x's are not P) and Ax Px <=> !Ex! Px (there does not exist an x which is not P)

Negation is relatively tricky to represent in a constructive logic -- hence the use of functions/implications and bottoms/contradictions. The type ConcreteType -> b represents the negation of ConcreteType, because it shows that ConcreteType "implies the contradiction".

Put these ideas together, and you will recover the duality as expressed earlier.

I'd been looking for a good explanation of how to get from Ex Px to !Ax! Px in constructive logic, and this is basically it. What is said here is actually a slightly different statement, which is what had me confused! If you do the naive encoding, you get something like -- This is my favorite representation of "Contradiction" in Haskell, since -- it has reductio ad absurdum encoded directly in the type -- and only requires Rank2Types. newtype Contradiction = Bottom { absurd :: forall a. a } -- absurd :: forall a. Contradiction -> a type Not a = a -> Contradiction newtype NotC (c :: * -> Constraint) = MkNotC { unNotC :: forall a. c a => Not a } type UselessExists (c :: * -> Constraint) = Not (NotC c) -- here I'm using ConstraintKinds as, in a sense, the 'most generic' way of specifying a type-level predicate, -- at least in bleeding edge Haskell. It's trivial to make a less generic version for any particular constraint -- you care about without going quite so overboard on type system extensions :) -- i.e. -- newtype NoShow = MkNoShow { unNoShow :: forall a. Show a => Not a } -- type UselessExistsShow = Not NoShow -- A simple example: there is a type that is equal to Bool: silly :: UselessExists ((~) Bool) silly (MkNotC k) = k True -- need silly :: NotC ((~) Bool) -> Contradiction -- after pattern matching on MkNotC -- k :: forall a. (a ~ Bool) => a -> Contradiction -- i.e. k :: Bool -> Contradiction -- therefore, k True :: Contradiction. This type is useless, however; NotC c isn't usefully inhabited at any reasonable c -- there's no way to actually call it! The magic comes when you unify the 'return type' from the two Nots instead of using bottoms as a catch-all... I guess this is the CPS translation of negation? type NotR r a = a -> r newtype NotRC r (c :: * -> Constraint) = MkNotRC { unNotRC :: forall a. c a => NotR r a } -- MkNotRC :: forall r c. (forall a. c a => a -> r) -> NotRC r type ExistsR r (c :: * -> Constraint) = NotR r (NotRC r c) -- ~= c a => (a -> r) -> r newtype Exists (c :: * -> Constraint) = MkExists { unExists :: forall r. ExistsR r c } -- MkExists :: forall c. (forall r. NotR r (NotRC r c)) -> Exists c -- ~= forall c. (forall r. c a => (a -> r) -> r) -> Exists c -- A simple example: there is a type that is equal to Bool: silly2 :: Exists ((~) Bool) silly2 = MkExists (\(MkNotRC k) -> k False) This version allows you to specify the type of 'absurd' result you want, and use that to let the witness of existence escape out via whatever interface the provided constraint gives. caseExists :: (forall a. c a => a -> r) -> Exists c -> r caseExists k (MkExists f) = f (MkNotRC k) main = putStrLn $ caseExists show silly2 -- should print "False"

wren ng thornton

15 Aug 15 Aug

3:20 a.m.

On 8/13/12 9:25 PM, Jay Sulzberger wrote:

...

I did suspect that, in some sense, "constraints" in combination with "forall" could give the quantifier "exists".

It's even easier than that. (forall a. P(a)) -> Q <=> exists a. (P(a) -> Q) Where P and Q are metatheoretic/schematic variables. This is just the usual thing about antecedents being in a "negative" position, and thus flipping as you move into/out of that position. The duality mentioned previously is just for the case where you don't have that handy "-> Q" there. How do we get the universal quantifier into a negative position when there's no implication? Why, we add an implication, of course. Even better, add two. -- Live well, ~wren

David Feuer

12:32 p.m.

On Aug 15, 2012 3:21 AM, "wren ng thornton" wrote:

...

It's even easier than that.

(forall a. P(a)) -> Q <=> exists a. (P(a) -> Q)

Where P and Q are metatheoretic/schematic variables. This is just the usual thing about antecedents being in a "negative" position, and thus flipping as you move into/out of that position.

Most of this conversation is going over my head. I can certainly see how exists a. (P(a)->Q) implies that (forall a. P(a))->Q. The opposite certainly doesn't hold in classical logic. What sort of logic are you folks working in?

Ryan Ingram

3:39 p.m.

In classical logic A -> B is the equivalent to ~A v B (with ~ = not and v = or) So (forall a. P(a)) -> Q {implication = not-or} ~(forall a. P(a)) v Q {forall a. X is equivalent to there does not exist a such that X doesn't hold} ~(~exists a. ~P(a)) v Q {double negation elimination} (exists a. ~P(a)) v Q {a is not free in Q} exists a. (~P(a) v Q) {implication = not-or} exists a. (P(a) -> Q) These steps are all equivalencies, valid in both directions. On Wed, Aug 15, 2012 at 9:32 AM, David Feuer wrote:

...

On Aug 15, 2012 3:21 AM, "wren ng thornton" wrote:

...
It's even easier than that.

(forall a. P(a)) -> Q <=> exists a. (P(a) -> Q)

Where P and Q are metatheoretic/schematic variables. This is just the usual thing about antecedents being in a "negative" position, and thus flipping as you move into/out of that position.

Most of this conversation is going over my head. I can certainly see how exists a. (P(a)->Q) implies that (forall a. P(a))->Q. The opposite certainly doesn't hold in classical logic. What sort of logic are you folks working in?

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

David Feuer

7:32 p.m.

I understand this now, though I still don't understand the context. Thanks! I managed to mix up implication with causation, to my great embarrassment. On Aug 15, 2012 3:39 PM, "Ryan Ingram" wrote:

...

In classical logic A -> B is the equivalent to ~A v B (with ~ = not and v = or)

So

(forall a. P(a)) -> Q {implication = not-or} ~(forall a. P(a)) v Q {forall a. X is equivalent to there does not exist a such that X doesn't hold} ~(~exists a. ~P(a)) v Q {double negation elimination} (exists a. ~P(a)) v Q {a is not free in Q} exists a. (~P(a) v Q) {implication = not-or} exists a. (P(a) -> Q)

These steps are all equivalencies, valid in both directions.

On Wed, Aug 15, 2012 at 9:32 AM, David Feuer wrote:

...
On Aug 15, 2012 3:21 AM, "wren ng thornton" wrote:

...
It's even easier than that.

(forall a. P(a)) -> Q <=> exists a. (P(a) -> Q)

Where P and Q are metatheoretic/schematic variables. This is just the usual thing about antecedents being in a "negative" position, and thus flipping as you move into/out of that position.

Most of this conversation is going over my head. I can certainly see how exists a. (P(a)->Q) implies that (forall a. P(a))->Q. The opposite certainly doesn't hold in classical logic. What sort of logic are you folks working in?

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

wren ng thornton

16 Aug 16 Aug

11:05 p.m.

On 8/15/12 12:32 PM, David Feuer wrote:

...

On Aug 15, 2012 3:21 AM, "wren ng thornton" wrote:

...
It's even easier than that.

(forall a. P(a)) -> Q <=> exists a. (P(a) -> Q)

Where P and Q are metatheoretic/schematic variables. This is just the usual thing about antecedents being in a "negative" position, and thus flipping as you move into/out of that position.

Most of this conversation is going over my head. I can certainly see how exists a. (P(a)->Q) implies that (forall a. P(a))->Q. The opposite certainly doesn't hold in classical logic. What sort of logic are you folks working in?

Ryan gave a nice classical proof. Though note that, in a constructive setting you're right to be dubious. The validity of the questioned article is related to the "generalized Markov's principle" which Russian constructivists accept but which is not derivable from Heyting's axiomatization of intuitionistic logic: GMP : ~(forall x. P(x)) -> (exists x. ~P(x)) There's been a fair amount of work on showing that GMP is constructively valid; though the fact that it does not derive from Heyting's axiomatization makes some squeamish. For these reasons it may be preferable to stick with the double-negation form upthread for converting between quantifiers. I just mentioned the above as a simplification of the double-negation form, which may be more familiar to those indoctrinated in classical logic. -- Live well, ~wren

Albert Y. C. Lai

15 Aug 15 Aug

2:55 p.m.

On 12-08-15 03:20 AM, wren ng thornton wrote:

...

(forall a. P(a)) -> Q <=> exists a. (P(a) -> Q)

For example: A. (forall p. p drinks) -> (everyone drinks) B. exists p. ((p drinks) -> (everyone drinks)) In a recent poll, 100% of respondents think A true, 90% of them think B paradoxical, and 40% of them have not heard of the Smullyan drinking paradox. Hehe! http://www.vex.net/~trebla/weblog/any-all-some.html

wren ng thornton

16 Aug 16 Aug

11:07 p.m.

On 8/15/12 2:55 PM, Albert Y. C. Lai wrote:

...

On 12-08-15 03:20 AM, wren ng thornton wrote:

...
(forall a. P(a)) -> Q <=> exists a. (P(a) -> Q)

For example:

A. (forall p. p drinks) -> (everyone drinks) B. exists p. ((p drinks) -> (everyone drinks))

In a recent poll, 100% of respondents think A true, 90% of them think B paradoxical, and 40% of them have not heard of the Smullyan drinking paradox.

:) Though bear in mind we're discussing second-order quantification here, not first-order. -- Live well, ~wren

Alexander Solla

17 Aug 17 Aug

12:54 a.m.

On Thu, Aug 16, 2012 at 8:07 PM, wren ng thornton wrote:

...

On 8/15/12 2:55 PM, Albert Y. C. Lai wrote:

...
On 12-08-15 03:20 AM, wren ng thornton wrote:

...
(forall a. P(a)) -> Q <=> exists a. (P(a) -> Q)

For example:

A. (forall p. p drinks) -> (everyone drinks) B. exists p. ((p drinks) -> (everyone drinks))

In a recent poll, 100% of respondents think A true, 90% of them think B paradoxical, and 40% of them have not heard of the Smullyan drinking paradox.

:)

Though bear in mind we're discussing second-order quantification here, not first-order.

Can you expand on what you mean here? I don't see two kinds of quantification in the type language (at least, reflexively, in the context of what we're discussing). In particular, I don't see how to quantify over predicates for (or sets of, via the extensions of the predicates) types. Is Haskell's 'forall' doing double duty?

wren ng thornton

18 Aug 18 Aug

11:24 p.m.

On 8/17/12 12:54 AM, Alexander Solla wrote:

...

On Thu, Aug 16, 2012 at 8:07 PM, wren ng thornton wrote:

...
Though bear in mind we're discussing second-order quantification here, not first-order.

Can you expand on what you mean here? I don't see two kinds of quantification in the type language (at least, reflexively, in the context of what we're discussing). In particular, I don't see how to quantify over predicates for (or sets of, via the extensions of the predicates) types.

Is Haskell's 'forall' doing double duty?

Nope, it's the "forall" of mathematics doing double duty :) Whenever doing quantification, there's always some domain being quantified over, though all too often that domain is left implicit; whence lots of confusion over the years. And, of course, there's the scope of the quantification, and the entire expression. For example, consider the expression: forall a. P(a) The three important collections to bear in mind are: (1) the collection of things a ranges over (2) the collection of things P(a) belongs to (3) the collection of things forall a. P(a) belongs to So if we think of P as a function from (1) to (2), and name the space of such functions (1->2), then we can think of the quantifier as a function from (1->2) to (3). When you talk to logicians about quantifiers, the first thing they think of is so-called "first-order" quantification. That is, given the above expression, they think that the thing being quantified over is a collection of "individuals" who live outside of logic itself[1]. For example, we could be quantifying over the natural numbers, or over the kinds of animals in the world, or any other extra-logical group of entities. In Haskell, when we see the above expression we think that the thing being quantified over is some collection of types[2]. But, that means when we think of P as a function it's taking types and returning types! So the thing you're quantifying over and the thing you're constructing are from the same domain[3]! This gets logicians flustered and so they call it "second-order" (or more generally, "higher-order") quantification. If you assert the primacy of first-order logic, it makes sense right? In the first-order case we're quantifying over individuals; in the second-order case we're quantifying over collections of individuals; so third-order would be quantifying over collections of collections of individuals; and on up to higher orders. Personally, I find the names "first-order" and "second-order" rather dubious--- though the distinction is a critical one to make. Part of the reason for its dubiousness can be seen when you look at PTSes which make explicit that (1), (2), and (3) above can each be the same or different in all combinations. First-order quantification is the sort of thing you get from Pi/Sigma types in dependently typed languages like LF; second-order quantification is the sort of thing you get from the forall/exists quantifiers in polymorphic languages like System F. But the Barendregt cube makes it clear that these are *orthogonal* features. Neither one of them comes "first" or "second"; they just do very different things. Logicians thought first of first-order quantification, so they consider that primitive and worry about the complications of dealing with second-/higher-order quantification. Until recently type theory was focused on polymorphism of various sorts, so that's considered primitive or at least easier, whereas dependent types are exotic and worrisome/hard. [1] This is also the root of the distinction between "functions", "predicates", and "logical connectives" in traditional logic. Functions map individuals to individuals; predicates map individuals to propositions/truth-values; and connectives map propositions/TVs to propositions/TVs. Though, traditionally, the set of connectives is taken to be small and fixed whereas functions and predicates are left to be defined by a "signature". [2] Namely monotypes. If we allowed quantified variables to be instantiated with polymorphic types, then we'd get "impredicative" quantification. Impredicativity can be both good and bad, depending on what you're up to. [3] Well, they're only the same domain for impredicative quantification. Otherwise the collection of types you're constructing is "bigger" than the collection you're quantifying over. -- Live well, ~wren

Ryan Ingram

20 Aug 20 Aug

9:11 p.m.

Also, I have to admit I was a bit handwavy here; I meant P in a metatheoretic sense, that is "P(a) is some type which contains 'a' as a free variable", and thus the 'theorem' is really a collection of theorems parametrized on the P you choose. For example, P(a) could be "Show a & a -> Int"; in that case we get the theorem exists a. (Show a, a -> Int) <=> forall r. (forall a. Show a => (a -> Int) -> r) -> r as witnessed by the following code (using the ExistentialQuantification and RankNTypes extensions) data P = forall a. Show a => MkP (a -> Int) type CPS_P r = (forall a. Show a => (a -> Int) -> r) -> r isoR :: P -> forall r. CPS_P r isoR (MkP f) k = -- pattern match on MkP brings a fresh type T into scope, -- along with f :: T -> Int, and the constraint Show T. -- k :: forall a. Show a => (a -> Int) -> r -- so, k {T} f :: r isoL :: (forall r. CPS_P r) -> P isoL k = k (\x -> MkP x) -- k :: forall r. (forall a. Show a => (a -> Int) -> r) -> r -- k {P} = (forall a. Show a => (a -> Int) -> P) -> P -- MkP :: forall a. Show a => (a -> Int) -> P -- therefore, k {P} MkP :: P Aside: the type 'exists a. (Show a, a -> Int)' is a bit odd, and is another reason we don't have first class existentials in Haskell. The 'forall' side is using currying (a -> b -> r) <=> ((a,b) -> r) which works because the constraint => can be modeled by dictionary passing. But we don't have a simple way to represent the dictionary (Show a) as a member of a tuple. One answer is to pack it up in another "existential"; I find this a bit of a misnomer since there's nothing existential about this data type aside from the dictionary: data ShowDict a = Show a => MkShowDict Then the theorem translation is a bit more straightforward: data P = forall a. MkP (ShowDict a, a -> Int) type CPS_P r = (forall a. (ShowDict a, a -> Int) -> r) -> r -- theorem: P <=> forall r. CPS_P r isoL :: P -> forall r. CPS_P r isoL (MkP x) k = k x isoR :: (forall r. CPS_P r) -> P isoR k = k (\x -> MkP x) -- ryan On Sat, Aug 18, 2012 at 8:24 PM, wren ng thornton wrote:

...

On 8/17/12 12:54 AM, Alexander Solla wrote:

...
On Thu, Aug 16, 2012 at 8:07 PM, wren ng thornton wrote:

...
Though bear in mind we're discussing second-order quantification here, not first-order.

Can you expand on what you mean here? I don't see two kinds of quantification in the type language (at least, reflexively, in the context of what we're discussing). In particular, I don't see how to quantify over predicates for (or sets of, via the extensions of the predicates) types.

Is Haskell's 'forall' doing double duty?

Nope, it's the "forall" of mathematics doing double duty :)

Whenever doing quantification, there's always some domain being quantified over, though all too often that domain is left implicit; whence lots of confusion over the years. And, of course, there's the scope of the quantification, and the entire expression. For example, consider the expression:

forall a. P(a)

The three important collections to bear in mind are: (1) the collection of things a ranges over (2) the collection of things P(a) belongs to (3) the collection of things forall a. P(a) belongs to

So if we think of P as a function from (1) to (2), and name the space of such functions (1->2), then we can think of the quantifier as a function from (1->2) to (3).

When you talk to logicians about quantifiers, the first thing they think of is so-called "first-order" quantification. That is, given the above expression, they think that the thing being quantified over is a collection of "individuals" who live outside of logic itself[1]. For example, we could be quantifying over the natural numbers, or over the kinds of animals in the world, or any other extra-logical group of entities.

In Haskell, when we see the above expression we think that the thing being quantified over is some collection of types[2]. But, that means when we think of P as a function it's taking types and returning types! So the thing you're quantifying over and the thing you're constructing are from the same domain[3]! This gets logicians flustered and so they call it "second-order" (or more generally, "higher-order") quantification. If you assert the primacy of first-order logic, it makes sense right? In the first-order case we're quantifying over individuals; in the second-order case we're quantifying over collections of individuals; so third-order would be quantifying over collections of collections of individuals; and on up to higher orders.

Personally, I find the names "first-order" and "second-order" rather dubious--- though the distinction is a critical one to make. Part of the reason for its dubiousness can be seen when you look at PTSes which make explicit that (1), (2), and (3) above can each be the same or different in all combinations. First-order quantification is the sort of thing you get from Pi/Sigma types in dependently typed languages like LF; second-order quantification is the sort of thing you get from the forall/exists quantifiers in polymorphic languages like System F. But the Barendregt cube makes it clear that these are *orthogonal* features. Neither one of them comes "first" or "second"; they just do very different things. Logicians thought first of first-order quantification, so they consider that primitive and worry about the complications of dealing with second-/higher-order quantification. Until recently type theory was focused on polymorphism of various sorts, so that's considered primitive or at least easier, whereas dependent types are exotic and worrisome/hard.

[1] This is also the root of the distinction between "functions", "predicates", and "logical connectives" in traditional logic. Functions map individuals to individuals; predicates map individuals to propositions/truth-values; and connectives map propositions/TVs to propositions/TVs. Though, traditionally, the set of connectives is taken to be small and fixed whereas functions and predicates are left to be defined by a "signature".

[2] Namely monotypes. If we allowed quantified variables to be instantiated with polymorphic types, then we'd get "impredicative" quantification. Impredicativity can be both good and bad, depending on what you're up to.

[3] Well, they're only the same domain for impredicative quantification. Otherwise the collection of types you're constructing is "bigger" than the collection you're quantifying over.

-- Live well, ~wren

______________________________**_________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/**mailman/listinfo/haskell-cafe http://www.haskell.org/mailman/listinfo/haskell-cafe

oleg＠okmij.org

14 Aug 14 Aug

4:02 a.m.

New subject: Data structure containing elements which are instances of the

...

It's only a test case. The real thing is for a game and will be something like:

...

class EntityT e where update :: e -> e render :: e -> IO () handleEvent :: e -> Event -> e getBound :: e -> Maybe Bound

...

data Entity = forall e. (EntityT e) => Entity e

...

data Level = Level { entities = [Entity], ... }

I suspected the real case would look like that. It is also covered on the same web page on Eliminating existentials. Here is your example without existentials, in pure Haskell98 (I took a liberty to fill in missing parts to make the example running) data Event = Event Int -- Stubs type Bound = Pos type Pos = (Float,Float) data EntityO = EntityO{ update :: EntityO, render :: IO (), handleEvent :: Event -> EntityO, getBound :: Maybe Bound } type Name = String new_entity :: Name -> Pos -> EntityO new_entity name pos@(posx,posy) = EntityO{update = update, render = render, handleEvent = handleEvent, getBound = getBound} where update = new_entity name (posx+1,posy+1) render = putStrLn $ name ++ " at " ++ show pos handleEvent (Event x) = new_entity name (posx + fromIntegral x,posy) getBound = if abs posx + abs posy < 1.0 then Just pos else Nothing data Level = Level { entities :: [EntityO] } levels = Level { entities = [new_entity "e1" (0,0), new_entity "e2" (1,1)] } evolve :: Level -> Level evolve l = l{entities = map update (entities l)} renderl :: Level -> IO () renderl l = mapM_ render (entities l) main = renderl . evolve $ levels I think the overall pattern should look quite familiar. The code shows off the encoding of objects as records of closures. See http://okmij.org/ftp/Scheme/oop-in-fp.txt for the references and modern reconstruction of Ken Dickey's ``Scheming with Objects''. It is this encoding that gave birth to Scheme -- after Steele and Sussman realized that closures emulate actors (reactive objects). Incidentally, existentials do enter the picture: the emerge upon closure conversion: Yasuhiko Minamide, J. Gregory Morrisett and Robert Harper Typed Closure Conversion. POPL1996 http://www.cs.cmu.edu/~rwh/papers/closures/popl96.ps This message demonstrates the inverse of the closure conversion, eliminating existentials and introducing closures.

4657

Age (days ago)

4667

Last active (days ago)

List overview

Download

24 comments

12 participants

participants (12)

Albert Y. C. Lai
Alexander Solla
Antoine Latter
Daniel Trstenjak
David Feuer
Heinrich Apfelmus
Jay Sulzberger
Johan Holmquist
oleg＠okmij.org
Patrick Palka
Ryan Ingram
wren ng thornton