Re: [Haskell-cafe] Re: Existencial quantification and polymorphic datatypes (actually, components...)
-BEGIN PGP SIGNED MESSAGE- Hash: SHA1 Gleb Alexeyev wrote: | Mauricio wrote: | | data SomeNum = SN (forall a. a) | | [...] | | you cannot do anything to the value you extract Maybe. Say you construct (SN x). If you later extract x, you can observe that it terminates (using seq, perhaps), assuming that it does terminate. You still can't really do anything with the value, but you can at least observe something about its computation. The uses of this may be obscure (I can't think of any right now), but I wouldn't say they necessarily don't exist. - - Jake -BEGIN PGP SIGNATURE- Version: GnuPG v1.4.9 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iEYEARECAAYFAkl3eb8ACgkQye5hVyvIUKnGZgCcDvZKVmqcwjdx97MkPu3I5r3n KsUAn0IlCTwyCH5h5QTyDPvM1MkX36Hz =Ocgm -END PGP SIGNATURE- ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Existencial quantification and polymorphic datatypes (actually, components...)
On Wed, 2009-01-21 at 13:38 -0600, Jake McArthur wrote: -BEGIN PGP SIGNED MESSAGE- Hash: SHA1 Gleb Alexeyev wrote: | Mauricio wrote: | | data SomeNum = SN (forall a. a) | | [...] | | you cannot do anything to the value you extract Maybe. Say you construct (SN x). If you later extract x, you can observe that it terminates (using seq, perhaps), assuming that it does terminate. The definition you quoted is equivalent to data SomeNum where SN :: (forall a. a) - SomeNum So if I say case y of SN x - ... Then in the sequel (...) I can use x at whatever type I want --- it's polymorphic --- but whatever type I use it at, it cannot terminate. I think you meant to quote the definition data SomeNum = forall a. SN a which is equivalent to data SomeNum where SN :: forall a. a - SomeNum in which case if I say case y of SN x - ... then x is a perfectly monomorphic value, whose type happens to be a (fresh) constant distinct from all other types in the program. So I can't do anything useful with x, although as you say, it can be forced with seq. OTOH, you could do exactly the same thing with a normal judgment of type (), if you found a use for it. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Existencial quantification and polymorphic datatypes (actually, components...)
-BEGIN PGP SIGNED MESSAGE- Hash: SHA1 Jonathan Cast wrote: | I think you meant to quote the definition | | data SomeNum = forall a. SN a Quite so. Thanks for clearing that up. - - Jake -BEGIN PGP SIGNATURE- Version: GnuPG v1.4.9 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iEYEARECAAYFAkl3gr8ACgkQye5hVyvIUKmiDgCfeH8fEn0+iDEMlQwtCHtMXAti vSoAnAwYibedZTR1YyzrcC0OTspXsjMX =Vagv -END PGP SIGNATURE- ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Existencial quantification and polymorphic datatypes (actually, components...)
4294967296 :: Integer (...) In the above you can see the polymorphism of the return type of fromInteger, it returns a Int8 or a Int32. You can see the polymorphism of the argument of show, it takes an Int8 or Int32 or Integer. The latest ghc-6.10.1 also allows avoiding use of SomeNum, see impredicative-polymorphism: http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.html#impredicative-polymorphism Great, thanks! I'm enlightened :) But how is this: data SomeNum = forall a. SN a different from: data SomeNum = SN (forall a. a) ? Maurício ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Existencial quantification and polymorphic datatypes (actually, components...)
Mauricio wrote: But how is this: data SomeNum = forall a. SN a different from: data SomeNum = SN (forall a. a) In the first case the constructor SN can be applied to the monomorphic value of any type, it effectively hides the type of the argument. For example, you can have a list like [SN True, SN foo, SN 42], because for all x SN x has type SomeNum. In the second case, SN can be applied only to polymorphic values, SN True or SN foo won't compile. The only thing that both types have in common - they are both useless. Polymorphic and existential types must have more structure to be useful - you cannot _construct_ SomeNum #2 and you cannot do anything to the value you _extract_ from SomeNum #1. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Existencial quantification and polymorphic datatypes (actually, components...)
I just thought that the shorter explanation could do better: the
difference is in the types of the constructor functions.
Code:
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE RankNTypes #-}
data SomeNum1 = forall a. SN1 a
data SomeNum2 = SN2 (forall a. a)
ghci session:
*Main :t SN1
SN1 :: a - SomeNum1
*Main :t SN2
SN2 :: (forall a. a) - SomeNum2
This is not the whole story, types of the bound variables you get on
pattern matching differ too, but this makes the short explanation a bit
longer :).
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Existencial quantification and polymorphic datatypes (actually, components...)
Great, thanks! I'm enlightened :) And no one had to hit you with a stick first! But how is this: data SomeNum = forall a. SN a different from: data SomeNum = SN (forall a. a) ? At a glance they look the same to me — but only the first is accepted by ghc. There is also the GADT syntax: data SomeNum where SomeNum :: forall a. (Typeable a, Num a) = a - SomeNum which is accepted by ghc with the LANGUAGE GADTs extension. The GADT is more than simple syntactic sugar, it allows for easier use this kind of existential type. -- Chris ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Existencial quantification and polymorphic datatypes (actually, components...)
But how is this: data SomeNum = forall a. SN a different from: data SomeNum = SN (forall a. a) At a glance they look the same to me — but only the first is accepted by ghc. Following the link you pointed in the last message, I found this at 8.8.4.1: data T a = T1 (forall b. b - b - b) a If I understand properly, it can be activated with -XPolymorphicComponents. It's different from my example, but I would like to know what it does that this can't: data T a = forall b. T1 (b-b-b) a (The last one I think I understand well after the previous message, although I see no use for this particular form, since after pattern match there's no other 'b' value to which we could aply that function field.) Link for convenience: http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.html Maurício ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Existencial quantification and polymorphic datatypes (actually, components...)
On Tue, Jan 20, 2009 at 2:51 PM, Mauricio briqueabra...@yahoo.com wrote: But how is this: data SomeNum = forall a. SN a different from: data SomeNum = SN (forall a. a) At a glance they look the same to me — but only the first is accepted by ghc. Following the link you pointed in the last message, I found this at 8.8.4.1: data T a = T1 (forall b. b - b - b) a If I understand properly, it can be activated with -XPolymorphicComponents. It's different from my example, but I would like to know what it does that this can't: data T a = forall b. T1 (b-b-b) a In the first example, T stores a function which works for every type. In the second example, T stores a function which works on a specific type. So with the first definition, you can do something like this: foo :: T1 a - (Bool, Int) foo (T1 f _) = (f True False, f 1 2) But you can't really do anything useful with the second example. (The last one I think I understand well after the previous message, although I see no use for this particular form, since after pattern match there's no other 'b' value to which we could aply that function field.) Here's a more useful example of existential quantification: data Stream a = forall b. Stream (b - a) (b - b) b head :: Stream a - a head (Stream h t b) = h b tail :: Stream a - Stream a tail (Stream h t b) = Stream h t (t b) -- Dave Menendez d...@zednenem.com http://www.eyrie.org/~zednenem/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Existencial quantification and polymorphic datatypes (actually, components...)
On Tue, Jan 20, 2009 at 1:14 PM, David Menendez d...@zednenem.com wrote: On Tue, Jan 20, 2009 at 2:51 PM, Mauricio briqueabra...@yahoo.com wrote: But how is this: data SomeNum = forall a. SN a different from: data SomeNum = SN (forall a. a) At a glance they look the same to me — but only the first is accepted by ghc. Following the link you pointed in the last message, I found this at 8.8.4.1: data T a = T1 (forall b. b - b - b) a The constructor here is irrelevant. The function here can do anything a top-level function of type: something :: b - b - b I like to think about quantification in this regard in terms of isomorphisms. Think about what a function of type forall b. b - b - b can do. It cannot do anything with its arguments, because it must work on all types, so it only has one choice to make: it can return the first argument, or it can return the second argument. So, forall b. b - b - b is isomorphic to Bool. For symmetry, the constructor T1 has type: T1 :: (forall b. b - b - b) - a - T1 a If I understand properly, it can be activated with -XPolymorphicComponents. It's different from my example, but I would like to know what it does that this can't: data T a = forall b. T1 (b-b-b) a The constructor T1 here has type: T1 :: forall b. (b - b - b) - a - T1 a See the difference? You can pass the latter a function of any type you choose, eg. (Int - Int - Int) or ((Bool - Bool) - (Bool - Bool) - (Bool - Bool)). So when somebody gets a T from you, they have no idea what type the function you gave it was, so they can only use it in limited ways (in this case, nothing useful at all can be done with it). Here's another existential type: data T' a = forall b. T' (b - a) b Here, a T' contains a value of some type b -- who knows what it is -- and a function to get from that value to an a. Since we don't know anything about b, all we can do is to apply the function. T' a is isomorphic to a. But it might have different operational behavior; e.g. maybe a is a huge list which is cheaply generated from some small generator value (of type b). Then if you pass a T' around, it's the same as passing that big list around, except for you don't cache the results of the list, improving memory performance. It's like inverse memoization. Not all existential types are for inverse memoization, this is just one case. I found it easiest to reason about these with the types of the constructors, and thinking about what non-quantified type they are isomorphic to. Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
