4

DataKinds によってプロモートされたペアによって、2 つの型を取る型コンストラクタ f があるとします。

forall (f :: (ka, kb) -> *)

次に、数量詞のforwardような関数を実装できます。curryforall

forward :: forall (f :: (ka, kb) -> *).
           (forall (ab :: (ka, kb)).     f ab) ->
           (forall (a :: ka) (b :: kb).  f '(a, b))
forward x = x

ただし、逆関数には問題があります。

backward :: forall (f :: (*, *) -> *).
            (forall (a :: *) (b :: *). f '(a, b)) ->
            (forall (ab :: (*, *)). f ab)
backward x = x

GHC 8.0.1 では次のエラー メッセージが表示されます。

    • タイプ「ab」を「(a0, b0)」と一致させることができませんでした
      'ab' は、によってバインドされた固定型変数です。
        次の型シグネチャ:
          後方 :: forall (ab :: (*, *))。(forall a b. f '(a, b)) -> f ab
        6時116分
      予想されるタイプ: f ab
        実際の型: f '(a0, b0)
    • 式: x
      「後方」の式: 後方 x = x

概念的には、有効なプログラムのようです。この機能を実装する別の方法はありますか? それとも、これはGHCの既知の制限ですか?

4

1 に答える 1

6

pigworker と Daniel Wagner が指摘するように、問題abは「スタック型」である可能性があることです。型ファミリを使用してこれを回避できる場合があります (ピグワーカーの論文の 1 つで学んだように):

type family Fst (x :: (k1, k2)) :: k1 where
  Fst '(t1, t2) = t1

type family Snd (x :: (k1, k2)) :: k2 where
  Snd '(t1, t2) = t2

backward :: forall (f :: (*, *) -> *) (ab :: (*, *)) proxy .
            proxy ab ->
            (forall (a :: *) (b :: *). f '(a, b)) ->
            f '(Fst ab, Snd ab)
backward _ x = x

別のオプションとして、ラッパーを使用することがあります。

newtype Curry f x y = Curry (f '(x,y))

data Uncurry f xy where
  Uncurry :: f x y -> f '(x, y)
于 2016-09-06T18:46:24.537 に答える