どのようにこの奇妙なタイプの署名FOO ::歌うを読み取るために、N - >（KnownNat N => R） - > R

Question

シングルトンでwithKnownNatには、次の奇妙な型シグネチャ持つ機能をパッケージ化：

withKnownNat :: Sing n -> (KnownNat n => r) -> rを。

コンテキストは、::（hasType）シンボルの後ではなく、2番目の関数引数：-> (KnownNat n => r) ->の後にあります。

この署名を読むにはどうすればよいですか？それはどういう意味ですか？それはどこに文書化されていますか？

Answer 1

これら2つのシグネチャの違い：

withKnownNat :: Sing n -> (KnownNat n => r) -> r 
withKnownNat' :: KnownNat n => Sing n -> r -> r 

が制約KnownNat nが保持しているという証拠を提供するために必要とされる人です。

フロントアップ制約を持つ仮説バージョンは（「::（hasType）記号の後」）関数を呼び出すためにKnownNat nを証明することができるようにwithKnownNat'の発信者を必要とします。そのタイプシグネチャは、「KnownNat nを証明できれば、私にSing nとrの両方を渡したら、私はrを返すでしょう。

KnownNat nという制約とSing nという引数を無視して、それだけをrに戻すことで実装できるため、特に便利なわけではありません。そしてrが何であるか分からずに返すことが他にはあまりできませんでした。r;それはnでいくつかの操作を行う可能性があり、いくつかの条件の下でエラーを発生させるか、内部的に安全でない機能を使って厄介なハッキングを行うことがあります。

実際のバージョンでは、KnownNat n制約の下にある関数はすべてwithKnownNatではなく、その引数の1つに制約があります。つまり、withKnownNatの発信者はがKnownNat nであることを証明できなければなりません。代わりに、呼び出し側はがの証明がKnownNat nであることを必要とする引数を渡すことができます。ファンクションへの引数は、タイプKnownNat n => rは、「 の値で、の場合、KnownNat nが成立する」という値として読み取ることができます。あなたが私にSing nと（2）の値を持っていると仮定すると、KnownNat nの値を持っているなら、私はあなたにタイプrの値を与えます。 。

これは、タイプからちょうどもっと有用であることがわかります。 rのポリモーフィックなので、withKnownNatのrという唯一の方法は、私たちが与えたKnownNat n => rからです。 KnownNat nと表示される場合は、実際にKnownNat n => rの値をrの値として使用してに戻すことができます。したがって、基本的にwithKnownNatのこのタイプは、Sing nがあるときはいつも、同じにはKnownNat nが必要なものを使うことができるという約束をします。 withKnownNatは、一方を他方に変換するために呼び出す必要があります。

---

それだけでなく、関数の戻り値と同じことを意味しますが、それは制約を必要とする戻り値を得ることが、全体の機能の場合とまったく同じものにうまくいくことが判明GHCは常にarg -> (constraints => result)のような型をちょうどconstraints => args -> resultに変換します。

Answer 2

KnownNat nは、基本的に「n」というnに関連付けられた「特定の番号があります」という意味にすぎません。したがって、何かに制約KnownNat n => ...がある場合は、1つの特定の数値を渡すのと同じです。

withKnownNat' :: Sing n -> (Integer -> r) -> r 

今度は何もなく、本質的Singを持っていることを除いてthe actual

natVal :: KnownNat n => proxy n -> Integer 

の特定のインスタンスである

natVal :: Sing n -> Integer 

を書くCPS方法...ではないことtypeclass constraint baked-inです。