5

非常に単純な考え方の背後にあるにもかかわらず、existential/rank-n 型を正しく使用するのは驚くほど難しいことが判明しました。

存在する型を型にラップするdata必要があるのはなぜですか?

次の簡単な例があります。

{-# LANGUAGE RankNTypes, ImpredicativeTypes, ExistentialQuantification #-}
module Main where

c :: Double
c = 3

-- Moving `forall` clause from here to the front of the type tuple does not help,
-- error is the same
lists :: [(Int, forall a. Show a => Int -> a)]
lists = [ (1, \x -> x)
        , (2, \x -> show x)
        , (3, \x -> c^x)
        ]

data HRF = forall a. Show a => HRF (Int -> a)

lists' :: [(Int, HRF)]
lists' = [ (1, HRF $ \x -> x)
         , (2, HRF $ \x -> show x)
         , (3, HRF $ \x -> c^x)
         ]

の定義をコメントアウトするとlists、コードは正常にコンパイルされます。コメントアウトしないと、次のエラーが発生します。

test.hs:8:21:
    Could not deduce (a ~ Int)
    from the context (Show a)
      bound by a type expected by the context: Show a => Int -> a
      at test.hs:8:11-22
      `a' is a rigid type variable bound by
          a type expected by the context: Show a => Int -> a at test.hs:8:11
    In the expression: x
    In the expression: \ x -> x
    In the expression: (1, \ x -> x)

test.hs:9:21:
    Could not deduce (a ~ [Char])
    from the context (Show a)
      bound by a type expected by the context: Show a => Int -> a
      at test.hs:9:11-27
      `a' is a rigid type variable bound by
          a type expected by the context: Show a => Int -> a at test.hs:9:11
    In the return type of a call of `show'
    In the expression: show x
    In the expression: \ x -> show x

test.hs:10:21:
    Could not deduce (a ~ Double)
    from the context (Show a)
      bound by a type expected by the context: Show a => Int -> a
      at test.hs:10:11-24
      `a' is a rigid type variable bound by
          a type expected by the context: Show a => Int -> a at test.hs:10:11
    In the first argument of `(^)', namely `c'
    In the expression: c ^ x
    In the expression: \ x -> c ^ x
Failed, modules loaded: none.

なぜこうなった？2 番目の例は最初の例と同等ではないでしょうか? これらの n ランク型の使用法の違いは何ですか? そのような種類のポリモーフィズムが必要な場合に、余分な ADT 定義を省略して単純な型のみを使用することはまったく可能ですか?

4

3 に答える 3

6

あなたの最初の試みは、存在型を使用していません。むしろあなたの

lists :: [(Int, forall a. Show a => Int -> a)]

2 番目のコンポーネントは、あなたが選択した表示可能なタイプだけでなく、私が選択した任意の表示可能なタイプの要素を提供できる必要があります。あなたが探しています

lists :: [(Int, exists a. Show a * (Int -> a))]  -- not real Haskell

しかし、それはあなたが言ったことではありません。データ型のパッケージ化方法により、カリー化によって回復できexistsますforall。あなたが持っている

HRF :: forall a. Show a => (Int -> a) -> HRF

つまり、値を作成するには、 type 、辞書 for 、関数 inHRFを含むトリプルを提供する必要があります。つまり、コンストラクターの型は、この非型を効果的にカリー化します。aShowaInt -> aHRF

HRF :: (exists a. Show a * (Int -> a)) -> HRF   -- not real Haskell

ランク n 型を使用して存在をチャーチ エンコードすることで、データ型の方法を回避できる場合があります。

type HRF = forall x. (forall a. Show a => (Int -> a) -> x) -> x

しかし、それはおそらくやり過ぎです。

于 2012-06-03T14:12:13.007 に答える
3

The examples are not equivalent. The first,

lists :: [(Int, forall a. Show a => Int -> a)]

says that each second component can produce any desired type, as long as it's an instance of Show from an Int.

The second example is modulo the type wrapper equivalent to

lists :: [(Int, exists a. Show a => Int -> a)]

つまり、各 2 番目のコンポーネントはに属する型を生成できますShowが、その関数が返す型はIntわかりません。

さらに、タプルに入れる関数は最初の契約を満たさない:

lists = [ (1, \x -> x)
        , (2, \x -> show x)
        , (3, \x -> c^x)
        ]

\x -> x入力として与えられた結果と同じ型を生成するので、ここではInt. showは常に を生成するStringため、1 つの固定型です。最後に、 has\x -> c^xと同じ型c、つまりを生成しますDouble。

于 2012-06-03T14:06:31.960 に答える
3

存在型の処理に関して考慮しなければならない問題が 2 つあります。

  • 「nになれるもの」を収納するなら、見せ方とshow一緒に見せられるものを収納しなければなりません。
  • 実際の変数は、1 つの型のみを持つことができます。

最初のポイントは、存在型ラッパーが必要な理由です。次のように書くと、

data Showable = Show a => Showable a

実際に何が起こるかというと、次のようなものが宣言されます。

data Showable a = Showable (instance of Show a) a

つまり、 のクラス インスタンスへの参照はShow a、値とともに格納されますa。これが起こらなければ、 をアンラップする関数を持つことはできません。Showableその関数は を表示する方法を知らないからaです。

let2 番目のポイントは、型の奇抜さがときどき得られる理由と、たとえばバインディングで存在型をバインドできない理由です。

また、コードの推論にも問題があります。任意の整数を指定すると、呼び出し元が選択forall a . Show a => (Int -> a)した任意の種類の表示可能な値を生成できる関数を取得するような関数がある場合。おそらく、関数が整数を取得すると、インスタンスが存在する型を返すことを意味します。exists a . Show a => (Int -> a)Show

于 2012-06-03T14:06:41.130 に答える