# Quantified contexts

### From HaskellWiki

(Another class system extension proposal) |
(Clarified proposal by desugaring to dictionaries) |
||

(2 intermediate revisions by 2 users not shown) | |||

Line 13: | Line 13: | ||

arrowZero :: c a b |
arrowZero :: c a b |
||

arrowPlus :: c a b -> c a b -> c a b |
arrowPlus :: c a b -> c a b -> c a b |
||

+ | class Alternative f where |
||

+ | empty :: f a |
||

+ | (<|>) :: f a -> f a -> f a |
||

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

− | If you look closely '''these are all the same''. |
+ | If you look closely ''these are all the same''. |

The only difference is in the superclasses and in the arity of the argument. |
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. |
You will find that any class that is an instance of MonadPlus can be made an instance of Monoid. |
||

Line 63: | Line 66: | ||

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

− | A big disadvantage of these instances is that it is an all or nothing aproach. |
+ | A big disadvantage of these instances is that it is an all or nothing approach. |

It is no longer possible to declare an <hask>instance Monoid (t a)</hask> directly, because it overlaps with the instance using <hask>Monoid2</hask>. |
It is no longer possible to declare an <hask>instance Monoid (t a)</hask> directly, because it overlaps with the instance using <hask>Monoid2</hask>. |
||

Usually this is not a big problem, but it also forces the parameter of the type constructor to have kind <hask>*</hask> and there can't be constraints on it. |
Usually this is not a big problem, but it also forces the parameter of the type constructor to have kind <hask>*</hask> and there can't be constraints on it. |
||

Line 96: | Line 99: | ||

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

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

− | or without the superflous extra class, for example |
+ | or without the superfluous extra class, for example |

<haskell> |
<haskell> |
||

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

Line 106: | Line 109: | ||

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

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

+ | |||

+ | === How this replaces chained instances === |
||

+ | With quantified contexts the typeOfN functions can have the type signatures: |
||

+ | <haskell> |
||

+ | typeOf :: Typeable a => a -> String -- member of class Typeable |
||

+ | typeOf1 :: (forall a. Typeable (t a)) => t a -> String |
||

+ | typeOf2 :: (forall a b. Typeable (t a b)) => t a b -> String |
||

+ | </haskell> |
||

+ | A Typeable instance could be used where right now the 'Typeable1' class would be needed, for example |
||

+ | <haskell> |
||

+ | thisUsesTypeOf1 :: (forall a. Typeable (t a)) => (forall a. t a) -> String |
||

+ | thisUsesTypeOf1 empty = typeOf1 (empty :: t Int) ++ typeOf1 (empty :: t Bool) |
||

+ | |||

+ | instance Typeable (Set a) where ... |
||

+ | test = thisUsesTypeOf1 (Data.Set.empty :: forall a. Set a) |
||

+ | </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. |
||

+ | |||

+ | |||

+ | == Description in terms of dictionaries == |
||

+ | |||

+ | The idea of quantified contexts is best described in terms of the dictionary transformation. |
||

+ | A normal type class constraint like |
||

+ | <haskell> |
||

+ | f :: Monoid a => a |
||

+ | </haskell> |
||

+ | becomes |
||

+ | <haskell> |
||

+ | f :: MonoidDict a -> a |
||

+ | </haskell> |
||

+ | |||

+ | The translation for quantified contexts would use Rank2Types: |
||

+ | <haskell> |
||

+ | f :: forall a. Monoid (m a) => m a |
||

+ | </haskell> |
||

+ | becomes |
||

+ | <haskell> |
||

+ | f :: (forall a. MonoidDict (m a)) -> m a |
||

+ | </haskell> |
||

+ | |||

+ | Invoking such a function f is only possible if there is an instance in scope of the form "<hask>instance Monoid (SomeM a)</hask>". In other words, the compiler must be able to construct a value of type <hask>forall a. MonoidDict (m a)</hask> when f is invoked. |
||

+ | |||

+ | Higher rank types are also possible in principle, so you could have |
||

+ | <haskell> |
||

+ | f :: (forall a. Ord a => Monoid (m a)) => m a |
||

+ | </haskell> |
||

+ | The dictionary argument to f is now a function, which when given an OrdDict a gives back a MonoidDict (m a). |
||

+ | |||

+ | == How this works with type functions? == |
||

+ | |||

+ | Consider the function |
||

+ | <haskell> |
||

+ | problem :: (forall a. MyClass (MyTypeFunction a)) => ... |
||

+ | </haskell> |
||

+ | The only way to invoke 'problem' is if there were an instance |
||

+ | <haskell> |
||

+ | instance MyClass (MyTypeFunction a) where ... |
||

+ | </haskell> |
||

+ | I.e. with a type variable in the instance head. Assuming you could declare such an instance, there is no reason why it can't be used as an to satisfy a quantified context. |

## Latest revision as of 19:49, 1 May 2010

## Contents |

## [edit] 1 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 class Alternative f where empty :: f a (<|>) :: f a -> f a -> f a

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 useclass Typeable a where typeOf :: a -> TypeRep class Typeable1 t where typeOf1 :: t a -> TypeRep class Typeable2 t where typeOf2 :: t a b -> TypeRep -- etc.

## [edit] 2 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.

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

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

A big disadvantage of these instances is that it is an all or nothing approach.

It is no longer possible to declare anFor 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

## [edit] 3 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 theclass (Monad m, forall a. Monoid (m a)) => MonadPlus m

or without the superfluous 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 ()

### [edit] 3.1 How this replaces chained instances

With quantified contexts the typeOfN functions can have the type signatures:

typeOf :: Typeable a => a -> String -- member of class Typeable typeOf1 :: (forall a. Typeable (t a)) => t a -> String typeOf2 :: (forall a b. Typeable (t a b)) => t a b -> String

A Typeable instance could be used where right now the 'Typeable1' class would be needed, for example

thisUsesTypeOf1 :: (forall a. Typeable (t a)) => (forall a. t a) -> String thisUsesTypeOf1 empty = typeOf1 (empty :: t Int) ++ typeOf1 (empty :: t Bool) instance Typeable (Set a) where ... test = thisUsesTypeOf1 (Data.Set.empty :: forall a. Set a)

## [edit] 4 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.

## [edit] 5 Description in terms of dictionaries

The idea of quantified contexts is best described in terms of the dictionary transformation. A normal type class constraint like

f :: Monoid a => a

becomes

f :: MonoidDict a -> a

The translation for quantified contexts would use Rank2Types:

f :: forall a. Monoid (m a) => m a

becomes

f :: (forall a. MonoidDict (m a)) -> m a

Higher rank types are also possible in principle, so you could have

f :: (forall a. Ord a => Monoid (m a)) => m a

The dictionary argument to f is now a function, which when given an OrdDict a gives back a MonoidDict (m a).

## [edit] 6 How this works with type functions?

Consider the function

problem :: (forall a. MyClass (MyTypeFunction a)) => ...

The only way to invoke 'problem' is if there were an instance

instance MyClass (MyTypeFunction a) where ...

I.e. with a type variable in the instance head. Assuming you could declare such an instance, there is no reason why it can't be used as an to satisfy a quantified context.