Idris的'half'功能類型簽名

我是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) 

這可能嗎？

謝謝。

來源

2016-11-30 Cristiano Paris

你想要什麼來表達half n一些Nat烏拉爾號k這樣n = k + k成立。的方式做到這一點是通過使用sigma type，即依賴對一號碼k和證明n = k + k（這是一個依賴對因爲類型的秒座標的，n = k + k依賴於值的第一座標， k）。

的伊德里斯標準庫depedent對定義DPair，包括一些語法糖，讓您寫

half : (n : Nat) -> (k ** n = k + k)

但是，請注意，您將無法實現half（作爲一個整體功能），因爲有沒有好的答案例如half 1。也許你想要的是

half : (n : Nat) -> (k ** Either (n = k + k) (n = k + k + 1))

？

來源

2016-12-01 02:00:46 Cactus

嗯，謝謝，它確實是typechecks。無論如何，我想要表達的是類似「half：（n：Nat） - > Even n - > Nat」的信息，因爲生成的「Nat」實際上是第一個「Nat」的一半。在你的情況下，函數總數是多少（即只接受輸入甚至是'Nat'）？你使用Eirther這個事實讓我覺得它不是，而在第一個版本中，我們必須提供一半帶有證明的'n'，即偶數，這就省去了1，3和所有其他的奇數。再次感謝你的幫助。 –

第二個版本可以做成總數，因爲每個'n'都是'2 * k'或'2 * k + 1'。當然，第一個不能，因爲沒有'k'，例如， '1 = 2 * k'。 – Cactus

您不應該使用k兩次。（n：Nat） - >（k：Nat） - >（n = k + k） - > Nat 是正確的，但是沒用。我認爲你需要一半：（n：Nat） - >也許（k ** n = k + k）

來源

2017-11-02 10:11:58

Idris的'half'功能類型簽名

回答

相關問題