11:15 pm, 27 Nov 05
autrijus
If I haven't pointed it out before, Autrijus Tang's blog is great reading. He's 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.)
(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.)
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, Vx would be a forall type (eg. a 'x in ML). P, would be a function with a return type T. However, I can't think of a sensible interpretation of the negations...
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) -> Fooand say it has a nearly isomorphic existential type (the below isn't valid Haskell):
MkFoo :: (exists a . (a, a -> Bool)) -> Foo