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⑈