如何在Idris中編寫一個非常懶惰的版本？

Question

inf : Nat 
inf = S inf 

minimum' : Lazy Nat -> Lazy Nat -> Lazy Nat 
minimum' Z b = Z 
minimum' b Z = Z 
minimum' (S a) (S b) = S (minimum' a b) 

main : IO() 
main = do 
    print $ Force $ minimum' 2 inf 

我想寫最小的一個懶惰的版本，以便minimum 2 inf評估是2，但我的代碼似乎不起作用，它永遠不會停止，最小的「懶」的版本沒有任何不同，所以如何編寫一個真正懶惰的最低版本？

Answer 1

一個懶惰的納特不像一個合作的納特。 Nat有2個構造函數，Z和S. S需要被轉換成Lazy Nat。

你可以寫一個納特是coinductive像這樣：

codata CoNat : Type where 
    Z : CoNat 
    S : CoNat -> CoNat 

這應該是一樣的：

data CoNat : Type where 
    Z : CoNat 
    S : Inf CoNat -> CoNat 

確保您使用的「總」關鍵字，或使用「％默認總和「時使用codata。這使得Idris在正確的地方告訴你錯誤信息。

如果您同時擁有CoNat和Nat，則可以使用幾個不同的簽名來編寫minimum'。也許你想CoNat -> CoNat -> CoNat。我去了一個超級簡單的代替：

total 
inf : CoNat 
inf = S inf 

total 
minimum' : Nat -> CoNat -> Nat 
minimum' Z b = Z 
minimum' b Z = Z 
minimum' (S a) (S b) = S (minimum' a b) 

total 
main : IO() 
main = do 
    print $ minimum' 2 inf