ExistentialQuantifier

[John Meacham]

On Tue, Feb 14, 2006 at 11:56:25PM +0000, Ross Paterson wrote:
> Is this the same as ExistentialQuantification?
> (And what would an existential in a covariant position look like?)

well, the ExistentialQuantification page is restricted to declaring data types
as having existential components. in my opinion that page name is
something of a misnomer. by ExistentialQuantifiers I mean being able
to use 'exists <vars> . <type>' as a first class type anywhere you can
use a type.

data Foo = Foo (exists a . a) 
type Any = exists a . a 

by the page I mainly meant the syntatic use of being able to use
'exists'. Depending on where your type system actually typechecks it as
proper, it implys other extensions.

if you allow them as the components of data structures, then that is
what the current ExistentialQuantification page is about, and all
haskell compilers support this though with differing syntax as described
on that page.

when existential types are allowed in covarient positions you have
'FirstClassExistentials' meaning you can pass them around just like
normal values, which is a signifigantly harder extension than either of
the other two. It is also equivalent to dropping the restriction that
existential types cannot 'escape' mentioned in the ghc manual on
existential types.

an example might be

returnSomeFoo :: Int -> Char -> exists a . Foo a => a

which means that returnsSomeFoo will return some object, we don't know
what, except that is a member of Foo. so we can use all of Foos class
methods on it, but know nothing else about it. This is very similar to
OO style programing.

when in contravarient position:
takesSomeFoo :: Int -> (exists a . Foo a => a) -> Char
then this can be simply desugared to

takesSomeFoo :: forall a . Foo a => Int -> a -> Char
so it is a signifgantly simpler thing to do.

A plausable desugaring of FirstClassExistentials would be to have them
turn into an unboxed tuple of the value and its assosiated dictionary
and type. but there are a few subtleties in defining the translation as
straight haskell -> haskell (we need unboxed tuples for one :)) but the
translation to something like system F is more straightforward.


there is also room for other extensions between the two which I am
trying to explore with jhc. full first class existentials are somewhat
tricky, but the OO style programming is something many people have
expressed interest in so perhaps there is room for something interesting
in the middle that satiates the need for OO programming but isn't as
tricky as full first class existentials. I will certainly report back
here if I find anything...

Also, someone in the know should verify my theory and terminology :)

        John


-- 
John Meacham - ⑆repetae.net⑆john⑈