[Haskell-cafe] "Universal" constraints?

[Chris Wong]

On Sun, Jun 21, 2015 at 5:55 PM, Michael Walker <mike at barrucadu.co.uk> 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?

One solution is to add an equality operator to the class itself:

    class Monad m => Store m where
        type Var m :: * -> *
        eqVar :: Var m a -> Var m a -> Bool
        -- ...

It may not be as satisfactory as subclassing Eq itself, but it should
work in principle.

Chris

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


-- 
https://lambda.xyz