0

関連付けられた型のシノニムを使用して部分的に指定したいネストされた型があります。以下は、問題を示す非常に縮小されたコードです。

{-# LANGUAGE TypeFamilies,
FlexibleInstances,
FlexibleContexts,
MultiParamTypeClasses #-}

f :: Int -> Int
f x = x+1

data X t i
newtype Z i = Z i deriving (Eq,Show)
newtype Y q = Y (T q)

class Qux m r where
    g :: (T m) -> r

class (Integral (T a)) => Foo a where
    type T a
    -- ... functions

instance (Integral i) => Foo (X (Z i) i) where
    type T (X (Z i) i) = i

instance (Foo q) => Num (Y q) -- where ...

instance (Foo q, Foo (X m' Int)) => Qux (X m' Int) (Y q) where
    g x =  fromIntegral $ f $ x

これは (UndecidableInstances を使用しても) コンパイラ エラーにつながります。

Could not deduce (T (X m' Int) ~ Int)

この制約を Qux のインスタンスに追加すると、コンパイラが満足することはわかっています。ただし、私のプログラムでは (T (X arg1 arg2)) = arg2 であることを知っているので、この制約を記述しなくても済む方法を見つけようとしています。

私の質問は、Haskell に、X の 2 番目のパラメーターとして 'Int' を記述したときに、これがシノニム T (X a' Int) と (同じように) 同じであることを認識させることはできますか? インスタンスがどのように見えるかについて「特別な」知識を使用していることはわかっていますが、これをコンパイラに伝える方法があるはずです。

ありがとう

4

1 に答える 1

1

私はまだ質問を理解しているかどうかわからないので、あなたが書いたコードについて議論します。おそらく、私のとりとめのない部分は、役に立つ方向にあなたを指し示すか、私が答えることができるいくつかの鋭い質問を引き起こすでしょう. つまり、警告！とりとめのない応答先！

まず、Barクラスについて話しましょう。

-- class (i ~ S b) => Bar b i where
--     type S b
--     ...

制約がわかっているので、引数をi ~ S b削除するiこともできます。残りの議論ではそうします。

class Bar b where type S b
-- or, if the class is empty, just
-- type family S b
-- with no class declaration at all

この新しいクラスのインスタンスは次のようになります。

instance Bar (Z  i) where type S (Z  i) = i
instance Bar (Z' i) where type S (Z' i) = i

これが任意の型コンストラクターに当てはまる場合は、代わりにこれを 1 つのインスタンスとして記述することを検討できます。

-- instance Bar (f i) where type S (f i) = i

さて、Fooクラスについて話しましょう。上記と一致するように変更するには、次のように記述します

class Bar (T a) => Foo a where type T a

2 つのインスタンスを宣言しました。

-- instance (Bar (Z i) i) => Foo (X (Z i) i) where
--     type T (X (Z i) i) = Z i
--
-- instance (Bar (Z' i) i) => Foo (X' (Z' i) i) where
--     type T (X (Z' i) i) = Z' i

前と同じように2 番目の引数を削除できますBarが、別のこともできます。インスタンスがあることがわかっているのでBar (Z i)(上記で宣言しました!)、インスタンスの制約を取り除くことができます。

instance Foo (X (Z  i) i) where type T (X (Z  i) i) = Z  i
instance Foo (X (Z' i) i) where type T (X (Z' i) i) = Z' i

i引数を保持するかどうかXは、何Xを表現するかによって異なります。これまでのところ、クラス宣言やデータ型のセマンティクスは変更していません。宣言とインスタンス化の方法のみを変更しています。変更Xは、同じプロパティを持たない場合があります。の定義を見ずに言うのは難しいですX。データ宣言と十分な数の拡張により、上記のプレリュードがコンパイルされます。

さて、あなたの苦情：

  • あなたは、以下がコンパイルされないと言います:

    class Qux a
instance Foo (X  a' Int) => Qux (X  a' Int)
instance Foo (X' a' Int) => Qux (X' a' Int)

    しかし、 を使用するとUndecidableInstances、ここでコンパイルされます。そして、それが必要であることは理にかなっていますUndecidableInstances:誰かが後でやって来て、次のようなインスタンスを宣言するのを止めるものは何もありません

    instance Qux (X Y Int) => Foo (X Y Int)

Then, checking whether `Qux (X Y Int)` had an instance would require checking whether `Foo (X Y Int)` had an instance and vice versa. Loop.

  • S (T (X a'))) ~ Intあなたは、「私のプログラムでは、これらは常に単なるシノニムであることを知っていても、インスタンスの制約も必要です。」と言います。最初の「それ」が何なのかわかりません -- このエラーを再現できません -- ですから、うまく答えられません。また、私が前に不平を言ったように、この制約は ill-kinded:X :: (* -> *) -> * -> *であり、したがってX a' :: * -> *、Tkind の引数を期待します*。だから私はあなたがS (T (X a' Int)) ~ Int代わりに意味したと仮定するつもりです.

    これらの不満にもかかわらず、S (T (X a' Int)) ~ Intこれまでの仮定から証明できない理由を尋ねることができます。これまでのところ、パターンとFooに適合する型のインスタンスのみを宣言しました。したがって、型関数は、その引数の型がこれらのパターンのいずれかに適合する場合にのみ削減できます。タイプは、これらのパターンのいずれにも完全には適合しません。それを適切なパターンに詰め込むことができます:代わりに (たとえば) を減らすことを試みることができます。それから、したがってが見つかります。X (Z i) iX (Z' i) iTX a' IntX (Z Int) IntT (X (Z Int) Int) ~ Z IntS (T (X (Z Int) Int) ~ S (Z Int) ~ Int

    これは、型レベルの縮小を修正する方法に答えますが、構築されていないコードを修正する方法については説明していません。そのためには、型チェッカーが からS (T (X a' Int))への強制変換を必要とする理由を見つけ、 、または上記の一般化されたインスタンスを使用して、 のIntようなより具体的な (そして満足できる) 強制変換を行うことができるかどうかを確認する必要があります。エラーを再現するのに十分なコードがなければ、私たちは確かにそれを手助けすることはできません.S (T (X (Z Int) Int)) ~ IntBarS (T (X (f Int) Int)) ~ Int

  • 「X の 2 番目のパラメーターとして 'Int' を記述したときに、これが同義語 S (T (X a' Int)) と (まったく同じ) 同じものであることを Haskell に認識させることはできますか?」この質問がまったくわかりません。どういうわけか証明可能な平等を持ちたいX a Int ~ S (T (X a' Int))ですか？それが、あなたの質問を文字通り読んで得た解釈です。

    文脈上、証明可能な平等を得ることができるかどうかを尋ねたかったのではないかと思いますb ~ S (T (X a b))。その場合、答えは「間違いなく！」です。上記の事実を利用しb ~ S (Z b)て、この方程式をより強いものに減らしZ b ~ T (X a b)ます。Foo次に、上記のインスタンスを、この宣言を行うものに置き換えるだけで済みます。

    instance Foo (X a b) where T (X a b) = Z b

    代わりに、他の合理的な方程式を仮定することもできT (X a b) ~ aます。次に、それを証明するS (T (X a b)) ~ b必要があることを証明するにはS a ~ b( を減らすことによって)、この別の代替インスタンスTを書くことができます。Foo

    instance (Bar a, S a ~ b) => Foo (X a b) where T (X a b) = a
于 2012-07-16T16:15:03.333 に答える