6

我正在为我的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 ....

...并且我希望这些实例能够施加额外的约束，即 ifm是 a Monadthenp a' a b' b m是 aMonad对于所有a', a, b', and 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方法公开给实例编写器。

4

1 回答 1

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

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

于 2012-09-21T04:40:30.667 回答