On 27/01/06, Johannes Waldmann 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

On 1/30/06, Johannes Waldmann wrote:

How can we achieve the same effect in Haskell?

I see no reason why we can't create an existential datatype for every single-parameter type class, perhaps with autoboxing. -- Taral "Computer science is no more about computers than astronomy is about telescopes." -- Edsger Dijkstra

On Mon, 2006-01-30 at 18:13 +0100, Sebastian Sylvan wrote:

Seems like a convenient feature to me.

Also, you may want to have a function which works on a list of any values which are both readable and showable. Say (mockup syntax):

foo :: => [a] foo = [ 1, True, myRocketLauncher ]

Which would create a newtype called "ShowReadAble" or something with extistential types and also instantiate that type in both Show and Read.

I do agree that this is something I'd like in a lot of cases, and it probably would be used quite a bit more if it were convenient (and standardised!).

I leave it to someone else to figure out how to make this play nice with e.g. type inference.

I have often thought that it would be useful to have an existential corresponding to a class. There are several examples in Haskell where one wants to manipulate lists of values that support a common interface but are not necessarily the same type. Haskell makes it very convenient to do type based static dispatch but rather inconvenient to do runtime value dispatch. In general the preference for type based static dispatch is good. In OOP languages people often use the OOP value based dispatch when the Haskell style would be more appropriate, but it is not convenient in those languages. On the other hand there are sometimes when it really is better to do the value base dispatch. For example an extensible IO Handle data type. It is necessary to have lists of Handles so we can't have a Handle type class. One could have a record of functions. When I thought about this before I came to the conclusion that it would be convenient to be able to have a type class and a corresponding data type with the same name. The class gives the interface and the data type can be made a member of the type: class IStream s where readBlock :: s -> IO Block data IStream = IStream { istream_readBlock :: IO Block } instance IStream IStream where readBlock s = istream_readBlock s abstractIStream :: IStream s => s -> IStream abstractIStream s = IStream { istream_readBlock = readBlock s } So this allows us to have a type class so we can do ordinary type class stuff or if we need to manipulate streams of different underlying types only via their IStream interface then we can use abstractIStream to convert any instance of the IStream class to its most general instance, namely the IStream data type. But the above translation is a bit cumbersome and could be optimised. What's really going on is we're just converting from a class dictionary to an explicit dictionary. If this sort of thing were supported directly in the language then the dictionary conversion would be a no-op. So to summarise the feature, it might be nice to make doing runtime value-based dispatch through an interface (almost as) easy as the existing class mechanism which allows static type-based dispatch through an interface. Also to allow explicit conversion from one form to the other (anything in the class to a most general instance). Duncan

Am Montag, 30. Januar 2006 19:02 schrieb Duncan Coutts:

[...]

I have often thought that it would be useful to have an existential corresponding to a class.

How would this work with multi-parameter classes, constructor classes, etc.? If you propose something that only works in conjunction with a special kind of classes I would hesitate to include such thing in a Haskell standard. I think that it would often be nice to have Template Haskell standardized and implement features like autoboxing via some library using Template Haskell. This way, we would keep the actual language small but open the door for lots of useful extensions. This principle of a small but powerful (extensible) language is used already a lot without Template Haskell, so why not use it also in conjunction with Template Haskell in cases like the autoboxing approach.

[...]

Best wishes, Wolfgang

On Tue, 2006-01-31 at 13:28 +0000, Duncan Coutts wrote:

On Tue, 2006-01-31 at 13:59 +0100, Wolfgang Jeltsch wrote:

...

Am Montag, 30. Januar 2006 19:02 schrieb Duncan Coutts:

...

[...]

...

I have often thought that it would be useful to have an existential corresponding to a class.

How would this work with multi-parameter classes, constructor classes, etc.? If you propose something that only works in conjunction with a special kind of classes I would hesitate to include such thing in a Haskell standard.

As John Mecham said it'd be for single parameter type class with a parameter of kind *.

But you're probably right that people should get more experience with using this technique before giving special support in the language to make it convenient.

As Bulat noted we can already use this construction:

class (Monad m) => Stream m h | h->m where vClose :: h -> m () vIsEOF :: h -> m Bool .....

data Handle = forall h . (Stream IO h) => Handle h

instance Stream IO Handle where vClose (Handle h) = vClose h vIsEOF (Handle h) = vIsEOF h .....

But we have to give the name of the most general instance a different name to the class which is rather inconvenient.

So perhaps we should start with allowing a class a data type to have the same name and in a future standard think about making it easy to define Bulat's Handle instance above with a short hand like:

class (Monad m) => Stream m h | h->m where vClose :: h -> m () vIsEOF :: h -> m Bool ..... deriving data Stream

Actually this is unnecessary. All we need is: class (Monad m) => Stream m h | h->m where vClose :: h -> m () vIsEOF :: h -> m Bool newtype Handle = exists s. Stream s => Handle s deriving Stream So all we need is existentials and newtype-deriving. Duncan

so if I understand this proposal properly, it would mean the following every single parameter type class whole parameter is of kind * class Foo a where automatically declares a data type defined as data Foo = exists a . Foo a => Foo_ a (where Foo_ is some internal, non user accessable name) and an instance instance Foo Foo where method (Foo_ x) = method x ... this all seems quite nice, I really like it, we can always determine whether a name is a class or type from context (I think the only reason the namespaces are combined is due to import/export lists) the only issue is the autoboxing. we can't introduce an actual constructor because constructors are in a different namespace. so we would need to automatically turn anything of type Foo a => a into a Foo when it is used as such. it should be possible, but the exact changes to typechecking needed might be subtle.. an alternative might be to just allow existential types in structures so we can have [exists a . Foo a => a], but that probably has its own can of worms... John -- John Meacham - ⑆repetae.net⑆john⑈

On Tue, Jan 31, 2006 at 02:26:02AM +0000, Philippa Cowderoy wrote:

On Mon, 30 Jan 2006, John Meacham wrote:

...

an alternative might be to just allow existential types in structures so we can have [exists a . Foo a => a], but that probably has its own can of worms...

Yup. The boxy types paper gives us impredicativity and allows us to define the type, but in GHC you can't allow [exists a . num a => a] to subsume [Int] because that'd require mapping across the list to add in the dictionaries. You can hack it for lists, but you can't do it for general structures.

I believe JHC could handle it fine though.

well, jhc would also need to pass a type parameter rather than a dictionary in so it would likely have a similar issue. although, that raises another good point about autoboxing, [Foo] and [Int] would necessarily be different types. so how would you convert [Int] to [Foo]? (map id)? yeah, I am more convinced that the proposal is good except for the autoboxing bit, we will have to introduce some sort of explicit boxing operation, but the type of said operator would be quite odd.. if we make the requirement it be called monomorphically in 'c' then it becomes simpler, but still.. it is very warty.. introducing a dataconstructor for each class might be the only way to go. box :: forall (c::class) (a::*) . c a => a -> (c::*) notice the wacky made up quantification over classes, and the fact that (c::*) and (c::class) are not the same, but are linked... not very good. John -- John Meacham - ⑆repetae.net⑆john⑈

On Mon, 2006-01-30 at 18:20 -0800, John Meacham wrote:

so if I understand this proposal properly, it would mean the following

every single parameter type class whole parameter is of kind * class Foo a where

automatically declares a data type defined as

data Foo = exists a . Foo a => Foo_ a (where Foo_ is some internal, non user accessable name)

and an instance

instance Foo Foo where method (Foo_ x) = method x ...

this all seems quite nice, I really like it, we can always determine whether a name is a class or type from context (I think the only reason the namespaces are combined is due to import/export lists)

the only issue is the autoboxing. we can't introduce an actual constructor because constructors are in a different namespace. so we would need to automatically turn anything of type Foo a => a into a Foo when it is used as such.

Is that really necessary (or desirable)? As it was suggested in the thread on existential types it probably wants to be made explicit when you throw away type information by putting something behind an interface. How about just making the conversion "Foo a => a -> Foo" explicit? And of course the conversion is just the constructor Foo. Duncan

Am Dienstag, 31. Januar 2006 03:20 schrieb John Meacham:

[...]

an alternative might be to just allow existential types in structures so we can have [exists a . Foo a => a], but that probably has its own can of worms...

But it sounds very reasonable to me, more reasonable than the autoboxing approach :-(.

John

Best wishes, Wolfgang