"exists" keyword and "existential" types
I find myself confused by the lack of an "exists" quantifier to complement "forall". It imposes seemingly arbitrary restrictions on the ways in which types can be expressed, and makes some seemingly harmless (and useful) types entirely inexpressible. For example, it seems as though runST could just as well be given the type runST :: forall a. exists s. ST s a -> a This isn't necessarily better than the usual type, but why can't it be expressed? And it might actually be better: introducing exists would make it possible to hoist quantifiers from both sides of the function arrow, rather than just the RHS as GHC does now. And it would be nice to be able to pass around values of type (exists t. Interface t => t), which behave just like OOP interface pointers. I don't see how openInputStream :: FilePath -> IO (exists t. InputStream t => t) would cause any more problems than data Foo = forall t. InputStream t => Foo t openInputStream :: FilePath -> IO Foo What am I missing? While looking through old posts for insight, I came across a thread from last April started by Simon P-J, who wrote:
Many of you have grown to love existential data types, which we current write like this:
data T = forall a. Foo a (a -> Int)
Mark and I chose 'forall' rather than 'exists' to save grabbing another keyword from the programmer. And indeed, the type of the constructor Foo is Foo :: forall a. a -> (a->Int) -> T
But every single time I explain this to someone, I find I have to make excuses for using the term 'forall'. I say "it really means 'exists', but we didn't want to lose another keyword".
I have gradually concluded that our decision was a mistake. (In fairness to Mark, I think I was the primary advocate for it.) I reckon that we should
Allow 'exists' Deprecate 'forall' (for defining existentials, that is) Eventually allow only 'exists'
But I think the use of "forall" in this context is correct, and "exists" incorrect. I find it easy to explain: you're creating many different "Foo" constructors, one for every possible type a, so when you extract a value from a Foo you're getting some type a, but you don't know which. Using "exists" here would express something different, namely that there's only one Foo, but you don't know (and it mustn't matter) what type it expects to be bound to a, and therefore you can't apply Foo to a value unless that value is general enough to encompass all possible types for a. This gives the constructor function a rank-2 type, or equivalently an existentially-quantified variable at the top level. When you match against the value you're getting something which has to be able to stand in for any type. I think the source of confusion is not the use of forall, but the term "existential types". There is nothing existential about them! The type variables involved can be either existentially or universally quantified, depending on the context. They use exists in exactly the contexts where "ordinary" type variables use forall, and vice versa. Instead of changing the forall, I think we should change the name "existential types" to something which approximately reflects what they actually are, like "inaccessible types" or "hidden types". "Abstract types" would also be a possibility, but I think it would be confused with the separate concept of using module scope to hide value constructors. My other suggestions might also cause that kind of confusion, but I still think they're better than "existential types", which seems to have no more to do with the concept being expressed than "left-handed types" or "male types" would have. -- Ben
In article <Pine.LNX.4.21.0402150140100.16014-100000@dark.darkweb.com>, Ben Rudiak-Gould <benrg@dark.darkweb.com> wrote:
And it would be nice to be able to pass around values of type (exists t. Interface t => t), which behave just like OOP interface pointers.
A value of "type" (exists t. Interface t => t) consists of two values, one of type t, and one "dictionary" value. For that reason a data type is used to represent this (and a newtype type cannot be). So what's the difference? Data provides another layer of "thunkage". For instance: data D = MkD Int; newtype N = MkN Int; Then (MkN undefined) is the same as undefined, but (MkD undefined) is not. So how does this apply to (exists t. Interface t => t)? Well, you'd have two different versions of "undefined" depending on whether calculation of the dictionary was part of the undefinition.
I don't see how
openInputStream :: FilePath -> IO (exists t. InputStream t => t)
Bear in mind you can't even write IO (forall t. whatever) in Haskell.
would cause any more problems than
data Foo = forall t. InputStream t => Foo t openInputStream :: FilePath -> IO Foo
What am I missing?
Simply that undefined is not the same as (Foo undefined). Quite separately, if InputStream happens to look like this: class InputStream t where { f1 :: t -> something; f2 :: t -> something'; f3 :: t -> something''; -- etc. }; where none of the somethings refer to t, you'd be better off with a data-type: data InputStream { f1 :: something; f2 :: something'; f3 :: something''; -- etc. }; This is a much better way of doing semi-OOP. AFAIK you can't really do proper OOP-style extensibility in Haskell at all (and "exists" wouldn't help either). -- Ashley Yakeley, Seattle WA
On Mon, 16 Feb 2004, Ashley Yakeley wrote:
A value of "type" (exists t. Interface t => t) consists of two values, one of type t, and one "dictionary" value. For that reason a data type is used to represent this (and a newtype type cannot be).
This is an implementation detail, though. It's like a function with one declared parameter actually having two parameters, the other one a dictionary. We don't have to box the explicit parameter so that the implicit one can be propagated along with it.
So what's the difference? Data provides another layer of "thunkage". For instance:
data D = MkD Int; newtype N = MkN Int;
Then (MkN undefined) is the same as undefined, but (MkD undefined) is not.
I think this is orthogonal to the issue at hand. If there really is more than one kind of undefined for (exists t. Interface t => t) (which I don't think there is -- see below), then boxing it would just add yet another kind.
So how does this apply to (exists t. Interface t => t)? Well, you'd have two different versions of "undefined" depending on whether calculation of the dictionary was part of the undefinition.
Dictionary calculation can never diverge, can it? They only depend on the type, so if the program type-checks then it's always possible to construct every dictionary. If the dictionary is stored with the value in an unlifted pair, then there's only one kind of "undefined". And in any case, if problems like this really existed, they would apply equally to implicit dictionary arguments, which seem to work without a hitch. I'm effectively just proposing that we add implicit dictionary return values.
openInputStream :: FilePath -> IO (exists t. InputStream t => t)
Bear in mind you can't even write IO (forall t. whatever) in Haskell.
True, but why is this? Is there a deep reason why we can use nested foralls as the arguments to (->), but not as the arguments to any other type constructor?
data InputStream { f1 :: something; f2 :: something'; f3 :: something''; -- etc. };
This is a much better way of doing semi-OOP.
I agree that this is a useful technique, but I'd still like to explore the other possibilities. This technique won't help with my implicit parameter state-threading proposal, for one thing.
AFAIK you can't really do proper OOP-style extensibility in Haskell at all (and "exists" wouldn't help either).
Probably true. But I tend to use abstract interfaces far more often than subtype polymorphism when I program in C++; I'd hardly notice the difference if C++ didn't support inheritance at all. I don't know how true this is of other people. -- Ben
In article <Pine.LNX.4.21.0402161643310.20625-100000@dark.darkweb.com>, Ben Rudiak-Gould <benrg@dark.darkweb.com> wrote:
Bear in mind you can't even write IO (forall t. whatever) in Haskell.
True, but why is this? Is there a deep reason why we can use nested foralls as the arguments to (->), but not as the arguments to any other type constructor?
Apparently it makes type-checking Very Very Hard. Simon PJ may have explained it to me ("impredicative", he called it), but I don't remember offhand. -- Ashley Yakeley, Seattle WA
On Tue, 17 Feb 2004 14:40:18 -0800, Ashley Yakeley <ashley@semantic.org> wrote:
Ben Rudiak-Gould <benrg@dark.darkweb.com> wrote:
Bear in mind you can't even write IO (forall t. whatever) in Haskell.
True, but why is this? Is there a deep reason why we can use nested foralls as the arguments to (->), but not as the arguments to any other type constructor?
Apparently it makes type-checking Very Very Hard. Simon PJ may have explained it to me ("impredicative", he called it), but I don't remember offhand.
Whenever you instantiate type variables with type schemes, you are impredicative. Impredicative instantiation makes type checking (much) harder -- without extra constraints, you don't even have principal types. i.e. choose :: a -> a -> a choose x y = x What is the type of "choose id" if your system is impredicative? Either "forall a. (a -> a) -> (a -> a)" or "(forall a. a->a) -> (forall a. a->a)" Note that neither of these types subsumes the other. This is why MLF adds extra constraints which enables them to give a principle type to this expression. (namely: forall a. (a >= forall a. a -> a) => a -> a) Anyway, Ben Rudiak's particular case, namely instantiating arguments of a type with type schemes, is difficult due to another problem. It is very hard to know whether an argument to a type is used contra-variantly or co-variantly (or both, or not at all). This means that we can't do a proper subsumption check on type schemes. i.e. data Contra a = Contra (a -> Int) data Co a = Co (Int -> a) data None a = None data Both a = Contra (a -> Int) | Co a In this case it may seem trivial to infer the contra/co variance of the argument but try this with some type constructors as arguments :-) In a particular case one can give type rules of course, for example for tuples or the IO monad. All the best, Daan.
On Wed, 18 Feb 2004, Daan Leijen wrote:
choose :: a -> a -> a choose x y = x
What is the type of "choose id" if your system is impredicative? Either "forall a. (a -> a) -> (a -> a)" or "(forall a. a->a) -> (forall a. a->a)" Note that neither of these types subsumes the other.
This is bad, but it doesn't seem any worse than what we've got already in GHC and Hugs. In fact, what we've got is much worse: not only can't we infer most general types, we can't even determine the meaning of a correct program without looking at explicit type signatures.
Anyway, Ben Rudiak's particular case, namely instantiating arguments of a type with type schemes, is difficult due to another problem. It is very hard to know whether an argument to a type is used contra-variantly or co-variantly (or both, or not at all).
I noticed that problem but didn't think about the difficulties of type constructor parameters. It seems like you could make this work by extending the kind system, but maybe it's not worth it. -- Ben
Ben Rudiak-Gould wrote:
... we can't even determine the meaning of a correct program without looking at explicit type signatures.
So what? Can we do this in other languages? Do we want it? I think not. The Haskell design (of type inference rather than type checking) has the strange feeling of "our types are so strong that you can completely avoid (writing) them". To me, this seems contrary to sound software engineering. -- -- Johannes Waldmann, Tel/Fax: (0341) 3076 6479 / 6480 -- ------ http://www.imn.htwk-leipzig.de/~waldmann/ ---------
Hi
Ben Rudiak-Gould wrote:
... we can't even determine the meaning of a correct program without looking at explicit type signatures.
Johannes Waldmann wrote:
So what? Can we do this in other languages? Do we want it? I think not.
The Haskell design (of type inference rather than type checking) has the strange feeling of "our types are so strong that you can completely avoid (writing) them". To me, this seems contrary to sound software engineering.
To a large extent, I would agree with this remark. It seems to me that (1) We should write types when we are telling the compiler what the plan is. (2) We should not need to write types (or at least not often) to convince the compiler that we are following the plan. Indeed, if one replaces `compiler' in the above by `editor', one begins to discover that the writing of an explicit type signature can assist us in determining not merely the meaning of a correct program, but the program itself. The writing of explicit type signatures (and in particular, class constraints) serves more than the practical necessity of helping a dim computer to cope and more than the moral purpose of disciplined documentation. It gives programmers a very compact language for describing a great deal of tedious plumbing. That's really good. Types are not and should not be regarded as passive things which machines check and programmers try to ignore. One only needs to look at what, in toto, Haskell compilers actually do with types (let alone what editors could do), to see that writing a type can be a highly effective act of programming, and hence that reading types can be a very efficient means of program comprehension. It's not types we should be not reading or not writing: it's the boring bits of programs. Cheers Conor
participants (5)
-
Ashley Yakeley -
Ben Rudiak-Gould -
Conor McBride -
Daan Leijen -
Johannes Waldmann