On 21 June 2015 at 15:55, Michael Walker wrote:

Hi all,

I was wondering about constraints in class declarations. Suppose we have something like this:

class Monad m => Store m where type Var m :: * -> *

new :: a -> m (Var m a) read :: Var m a -> m a write :: Var m a -> a -> m ()

[snip]

... it would be nice to be able to specify that all instances of our Store class have this property. Something like,

class (Monad m, Eq (Var m a)) => Store m where ...

But we can't write this! The `a` isn't in scope! What I really want to do is to be able to write class constraints like this,

Edward Kmett's constraints package has a Forall constraint that can be used for cases like this (but may require some fiddling when this constraint is used/required). -- Ivan Lazar Miljenovic Ivan.Miljenovic@gmail.com http://IvanMiljenovic.wordpress.com

You can use `Eq1` class (either from prelude-extras [1], or your own): {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE FlexibleContexts #-} import Data.IORef import Data.STRef import Control.Monad.ST -- | U for universal. class UEq1 f where (==#) :: f a -> f a -> Bool instance UEq1 IORef where (==#) = (==) instance UEq1 (STRef s) where (==#) = (==) class (Monad m, UEq1 (Var m)) => Store m where type Var m :: * -> * new :: a -> m (Var m a) read :: Var m a -> m a write :: Var m a -> a -> m () instance Store IO where type Var IO = IORef new = newIORef read = readIORef write = writeIORef instance Store (ST s) where type Var (ST s) = STRef s new = newSTRef read = readSTRef write = writeSTRef In same way you can lift any constraint to * -> * kind... - [1] https://hackage.haskell.org/package/prelude-extras-0.4/docs/Prelude-Extras.h... - [2] https://hackage.haskell.org/package/transformers-0.4.3.0/docs/Data-Functor-C... - Oleg

On 21 Jun 2015, at 08:55, Michael Walker wrote:

Hi all,

I was wondering about constraints in class declarations. Suppose we have something like this:

class Monad m => Store m where type Var m :: * -> *

new :: a -> m (Var m a) read :: Var m a -> m a write :: Var m a -> a -> m ()

Then some reasonable implementations would be IO and ST, using IORefs and STRefs,

instance Store IO where type Var IO = IORef

new = newIORef read = readIORef write = writeIORef

instance Store (ST s) where type Var (ST s) = STRef s

new = newSTRef read = readSTRef write = writeSTRef

Now, both IORefs and STRefs have equality, which doesn't require equality of the contained type,

instance Eq (IORef a) where ... instance Eq (STRef s a) where ...

This corresponds to pointer equality and, because reading the values is a monadic action, is as good an Eq instance as we can get. Given this, it would be nice to be able to specify that all instances of our Store class have this property. Something like,

class (Monad m, Eq (Var m a)) => Store m where ...

But we can't write this! The `a` isn't in scope! What I really want to do is to be able to write class constraints like this,

class (forall a. C (T a)) => D x where ...

Or why not get really crazy:

class (forall a. C a => D (T a)) => E x where ...

Is there some extension or combination of extensions that would make this work without completely sacrificing type safety? FlexibleContexts allows it (the simpler form, at least) for function constraints, but not for class constraints.

If not, has anyone thought about this sort of thing before?

-- Michael Walker (http://www.barrucadu.co.uk) _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe