| If GHC had true existential typing, as opposed to just | existential datatypes, | you could reasonably code what I think you want like this: | | class A a where | basicA :: Bool | nextA :: a -> (EX a'. A a' => a') | basicA = True | nextA = id Curiously enough, this thread intersects with the "higher-ranked types" thread on the Haskell list. If I do implement the Odersky/Laufer higher-ranked types inference mechanism, then I'll also allow existentials in arbitrary positions. The elimination of "stupid" existential wrapper constructors is discussed in a bit more detail in the paper Mark and I wrote recently: First class modules for Haskell http://research.microsoft.com/~simonpj/papers/first-class-modules/index. htm Simon
On Wednesday 24 October 2001 12:32, Simon Peyton-Jones wrote:
The elimination of "stupid" existential wrapper constructors is discussed in a bit more detail in the paper Mark and I wrote recently:
First class modules for Haskell http://research.microsoft.com/~simonpj/papers/first-class-modules/index.htm
I really like the thrust of the argument. I definitely agree with the direction of the paper. Your paper mentioned the binder rule, which requires an explict type for modules that appear as arguments of functions. I understand the need for this rule, and it is itself a reasonable restriction. The problem is that in combination with a lack of subtyping between records, this implies that one must specify every field that can and must appear in a module. I'm trying to decide if this is a reasonable restriction. From my experiences with other systems such as Modula-3, my instincts say no. Say you are implementing modules for Ints and Floats. My old habits would lead to the following signatures: record Int a = (+), (*) :: a -> a -> a div, mod :: a -> a -> a record Float a = (+),(*):: a -> a -> a (/) :: a -> a -> a sin, cos :: a -> a Then, by my understanding, one could not write a function that mentions only (+) and (*) that is polymorphic in these modules. You couldn't pass it both Int a and Float a, because the signatures are different, which seems to be an artificial restriction. I think extending the system with some form of subtyping between records would be important for a usable system. Your paper suggested that you are planning to do this. Any thoughts on current ideas in this direction? On the other hand, one could split each module up into several different pieces, such as "Ring a", and "Trig a". This might be very reasonable, but it strikes me as being a little too fine-grained. best, leon
participants (2)
-
Leon Smith -
Simon Peyton-Jones