12

次のような関数を頻繁に使用するコードがあります

foo :: (MyMonad m) => MyType a -> MyOtherType a -> ListT m a

これを短くするために、次のタイプエイリアスを作成しました。

type FooT m a = (MyMonad m) => ListT m a

GHCからRank2Types（またはRankNTypes）をオンにするように求められましたが、エイリアスを使用してコードを次のように短縮しても文句はありませんでした。

foo :: MyType a -> MyOtherType a -> FooT m a

対照的に、私が別のタイプエイリアスを書いたとき

type Bar a b = (Something a, SomethingElse b) => NotAsBar a b

負の位置で使用しました

bar :: Bar a b -> InsertTypeHere

GHCは私が間違っていると大声で叫んだ。

何が起こっているのかはわかっていると思いますが、あなたの説明からよりよく理解できると確信しているので、2つの質問があります。

  • タイプエイリアスは実際に何をしているのですか/それらは実際にはどういう意味ですか？
  • どちらの場合も簡潔にする方法はありますか？
4

2 に答える 2

12

型アノテーションには基本的に3つの部分があります。

  1. 変数宣言（これらは通常暗黙的です）
  2. 変数の制約
  3. タイプシグネチャヘッド

これらの3つの要素は基本的にスタックします。型変数は、制約または他の場所で使用する前に宣言する必要があり、クラス制約は型シグネチャヘッド内のすべての使用を対象としています。

foo変数が明示的に宣言されるように、型を書き直すことができます。

foo :: forall m a. (MyMonad m) => MyType a -> MyOtherType a -> ListT m a

変数宣言はforallキーワードによって導入され、に拡張され.ます。それらを明示的に導入しない場合、GHCは宣言のトップレベルでそれらを自動的にスコープします。次に制約があり=>ます。残りは型署名ヘッドです。

あなたのtype FooT定義でスプライスしようとするとどうなるか見てみましょう。

foo :: forall m a. MyType a -> MyOtherType a -> ( (MyMonad m) => ListT m a )

型変数mはのトップレベルで存在しfooますが、型エイリアスは最終値内でのみ制約を追加します！それを修正するには2つのアプローチがあります。次のいずれかを実行できます。

  • フォラルを最後まで動かすので、m後で存在します
  • またはクラス制約を一番上に移動します

制約を一番上に移動すると、次のようになります。

foo :: forall m a. MyMonad m => MyType a -> MyOtherType a -> ListT m a

GHCの有効化の提案はRankNTypes前者を実行し（ある種、私がまだ欠けているものがあります）、結果として次のようになります。

foo :: forall a. MyType a -> MyOtherType a -> ( forall m. (MyMonad m) => ListT m a )

これmは、他のどこにも表示されず、矢印の右側にあるため機能します。したがって、これら2つは本質的に同じことを意味します。

と比較するbar

bar :: (forall a b. (Something a, SomethingElse b) => NotAsBar a b) -> InsertTypeHere

タイプエイリアスが負の位置にある場合、上位のタイプは異なる意味を持ちます。ここで、の最初の引数は、適切な制約を使用して、およびでbar多形でなければなりません。これは、呼び出し元がこれらの型変数をインスタンス化する方法を選択する通常の意味とは異なります。そうではありませんabbar

おそらく、最善のアプローチは、ConstraintKinds拡張機能を有効にすることです。これにより、制約の型エイリアスを作成できます。

type BarConstraint a b = (Something a, SomethingElse b)

bar :: BarConstraint a b => NotAsBar a b -> InsertTypeHere

それはあなたが望んでいたものほど簡潔ではありませんが、毎回長い制約を書き出すよりもはるかに優れています。

ConstraintKinds別の方法として、タイプエイリアスをGADTに変更することもできますが、それによって、持ち込みたくない他のいくつかの結果が生じる可能性があります。より簡潔なコードを取得したいだけの場合は、これが最善のオプションだと思います。

于 2013-01-29T15:18:51.710 に答える
9

型クラスの制約は本質的に暗黙のパラメータと考えることができます-つまり、

Foo a => b

なので

FooDict a -> b

ここFooDict aで、はクラスで定義されたメソッドのディクショナリですFoo。たとえばEqDict、次のレコードになります。

data EqDict a = EqDict { equal :: a -> a -> Bool, notEqual :: a -> a -> Bool }

違いは、各タイプで各ディクショナリの値は1つだけであり（MPTCに対して適切に一般化）、GHCがその値を入力することです。

これを念頭に置いて、私たちはあなたの署名に戻ることができます。

type FooT m a = (MyMonad m) => ListT m a
foo :: MyType a -> MyOtherType a -> FooT m a

に拡大

foo :: MyType a -> MyOtherType a -> (MyMonad m => ListT m a)

辞書の解釈を使用する

foo :: MyType a -> MyOtherType a -> MyMonadDict m -> ListT m a

これは、引数を次のように並べ替えることと同等です。

foo :: MyMonadDict m -> MyType a -> MyOtherType a -> ListT m a

これは、辞書変換の逆と同等です。

foo :: (MyMonad m) => MyType a -> MyOtherType a -> ListT m a

それはあなたが探していたものです。

ただし、他の例では、そのようには機能しません。

type Bar a b = (Something a, SomethingElse b) => NotAsBar a b
bar :: Bar a b -> InsertTypeHere

に拡大

bar :: ((Something a, SomethingElse b) => NotAsBar a b) -> InsertTypeHere

これらの変数は、依然としてトップレベルで定量化されています（つまり、

bar :: forall a b. ((Something a, SomethingElse b) => NotAsBar a b) -> InsertTypeHere

）、あなたはbarの署名でそれらを明示的に言及したので、しかし私たちが辞書変換を行うとき

bar :: (SomethingDict a -> SomethingElseDict b -> NotAsBar a b) -> InsertTypeHere

これは同等ではないことがわかります

bar :: SomethingDict a -> SomethingElseDict b -> NotAsBar a b -> InsertTypeHere

それはあなたが望むものを生み出すでしょう。

型クラス制約が定量化のポイントとは異なる場所で使用される現実的な例を思い付くのはかなり難しいです-私は実際にそれを見たことがありません-それで、それが起こっていることを示すためだけに非現実的な例があります：

sillyEq :: forall a. ((Eq a => Bool) -> Bool) -> a -> a -> Bool
sillyEq f x y = f (x == y)

==引数を渡していないときに使用しようとするとどうなるかとは対照的fです。

sillyEq' :: forall a. ((Eq a => Bool) -> Bool) -> a -> a -> Bool
sillyEq' f x y = f (x == y) || x == y

エラーのインスタンスはありませんEq a。

(x == y)insillyEqはからそのdictEqを取得しfます; その辞書形式は次のとおりです。

sillyEq :: forall a. ((EqDict a -> Bool) -> Bool) -> a -> a -> Bool
sillyEq f x y = f (\eqdict -> equal eqdict x y)

少し後退すると、ここであなたが恐れている方法は苦痛になると思います-コンテキストを定量化するために何かを使用したいだけだと思います。コンテキストは「使用される関数シグネチャ」として定義されます。 "。その概念には単純なセマンティクスはありません。セットの関数と考えることができるはずですBar。引数として2つのセットを取り、別のセットを返します。あなたが達成しようとしている用途のためにそのような機能があるとは思わない。

コンテキストを短縮する限り、ConstraintKinds制約の同義語を作成できる拡張機能を利用できる可能性があるため、少なくとも次のように言うことができます。

type Bars a = (Something a, SomethingElse a)

取得するため

bar :: Bars a => Bar a b -> InsertTypeHere

しかし、あなたが望むことはまだ可能かもしれません-あなたの名前は私が言うのに十分な説明ではありません。型変数を抽象化する2つの方法である、存在記号と全称記号を調べることをお勧めします。

話の教訓：これらの引数がコンパイラーによって自動的に入力されることを除いて、それ=>は同じことを覚えておいてください。そして、明確に定義された数学的意味で型を定義しようとしていることを確認してください。->

于 2013-01-29T22:19:37.790 に答える