# Difference between revisions of "Quantified contexts"

(Another class system extension proposal) |
|||

Line 106: | Line 106: | ||

guard :: (Monad m, Monoid (m ())) => Bool -> m () |
guard :: (Monad m, Monoid (m ())) => Bool -> m () |
||

</haskell> |
</haskell> |
||

+ | |||

+ | == Response from SimonPJ == |
||

+ | |||

+ | I didn't see how Section 3 |
||

+ | addressed the issues raised in Sections 1 and 2. For example, to avoid |
||

+ | the cascade of `Typeable2`, `Typeable3` etc classes the solution is |
||

+ | presumably polymorphism at the kind level. (Tim Sheard's language Omega |
||

+ | has this.) |
||

+ | |||

+ | Still, I recognise the merit of quantification in contexts. Indeed, Ralf |
||

+ | Hinze and I suggested it back in 2000 in Section 7 of |
||

+ | [[http://research.microsoft.com/en-us/um/people/simonpj/papers/derive.htm |
||

+ | Derivable type classes]]. (This section is rather independent of the rest |
||

+ | of the paper.) |
||

+ | |||

+ | However, attractive as it is, it's quite a big step to add something akin |
||

+ | to local instance declarations. Our ICFP'08 paper |
||

+ | [[http://research.microsoft.com/~simonpj/papers/assoc-types/index.htm Type |
||

+ | checking with open type functions]] relies rather crucially on ''not'' |
||

+ | having such local instances. (We've managed to simplify the algorithm |
||

+ | quite a bit since then, but it still relies on that assumption.) |
||

+ | |||

+ | So I'm not sure I see how to make quantified contexts compatible with type |
||

+ | functions, and all the other stuff in Haskell. But their lack is clearly |
||

+ | a wart, and one that may become more pressing. |
||

+ | |||

+ | Meanwhile, clarifying the proposal would be a good thing, even if it's not |
||

+ | adopted right away. |

## Revision as of 10:47, 14 January 2009

## The problem

The base library currently contains (essentially) the following classes:

```
class Monoid a where
mempty :: a
mappend :: a -> a -> a
class MonadPlus m where
mzero :: m a
mplus :: m a -> m a -> m a
class ArrowPlus c where
arrowZero :: c a b
arrowPlus :: c a b -> c a b -> c a b
```

If you look closely '*these are all the same*.
The only difference is in the superclasses and in the arity of the argument.
You will find that any class that is an instance of MonadPlus can be made an instance of Monoid.
In fact, some types such as lists, are indeed instances of both classes.

This leads to duplication of code and of extra names for what is essentially the same thing.
When should you use `mappend`

instead of `mplus`

, and when shouldn't you?

This exact same situation is also found in the `Data.Typeable`

module, which has the classes:

```
class Typeable a where
typeOf :: a -> TypeRep
class Typeable1 t where
typeOf1 :: t a -> TypeRep
class Typeable2 t where
typeOf2 :: t a b -> TypeRep
-- etc.
```

## Chained instances

This Typeable library comes with instances

```
instance (Typeable2 t, Typeable a) => Typable (t a)
instance (Typeable3 t, Typeable a) => Typable2 (t a)
-- etc.
```

Which means that only one instance of `typeableN`

has to be written for a type constructor with arity n.

We could do the same for `Monoid`

.
The `MonadPlus`

and `ArrowPlus`

classes can not be used for this purpose, because they require `Monad`

and `Arrow`

superclasses.
But we could add `Monoid1`

, `Monoid2`

, etc.

```
class Monoid2 t where
mempty2 :: t a
mappend2 :: t a -> t a -> t a
class Monoid3 t where
mempty3 :: t a b
mappend3 :: t a b -> t a b -> t a b
instance Monoid2 t => Monoid (t a) where
mempty = mempty2
mappend = mappend2
```

`MonadPlus`

can then be a class alias or simply a subclass of both `Monad`

and `Monoid2`

.

```
class (Monad m, Monoid2 m) => MonadPlus m
```

A big disadvantage of these instances is that it is an all or nothing aproach.
It is no longer possible to declare an `instance Monoid (t a)`

directly, because it overlaps with the instance using `Monoid2`

.
Usually this is not a big problem, but it also forces the parameter of the type constructor to have kind `*`

and there can't be constraints on it.

For example there is currently an instance

```
instance Ord k => Monoid (Map k v)
```

This would become imposible, because the instance would need be

```
instance Monoid2 Map -- we need Ord
```

## Quantified contexts

An alternative would be a small extension of the Haskell language to allow quantifiers in contexts. Where we now write

```
function :: (Class a, Another (t a)) => Type a
```

We would also allow

```
function :: (forall b. Ctx => SomeClass b) => Type
```

The meaning is simple, to satisfy this context, an instance

```
instance Ctx => SomeClass b
```

is needed (or a more general one).

We can use these quantified contexts in the `Monoid`

example as:

```
class (Monad m, forall a. Monoid (m a)) => MonadPlus m
```

or without the superflous extra class, for example

```
guard :: (Monad m, forall a. Monoid (m a)) => Bool -> m ()
```

The compiler will never infer a quantified context; the above type is not the most general type of guard. If you gave no type signature the compiler would infer

```
guard :: (Monad m, Monoid (m ())) => Bool -> m ()
```

## Response from SimonPJ

I didn't see how Section 3 addressed the issues raised in Sections 1 and 2. For example, to avoid the cascade of `Typeable2`, `Typeable3` etc classes the solution is presumably polymorphism at the kind level. (Tim Sheard's language Omega has this.)

Still, I recognise the merit of quantification in contexts. Indeed, Ralf Hinze and I suggested it back in 2000 in Section 7 of [[http://research.microsoft.com/en-us/um/people/simonpj/papers/derive.htm Derivable type classes]]. (This section is rather independent of the rest of the paper.)

However, attractive as it is, it's quite a big step to add something akin
to local instance declarations. Our ICFP'08 paper
[[http://research.microsoft.com/~simonpj/papers/assoc-types/index.htm Type
checking with open type functions]] relies rather crucially on *not*
having such local instances. (We've managed to simplify the algorithm
quite a bit since then, but it still relies on that assumption.)

So I'm not sure I see how to make quantified contexts compatible with type functions, and all the other stuff in Haskell. But their lack is clearly a wart, and one that may become more pressing.

Meanwhile, clarifying the proposal would be a good thing, even if it's not adopted right away.