I have found that ghc has adopted the existential data constructors. Because it was first time I have heard this term I have found some articles about it. The less complex for me was the following explanation data Worker x y = Worker {buffer :: b, input :: x, output :: y} This is wrong in Haskell98 because we can 't just hide buffer :: b. We should write instead data Worker b x y = Worker {buffer :: b, input :: x, output :: y} Let suppose that b has an indefinite type. Then with existential types we could write data Worker x y = forall b. Buffer b => Worker {buffer :: b, input :: x, output :: y} The example above is similar to the example that Paul Hudak, John Hughes, Simon Peyton Jones and Philip Wadler mention in an article "a history of Haskell". Though I can't figure out how exactly could utilize such a type. To be honest haskell is my first functional language and I 'm not so familiar with. So, an example would be very helpful
On Wed, 13 Feb 2008, Simeon Mattes wrote:
I have found that ghc has adopted the existential data constructors. Because it was first time I have heard this term I have found some articles about it. The less complex for me was the following explanation
data Worker x y = Worker {buffer :: b, input :: x, output :: y}
Seems to be the example which is also presented here: http://www.haskell.org/haskellwiki/Existential_type
Simeon Mattes wrote:
I have found that ghc has adopted the existential data constructors. Because it was first time I have heard this term I have found some articles about it. The less complex for me was the following explanation
data Worker x y = Worker {buffer :: b, input :: x, output :: y}
This is wrong in Haskell98 because we can 't just hide buffer :: b. We should write instead data Worker b x y = Worker {buffer :: b, input :: x, output :: y}
Let suppose that b has an indefinite type. Then with existential types we could write data Worker x y = forall b. Buffer b => Worker {buffer :: b, input :: x, output :: y}
The example above is similar to the example that Paul Hudak, John Hughes, Simon Peyton Jones and Philip Wadler mention in an article "a history of Haskell".
Though I can't figure out how exactly could utilize such a type. To be honest haskell is my first functional language and I 'm not so familiar with. So, an example would be very helpful
I would say I don't see why this particular datatype is useful. I mean with no regard to existentials. Having output as a field in the data constructor seems strange to me.
Let's try a different example. Let's start with a list designed to hold numbers: data NumericList a = Num a => [a] Normally this would be fine. We can hold things like [1, 2, 3, 4, 5] and [1.7, 5.3, 2.0, 99.1]. But what if we wanted to be able to hold numbers with _different types_ in the list? That is, we won't know anything about them except that they are instances of Num. That is where existential types come in: data NumericList = forall a . Num a => [a] Now we can have NumericLists like [1 :: Int, 5.7 :: Double, 4%5 :: Rational]. The only useful thing you can do with the values, in this case, is apply functions of the Num type class, but there are times when this is useful. (There are actually ways to cast these values back to their original types elsewhere, but I'll ignore that because it is far out of the scope of your question). Does this help? - Jake
On Feb 13, 2008 2:41 PM, Jake McArthur
Now we can have NumericLists like [1 :: Int, 5.7 :: Double, 4%5 :: Rational].
No, we can't =). Using data NumericList = forall a . Num a => N [a] *Main> let a = N [1::Int,2,3,4] *Main> let b = N [1::Double,2,3,4] *Main> let c = N [1::Int,2::Double] <interactive>:1:18: Couldn't match expected type `Int' against inferred type `Double' In the expression: 2 :: Double In the first argument of `N', namely `[1 :: Int, 2 :: Double]' In the expression: N [1 :: Int, 2 :: Double] *Main> let d = [a, b, N [1::Rational,2,3,4]] The lists inside N will be homogeneous, but you can have a (homogeneous) list of N's such that each N has a diferrent list type. If you want a list of different types of numbers, you should do something like data Number = forall a. Num a => Number a type NumberList = [Number] x :: NumberList x = [Number (1::Int), Number (2::Double), Number (3::Rational)] or maybe data NumberList2 = forall a . Num a => Cons a NumberList2 | Nil x2 :: NumberList2 x2 = Cons (1::Int) $ Cons (2::Double) $ Cons (3::Rational) Nil Cheers, -- Felipe.
The help of all was very useful. But since Jake gave me an example I prefer to follow this up. Although I 'm not so familiar generally with datatypes I have understood you. It seems in this example that with existential types we can put in the same list different types although generally this is not allowed. I have tried to write this example with the ghc compiler 6.8.2 but there was an error pare error in data/newtype declaration. I have also tried to find the etymology of the word existential, since some times somebody can easily find a better answer, but I can't figure out why this is so. (really why "existential" types?). Maybe a completed example would be more helpful. existence Look up existence at Dictionary.com c.1384, from O.Fr. existence, from L.L. existentem "existent," prp. of L. existere "stand forth, appear," and, as a secondary meaning, "exist;" from ex- "forth" + sistere "cause to stand" (see assist). Existential as a term in logic is from 1819. Existentialism is 1941 from Ger. Existentialismus (1919), ult. from Dan. writer Søren Kierkegaard (1813-55), who wrote (1846) of Existents-Forhold "condition of existence," existentielle Pathos, etc. (I hope this way of questioning is not so strange)
The name "existential types" comes from the logical connective
"exists", which is the dual of "for all".
For example, given some property P of objects of type T, you can say
forall x : T. P(x) -- means that P holds for all things of type x
or
exists x : T. P(x) -- means that there is some x for which P holds.
For example, take P(x) to be "x is an integer".
Then:
forall x : Int, P(x) -- valid, all objects of type Int are integers
forall x : Float, P(x) -- not valid
exists x : Float, P(x) -- valid, for example, 1.0 :: Float is an integer
In Haskell, forall is only used for kinds, such as *, the type of
types, and * -> *, the kind of type constructor used for monads &
lists (among other things).
A couple of examples:
(+) :: forall a. Num a => a -> a -> a
means
forall a : *, Num a implies (+) has type (a -> a -> a)
return False :: forall a. Monad m => m Bool
means
forall m : * -> *, Monad m implies that (return False) has type (m Bool).
Similarily, you might want to say (note: this is not valid haskell)
[0 :: Int, 2 :: Double] :: [ t such that there exists a Num instance for t ],
However, you can express "exists" in terms of "forall":
exists x, P(x) is equivalent to (not (forall x, not P(x)))
that is, if it is not true for all x that P(x) does not hold, then
there must be some x for which it does hold.
The existential types extension to haskell uses this dual:
data Number = forall a. Num a => N a
means that the constructor N has type
N :: forall a. Num a => a -> Number
Consider this function:
isZero (N n) = (n == 0)
You have a Number and you are pattern matching on N, so what do you
know about the type of n?
Well, you know that N was called with an object of some type a, and
that Num a holds.
That is: exists a : *, Num a & type(n) == a
You can now express that list:
[ N (0 :: Int), N (2 :: Double) ] :: [ Number ]
and use it like any other list:
map isZero [ N (0 :: Int), N (2 :: Double) ] :: [Bool]
-- ryan
On 2/13/08, Simeon Mattes
The help of all was very useful. But since Jake gave me an example I prefer to follow this up.
Although I 'm not so familiar generally with datatypes I have understood you. It seems in this example that with existential types we can put in the same list different types although generally this is not allowed. I have tried to write this example with the ghc compiler 6.8.2 but there was an error
pare error in data/newtype declaration.
I have also tried to find the etymology of the word existential, since some times somebody can easily find a better answer, but I can't figure out why this is so. (really why "existential" types?). Maybe a completed example would be more helpful.
existence Look up existence at Dictionary.com c.1384, from O.Fr. existence, from L.L. existentem "existent," prp. of L. existere "stand forth, appear," and, as a secondary meaning, "exist;" from ex- "forth" + sistere "cause to stand" (see assist). Existential as a term in logic is from 1819. Existentialism is 1941 from Ger. Existentialismus (1919), ult. from Dan. writer Søren Kierkegaard (1813-55), who wrote (1846) of Existents-Forhold "condition of existence," existentielle Pathos, etc.
(I hope this way of questioning is not so strange)
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Hi Ryan, On Feb13, Ryan Ingram wrote:
However, you can express "exists" in terms of "forall": exists x, P(x) is equivalent to (not (forall x, not P(x))) that is, if it is not true for all x that P(x) does not hold, then there must be some x for which it does hold.
The existential types extension to haskell uses this dual: data Number = forall a. Num a => N a
means that the constructor N has type N :: forall a. Num a => a -> Number
Actually, the encoding of existential types doesn't use the negation trick, which doesn't even work in intuitionistic logic. The encoding of existentials is just currying: Given a function of type (A , B) -> C we can produce a function A -> B -> C "exists" is a lot like pairing, and "forall" is a lot like ->. So if all we want is existentials to the left of an -> we can just curry them away: (exists a.B) -> C becomes forall a. B -> C The existential type extension allows forall's to the left of the -> in the signature of a datatype constructor, so constructors can have existentially bound variables. I.e. data AnyNum where N : forall a. Num a => a -> AnyNum could just as well be written data AnyNum = N (exists a. Num a and a) but Haskell doesn't allow the latter syntax. -Dan
On Wed, 2008-02-13 at 16:31 -0500, Dan Licata wrote:
Hi Ryan,
On Feb13, Ryan Ingram wrote:
However, you can express "exists" in terms of "forall": exists x, P(x) is equivalent to (not (forall x, not P(x))) that is, if it is not true for all x that P(x) does not hold, then there must be some x for which it does hold.
The existential types extension to haskell uses this dual: data Number = forall a. Num a => N a
means that the constructor N has type N :: forall a. Num a => a -> Number
Actually, the encoding of existential types doesn't use the negation trick, which doesn't even work in intuitionistic logic.
The encoding of existentials is just currying:
Given a function of type
(A , B) -> C
we can produce a function
A -> B -> C
"exists" is a lot like pairing, and "forall" is a lot like ->. So if all we want is existentials to the left of an -> we can just curry them away:
(exists a.B) -> C
becomes
forall a. B -> C
Or categorically: Existentials are left adjoints. Universals are the dual of existentials. (->) is continuous in its first argument (because it's a right adjoint [to itself no less]) so it takes limits to limits, but it's also contravariant so it takes limits in the opposite category to limits or, effectively, it takes colimits to limits. Since we know the relevant universals exist, we have the above by continuity of right adjoints.
Oops, I was hasty in typing those data definitions. They will not work because they have no constructors. Sorry about that. - Jake
participants (8)
-
Dan Licata -
Daniil Elovkov -
Derek Elkins -
Felipe Lessa -
Henning Thielemann -
Jake McArthur -
Ryan Ingram -
Simeon Mattes