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

Question

我正在为我的 pipes 库编写一个类型类，以定义类 Proxy 类型的抽象接口(interface)。类型类看起来像:

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 是所有 a'、a、b' 和 b 的 Monad .

但是，我不知道如何将其干净地编码为 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:我正在考虑的下一个解决方案只是在 ProxyC 类中复制 Monad 类的方法:

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'

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

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

编辑:您还可以将值(value)级别证明与新类型包装器结合起来，而无需到处打开 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
  ...

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