Existential types: want better syntactic support (autoboxing?)

[Cale Gibbard]

On 27/01/06, Johannes Waldmann <waldmann at imn.htwk-leipzig.de> wrote:
> S.J.Thompson wrote:
> > Johannes - thanks for the pointer to this posting; would you have a
> > concrete proposal to make on the basis of this for Haskell'?
>
> Sort of an idea, but not fully worked out.
>
> Referring to
> http://www.haskell.org//pipermail/haskell-cafe/2005-June/010516.html
> I think I want to use exactly this implementation (class Figure, data
> EFigure) but hide the existence of EFigure (on the type level
> and on the data level) completely, by some syntax.
>
>
> E. g. a list of Figures could be written as [ Figure ], using the class
> name as a type name (for the special case where the class is unary).
> (This is what the Java people do but I am not sure whether this is
> a good idea in the Haskell context. Mixing types and classes, hm.)
>
>
> Also, when constructing objects of type EFigure, as in
>
> box :: Size -> EFigure ; box s = EFigure $ Box { ... }
>
> I want to omit the constructor EFigure,
> and the function should just read
>
> box :: Size -> Figure ; box s = Box { ... }
>
> This is the auto-boxing I was referring to in the subject of this mail.
> (We don't need auto-unboxing as we can have instance Figure EFigure,
> see the reference).
>
> While this is auto-boxing of function results (i. e. on exports),
> a more difficult question is, how should we do auto-boxing for
> function arguments (i. e. on imports). Assume f :: Foo -> Box
> and g : Figure -> Bar,  is  g ( f Foo )  OK? Probably yes,
> by translating to  g ( EFigure ( f Foo ) ). But then what about
> f2 :: Foo -> [ Box ]  and  g2 :: [ Figure ] -> Bar.
> We would need  g2 . f2  translated to  g2 . fmap EFigure . f2
> but of course at runtime, there should be no extra cost.
>
>
> (I'll have one more comment which I send in a separate message
> so that it shows up under its own header in the archive.)
>

How do we decide which constructor to apply, or even which existential
type is desired? What happens if there are multiple arguments?

Applying existential constructors essentially throws some type
information out the window -- right along with the priveleges that go
along with that information. You're essentially saying, "I never want
to be able to access the implementation of this data again, only
allowing operations via these specific typeclasses". I wouldn't
consider it an operation to be taken lightly. In Java, you see a lot
of casting things back to their original types, but of course, that's
not safe, and in Haskell, it's not even possible (and that's probably
for the best). DWIMmery here doesn't really seem appropriate to me, as
this is exactly the sort of large-scale design point you want to be
extra careful about in your code.

Perhaps you disagree? :) I'm not exactly sure what kind of design
you're thinking of where it's so inconvenient to apply the constructor
by hand that it would warrant this kind of change to the language --
perhaps you could give an example. :)

One of the things which I really like about Haskell is that it
generally forces you to think about conversions between types in an
appropriate manner. You have to apply fromIntegral to convert from
Integer to Double, and that's a good thing, because it reminds you of
all the problems that potentially can go along with that. Passing from
a concrete type to an existential type is a big deal, and I think it's
usually a good idea to have an extra reminder of when it's happening.

 - Cale