私はIdrisには新しく、基本的な概念と構文をキャッチしようとしています。Idrisの 'half'関数型シグネチャ
無意味に聞こえるかもしれませんが、私はhalf自然を半分にする関数を定義しようとしています。
私のような何かを思い付くしたい：
half : (n : Nat) -> (k : Nat) -> (n = k + k) -> (k : Nat)
もちろん、それは働いていません。具体的には：
error: expected: dependent type signature
half : (n : Nat) -> (k : Nat) -> (n = k + k) -> (k : Nat)
可能ですか？
ありがとうございました。
half nは、Natであり、その数字はkであり、n = k + kであることを表しています。第2の座標のタイプ、n = k + kは、第1の座標の値に依存するので、それを行う方法、すなわち数kの依存対と証明n = k + k（それが依存対だsigma typeを使用することによるものですk）。
イドリス標準ライブラリは、あなたが（合計関数として）halfを実装することができなくなりますのでご注意、しかし
half : (n : Nat) -> (k ** n = k + k)
を書き込むことができるようにいくつかのシンタックスシュガーを含め、depedentペアについてDPair定義してありますので、例えばいい答えはありませんhalf 1。おそらくあなたが望むのは
half : (n : Nat) -> (k ** Either (n = k + k) (n = k + k + 1))
ですか？
kを2回使用しないでください。 半分：（n：Nat） - >（k：Nat） - >（n = k + k） - > Nat は正しいが、役に立たない。 あなたは必要と思います 半分：（n：Nat） - >多分（k ** n = k + k）
まあ、ありがとう、それは確かにtypechecks。とにかく、私が表現したいのは、「半分：（n：Nat） - > n-> Nat」のようなもので、その結果、「Nat」は実際には最初の「Nat」が半分になるという追加情報です。あなたのケースでは、関数の合計は（すなわち、入力だけを 'Nat'でも受け入れていますか）？あなたが 'Eirther'を使用しているという事実は私には分かりませんが、最初のバージョンでは、' n'が偶数である証拠を半分提供しなければなりません。 。あなたの助けをもう一度ありがとう。 –
「n」がすべて「2 * k」または「2 * k + 1」であるため、2番目のバージョンを合計することができます。もちろん、最初のものはできません。 '1 = 2 * k 'である。 – Cactus