约束类型类或实例的派生变量

Question

我正在为我的pipes库编写一个类型类来定义Proxy类似于抽象的接口.类型类看起来像:

class ProxyC p where
    idT   :: (Monad m) => b' -> p a' a b' b m r
    (<-<) :: (Monad m)
          => (c' -> p b' b c' c m r)
          -> (b' -> p a' a b' b m r)
          -> (c' -> p a' a c' c m r)
    ... -- other methods

我也在编写以下形式的扩展名Proxy:

instance (ProxyC p) => ProxyC (SomeExtension p) where ....

......我想这些情况,以能够施加额外的约束,如果m是Monad则p a' a b' b m是Monad为所有a',a,b',和b.

但是,我不知道如何干净地将其编码为ProxyC类或实例的约束.我目前所知道的唯一解决方案是在类的方法签名中对其进行编码:

    (<-<) :: (Monad m, Monad (p b' b c' c m), Monad (p a' a b' b m))
          => (c' -> p b' b c' c m r)
          -> (b' -> p a' a b' b m r)
          -> (c' -> p a' a c' c m r)

...但我希望有一个更简单,更优雅的解决方案.

编辑:即使不是最后的解决方案有效,因为编译器不推断(Monad (SomeExtension p a' a b' b m))隐含(Monad (p a' a b' b m))的变数,给下面的实例,即使一个特定的选择:

instance (Monad (p a b m)) => Monad (SomeExtension p a b m) where ...

编辑#2:我正在考虑的下一个解决方案是复制Monad类中ProxyC类的方法:

class ProxyC p where
    return' :: (Monad m) => r -> p a' a b' b m r
    (!>=) :: (Monad m) => ...

...然后用每个ProxyC实例实例化它们.这似乎可以用于我的目的,因为这些Monad方法只需要在内部用于扩展写入,并且原始类型仍然具有适合Monad下游用户的实例.所有这一切只是将Monad方法暴露给实例编写器.

Answer 1

一个相当简单的方法是使用 GADT 将证明移至值级别

data IsMonad m where
  IsMonad :: Monad m => IsMonad m 

class ProxyC p where
  getProxyMonad :: Monad m => IsMonad (p a' a b' b m)

您需要在需要的地方显式打开字典

--help avoid type signatures
monadOf :: IsMonad m -> m a -> IsMonad m
monadOf = const

--later on
case getProxyMonad `monadOf` ... of
  IsMonad -> ...

使用 GADT 来通过命题证明的策略确实非常通用。如果您可以使用约束类型，而不仅仅是 GADT，则可以使用 Edward Kmett 的Data.Constraint包

class ProxyC p where
  getProxyMonad :: Monad m => Dict (Monad (p a' a b' b m))

这可以让你定义

getProxyMonad' :: ProxyC p => (Monad m) :- (Monad (p a' a b' b m))
getProxyMonad' = Sub getProxyMonad

然后使用一个奇特的中缀运算符告诉编译器在哪里寻找 monad 实例

 ... \\ getProxyMonad'

事实上，:-蕴涵类型形成了一个类别（其中对象是约束），并且这个类别有很多很好的结构，也就是说用它来做证明是非常好的。

ps 这些片段都没有经过测试。

编辑：您还可以将价值级别证明与新类型包装器结合起来，而无需到处打开 GADT

newtype WrapP p a' a b' b m r = WrapP {unWrapP :: p a' a b' b m r}

instance ProxyC p => Monad (WrapP p) where
  return = case getProxyMonad of
                Dict -> WrapP . return
  (>>=) = case getProxyMonad of
               Dict -> \m f -> WrapP $ (unWrapP m) >>= (unWrapP . f)

instance ProxyC p => ProxyC (WrapP p) where
  ...

我怀疑，但显然没有测试过，这种实现也会相对有效。