"class []" proposal Re: [Haskell-cafe] One thought: Num to 0 as ? to list?

[Brandon Moore]

Bulat Ziganshin wrote:
> Hello Malcolm,
>
> Tuesday, August 22, 2006, 4:22:50 PM, you wrote:
>
>   
>>> 2) allow to use type classes in type declarations like the types
>>> itself. for example, allow the following:
>>>
>>> f :: Num a => a -> Int
>>> write as
>>> f :: Num -> Int
>>>
>>> and following:
>>>
>>> sequence :: Monad m => [m a] -> m [a]
>>> write as
>>> sequence :: [Monad a] -> Monad [a]
>>>       
I dislike the way mentioning a class implicitly introduces a new type 
variable. To make the dependency explicit you might make the type that 
is supposed to get the constraint a parameter to the class name, like

sequence :: [Monad m a] -> Monad m [a]

>> e class contexts of (for instance)
>>     sequenceLift :: (Monad m, Monad r) => [m a] -> r [a]
>> if it were to be written instead as simply
>>     sequenceLift :: [Monad a] -> Monad [a]
>>     
This type could be written like [Monad m a] -> Monad r [a]

I think this syntax could be done with associated types, if class Monad 
declared an associated type synonym Monad m, and somehow all instances 
were known to define the synonym equal to the type getting the instance. 
Knowing the type Monad m = m only matters if you want to be able to use 
m and Monad m interchangeably.

>> And how would one add multiple class constraints to a single type
>> variable, for instance in:
>>     f :: (Functor m, Monad m) => (a->b) -> m [a] -> m b
>>     
I think it would just be confusing trying to inline constraints, but 
with the associated type interpretation it seems each "constrained 
occurrence" of a type would add another class constraint to the type, so 
maybe you could write
(a -> b) -> Monad m [a] -> Functor m b.
> both your examples cannot be written using proposed syntax
>
> what i propose is not full replacement of existing syntax - quite the
> contrary it is just a syntax sugar for most frequent cases of using
> classes in function signatures. the key idea is that in most cases we
> use only one type class for each type variable, and the same type for
> each occurrence of type class in the type:
>
> (+) :: Num -> Num -> Num
>   
I don't like how this repeats the class name. Repetition of the name a 
in Num a => a -> a -> a is completely different, because the name 'a' is 
just a placeholder for expressing some local sharing in the type.

This reminds me vaguely of the syntax proposed in Daan's paper on MLF, 
where some constraints about polymorphism could be inlined, as in

(x == forall a . a -> a) => [x]->String
-->
[forall a . a -> a] -> String

Maybe there's some similarly useful shorthand here?


> This also simplifies the case when programmer has developed his code
> with one concrete type in mind and later decided to transform it into
> typeclass. In this case my idea allows to retain old definitions in
> most cases (and promoting [] to type class is very typical example
> here! we can browse prelude/list module and count how many definitions
> need to be changed if [] becomes type class)
>   
This really isn't much easier than changing things to use
type classes. Instead of replacing the concrete type with the name of a 
class, you could replace the concrete type with a variable (maybe just 
change the case of the first letter) and add a constraint. Any editor 
smarter than ed should be able to automate either operation. (even sed, 
and pretty trivially if you don't handle multi-line type signatures)

> This proposal born from my experience of using type classes to make
> Streams library more flexible. i found that type signatures using type
> classes becomes larger and less readable and thought that they can be
> made no more complex than ordinary ones by using this idea. Java/C++
> also allows to specify names of abstract classes/interfaces instead of
> concrete classes. Haskell's benefit is that general syntax allows to
> express more complex restrictions. I propose to combine it with the
> OOP-like simple syntax for simple cases (which is 80-90% of total ones)
>
> so, while this proposal is rather minor, i think that it is Good thing
In general, the proposal reminds me a bit of the shorthand proposed in 
Daan Leijen's paper on MLF, available at
http://www.cs.uu.nl/~daan/pubs.html#qmlf

It's a nice type system, but for this message all that matters is that 
MLF handles polymorphism using constraints like
(x = forall a . a -> a) or (y >= forall a . a -> a), which appear in a 
type at the same place as class constraints. His shorthand is to allow 
the right side of a constraint to be embedded directly into a type, 
without naming it at all,
if there is only a single occurrence, and the type is left of an arrow 
for an = constraint, or right for a >= constraint, e.g.

(x = forall a . a -> a, y >= forall a . a -> a) => [x] -> [y]
--->
[forall a . a -> a] -> [forall a . a -> a]

(yes, MLF handles impredicative types quite nicely. Daan's paper shows 
how to add type classes to MLF, making it easy to work with types like 
[forall a . (Show a) => a], and if I read correctly even to infer the 
types in
x1 = [] :: forall a . [a]
x2 = const : x1 :: [forall a b. a -> b -> a]
x3 = min : x2 :: [forall a . (Ord a) -> a -> a -> a]
x4 = (<) : x3 :: [Bool -> Bool -> Bool]
Just the MLF heritage is enough to let you use
($) at type ((forall s . ST s a) -> a) -> (forall s . ST s a) -> a,
eg runST $ return 3 --yay!
)

There are several reasons to think this sort of shorthand would be more 
useful for MLF types than class constraints, but it does seem to be 
quite handy with MLF.

Perhaps there is something similar that could be done with type classes. 
In particular, I very much like Daan's rule of only inlining a 
constraint if the type it binds is only used once, which would mean

Num -> Num -> Num

would be equivalent to

(Num a, Num b, Num c) => a -> b -> c

For an alternate proposal, how about allowing a single-parameter type 
class as an annotation around a subexpression of a type expression, 
meaning the same as a constraint that that subexpression belong to that 
class. For example,

(+) :: Num a -> a -> a,
or
sort :: [Ord a] -> [a]

this is a bit closer to how I would read the types,
"sort takes a list of comparable a to a list of a"

Brandon