[Haskell] Re: "exists" keyword and "existential" types

[Ben Rudiak-Gould]

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