11:15 pm, 27 Nov 05

### autrijus

If I haven't pointed it out before, Autrijus Tang's blog is great reading. He's

(What are existential types? I've understood it a number of times and occasionally I discover a pattern I'm looking for while programming is an existential type, but I still don't understand them well enough to tell you the transformation from forall to existential types. Haskell lacks them in part because using that transformation means you can write existential in terms of forall, but they're still useful.)

*the*Perl 6 hacker but for example a recent post is about hacking in existential types into Haskell.(What are existential types? I've understood it a number of times and occasionally I discover a pattern I'm looking for while programming is an existential type, but I still don't understand them well enough to tell you the transformation from forall to existential types. Haskell lacks them in part because using that transformation means you can write existential in terms of forall, but they're still useful.)

awong## Vx P(x) = ~Ex ~P(x) in types?

Vx P(x) = ~Ex ~P(x) is an theorm in first-order boolean logic. IIRC, type systems are supposed to be "rank-2" logic systems (forgot waht rank-2 means, but I don't think it matters here)...so I think this theorm should commute to type theory...But that makes no sense. If you try to expand this analogy,

Vxwould be a forall type (eg. a'xin ML).P, would be a function with a return typeT. However, I can't think of a sensible interpretation of the negations...evan## Re: Vx P(x) = ~Ex ~P(x) in types?

I looked up the Haskell docs (http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html):They use:

`MkFoo :: forall a. a -> (a -> Bool) -> Foo`

and say it has a nearly isomorphic existential type (the below isn't valid Haskell):

`MkFoo :: (exists a . (a, a -> Bool)) -> Foo`