6

次の例は、私の実際の問題を煮詰めたものです。DataKinds の制約付き存在型から情報を取得する とどこか似ているようですが、求めていた答えを得ることができませんでした。

Kタイプとを持つ有限の昇格された DataKindAと、種類 * のタイプを持つ項を生成するBための poly-kindedProxyデータ型があるとします。

{-# LANGUAGE DataKinds, PolyKinds, GADTs, FlexibleInstances, FlexibleContexts #-}

data K = A | B

data Proxy :: k -> * where Proxy :: Proxy k

ここで、 が kind のShowすべてのタイプの -instancesを書きたいと思います。これは正確に 2 つです。Proxy aaK

instance Show (Proxy A) where show Proxy = "A"
instance Show (Proxy B) where show Proxy = "B"

しかし、Show-instance を使用するには、種類が次のように制限されている場合でも、明示的にコンテキストを提供する必要がありますK。

test :: Show (Proxy a) => Proxy (a :: K) -> String
test p = show p

私の目標は、型クラスの制約を取り除くことです。これは重要ではないように思えるかもしれませんが、私の実際のアプリケーションでは、これは大きな意味を持ちます。

次のように、単一のより一般的なインスタンスを定義することもできますShow。

instance Show (Proxy (a :: K)) where show p = "?"

Aこれにより、実際には制約を削除できますが、新しい問題は と の 2 つのタイプを区別することBです。

それで、私のケーキを食べて、それも食べる方法はありますか? つまり、型で型クラス制約を提供する必要はなくtest(kind アノテーションは問題ありません)、2 つの異なるshow実装を保持している (たとえば、何らかの方法で型を区別することによって) ということですか?

実際には、型情報だけを持っているコンテキストで、それぞれの型 ( A、B) を特定の値 (ここでは"A"、 ) に単純に関連付けることができれば、型クラス全体を削除しても問題ありません。"B"しかし、これを行う方法がわかりません。

提供された洞察に非常に感謝します。

4

3 に答える 3

6

いいえ、これは不可能です。「型情報だけ」を持っているコンテキストでは、実行時に実際には情報がありません。タイプ情報は消去されます。そのため、原則として問題の型が与えられた場合、いつでも辞書を作成できることを示すことができる閉じた種類の場合でも、クラス制約が必要です。クラス制約は、GHC が型を認識しているコンパイル時に、渡す適切なインスタンスを選択できることを保証します。実行時に、それがどのタイプであるかという情報は失われ、同じことを行う機会はありません。「フリーサイズ」のインスタンスを書くことは実際にうまくいきます。

全体像はわかりませんが、クラス辞書または文字列自体を、渡している値と明示的にバンドルすることで、これを回避できる可能性があります...

于 2015-09-05T00:23:43.613 に答える
2

知っています：

  1. a親切ですK
  2. kind の唯一の型KはAandですB
  3. Show (Proxy A)ホールド
  4. Show (Proxy B)ホールド

であることを証明するには十分Show (Proxy a)です。しかし、型クラスは、型で使用するために真であることを証明する必要があるという単なる命題ではなく、実装も提供します。実際に使用するには、 の実装がexistsshow (x :: Proxy a)であることを証明するだけでなく、それがどれであるかを実際に知る必要があります。Show (Proxy a)

Haskell 型の変数 (制約なし) はパラメトリックです。 で完全にポリモーフィックにする方法はなく、 と で異なる動作を提供するためにa検査することもできます。必要な「異なる動作」は、タイプごとに1つあることがわかっている場合、タイプごとに異なるインスタンスを選択するだけなので、実際にパラメトリックでなくても可能な限り「パラメトリックに近い」ものです。しかし、それはまだ意味の契約を破るものです.aABtest :: forall (a :: K). Proxy a -> String

型クラスの制約により、型から実装への型クラスのマッピングを使用して、呼び出された型に基づいてコードの動作を切り替えることができる限り、制約された型変数でコードをノンパラメトリックにすることができます。だからtest :: forall (a :: K). Show (Proxy a) => Proxy a -> Stringうまくいく。(実際の実装に関しては、型を選択できる同じ最終呼び出し元が、使用する関数から生成されたコードaのインスタンスも提供します)。Show (Proxy a)

あなたのinstance Show (Proxy (a :: K))アイデアを使うことができます。すべての. _ _a :: K _ しかし、インスタンス自体にも同じ問題が発生します。インスタンスでの の実装はでパラメトリックであるため、タイプに基づいて異なる文字列を返すためにそれを検査することはできません。show (x :: Proxy a)a :: Kshowa

Kish基本的に実行時に型を検査できるようにするために、制約された型変数の非パラメトリック性を利用するdfeuer の答えのようなものを使用できます。Kish a制約を満たすために渡されるインスタンス ディクショナリは、基本的に、変数に対して選択された型のランタイム レコードですa(迂回的な方法で)。このアイデアをさらに推し進めると、Typeable. しかし、.NET でコードをノンパラメトリックにするためには、なんらかの制約が必要ですa。

Aまたはの選択の実行時表現である型を明示的に使用することもできます(実行時に空の値であり、選択のコンパイル時表現のみを提供する とはB対照的に)、次のようなものです。Proxy

{-# LANGUAGE DataKinds, GADTs, KindSignatures, StandaloneDeriving #-}

data K = A | B

data KProxy (a :: K)
  where KA :: KProxy A
        KB :: KProxy B

deriving instance Show (KProxy a)

test :: KProxy a -> String
test = show

(ここでは、実装するだけでなくShow (Kproxy a)、実際に派生させることもできますが、スタンドアロンの派生が必要であることに注意してください)

これは GADTKProxyを使用testして でノンパラメトリックになることを可能にし、本質的に dfeuer の回答aの制約と同じ仕事をしますが、型シグネチャに余分な制約を追加する必要を回避します。Kishこの投稿の以前のバージョンで、 は でtest「ちょうど」パラメトリックのままでこれを行うことができると述べましたがa、これは誤りでした。

もちろん、プロキシを渡すには、実際にKAorを書く必要がありKBます。実際にタイプを選択するために記述しなければならなかった場合、それは面倒ではありませんProxy :: Proxy A(プロキシの場合はよくありますが、通常はあいまいなタイプを修正するためにのみ使用するためです)。しかし、呼び出しの残りの部分と矛盾している場合、コンパイラはあなたをキャッチしますが、シンボルを 1 つだけ記述Proxyして、コンパイラに正しい意味を推測させることはできません。型クラスでこれに対処できます。

class KProxyable (a :: K)
  where kproxy :: KProxy a

instance KProxyable A
  where kproxy = KA

instance KProxyable B
  where kproxy = KB

次に、の代わりに を使用し、コンパイラに裸の の型を推測させる代わりにKAを使用できます。愚かな例の時間:Proxy :: Proxy AkproxyProxy

foo :: KProxy a -> KProxy a -> String
foo kx ky = show kx ++ " " ++ show ky

GHCI:

λ foo KA kproxy
"KA KA"

KProxyable実際にはどこにも制約を設ける必要はないことに注意してください。型が分かるkproxyところで使います。ただし、これはまだ「上から入る」必要があります（制約を満たすインスタンス辞書とまったく同じです）。型の関数パラメトリックを独自に関連させる方法はありません。Show (Proxy a)a :: KKProxy a

これを機能させるのはコンストラクターと型の間の対応であるため、 empty-at-runtime でできるように、このスタイルで汎用プロキシを作成できるとは思いませんProxy。ただし、TemplateHaskell は確かにそのようなプロキシ タイプを生成できます。ここではシングルトンの概念が一般的な考え方だと思うので、 https://hackage.haskell.org/package/singletonsでおそらく必要なものが提供されますが、実際にそのパッケージを使用する方法についてはあまり詳しくありません。

于 2015-09-07T03:07:03.617 に答える