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

...そして、これらのインスタンスが追加の制約を課すことmができるようにしたいMonadと思います。p a' a b' b mMonada'ab'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

そして、派手な中置演算子を使用して、モナドインスタンスを探す場所をコンパイラに伝えます

 ... \\ getProxyMonad'

実際、:-含意タイプはカテゴリ (オブジェクトが制約である場合) を形成し、このカテゴリには多くの優れた構造があります。つまり、証明を行うのに非常に優れています。

ps これらのスニペットはどれもテストされていません。

編集：値レベルの証明をnewtypeラッパーと組み合わせることもでき、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 に答える