14

Haskell では、型の制約を論理 AND と組み合わせることができます。

次のことを考慮してください

type And (a :: Constraint) b = (a, b)

またはより複雑に

class (a, b) => And a b
instance (a, b) => And a b

Haskell で 2 つの制約を論理的に結合する方法を知りたいです。

私の最も近い試みはこれですが、うまくいきません。この試みでは、型制約をタグで具体化し、暗黙的なパラメーターでそれらを非具体化します。

data ROr a b where
 L :: a => ROr a b
 R :: b => ROr a b

type Or a b = (?choose :: ROr a b)

y :: Or (a ~ Integer) (Bool ~ Integer) => a
y = case ?choose of
 L -> 4

x :: Integer
x = let ?choose = L in y

ほとんど動作しますが、ユーザーは最終部分を適用する必要があり、コンパイラーがそれを行う必要があります。同様に、このケースでは、両方の制約が満たされている場合、3 番目の選択肢を選択できません。

論理的に、または 2 つの制約をまとめるにはどうすればよいですか?

4

2 に答える 2

14

ROr a b自動的に;を選択する方法はないと思います。bたとえば、満足されたが、後で満足された場合、それはオープンワールドの仮定に違反しaます。競合解決ルールは、必然的にインスタンスの追加によって既存のコードの動作を変更します。

つまり、満たされているが満たされていないR場合の選択は、インスタンスが満たされていないことを決定することを含むため、オープンワールドの仮定を破ります。1「両方とも満足する」コンストラクターを追加した場合でも、それを使用して、インスタンスが存在しないかどうかを判断できます (またはを取得するかどうかを確認することによって)。baLR

したがって、そのようなor制約が可能であるとは思いません。どのインスタンスを取得するかを観察できる場合は、インスタンスを追加することで動作が変化するプログラムを作成できます。取得するインスタンスを観察できない場合は、まったく役に立ちません。

1これと失敗する可能性がある通常のインスタンス解決との違いは、通常、コンパイラーは制約が満たされていると判断できないことです。ここでは、制約を満たすことができないと判断するようコンパイラーに求めています。微妙だが重要な違い。

于 2012-04-21T01:17:06.930 に答える
0

カフェに関するあなたの質問に答えるためにここに来ました。ここのqが同じかどうかはわかりませんが、とにかく...

3 つのパラメーターを持つ型クラス。

   class Foo a b c | a b -> c where
     foo :: a -> b -> c
   instance Foo A R A where ...
   instance Foo R A A where ...

関数の依存関係に加えて、パラメータ a と b の少なくとも 1 つが c であることを表現したいと思います。

import Data.Type.Equality
import Data.Type.Bool

class ( ((a == c) || (b == c)) ~ True)
      => Foo a b c  | a b -> c  where ...

多数の拡張機能をオンにする必要があります。特にUndecidableSuperClasses、クラス制約内の型ファミリの呼び出しは、GHC が見る限り不透明だからです。

あなたの質問はこちら

論理的に、または 2 つの制約をまとめるにはどうすればよいですか?

はるかにトリッキーです。型等価アプローチで==は、Closed Type Family を使用します。したがって、 kind を返す Closed Type Family を作成できますがConstraint、一般的な解決策があるとは思えません。Fooクラスの場合:

type family AorBeqC a b c :: Constraint where
  AorBeqC a b a = ()
  AorBeqC a b c = (b ~ c)

class AorBeqC a b c => Foo a b c  | a b -> c  where ...

貧弱で非対称なタイプの改善動作をする可能性があります。GHC がa, cそれらが離れていることを確認できる場合、2 番目の方程式に進み、(b ~ c)どちらかを改善するために使用します。それらが離れていることや、それらが統合可能であることを確認できない場合、スタックします。

一般に、@ehird が指摘するように、制約が満足できないかどうかをテストすることはできません。型の等価性は特別です。

于 2018-07-23T22:58:40.957 に答える