伊德里斯 - 感性步

證明考慮下面的函數伊德里斯 - 感性步

tryMove : (diskNumber : Nat) -> (from: Peg) -> (to: Peg)-> {default Oh prf: So (from /= to)} -> Disposition diskNumber -> Maybe (Disposition diskNumber) 
tryMove Z from to [] = Nothing 
tryMove (S k) from to (smallestDiskPosition :: restOfTheDisposition) = 
     map (smallestDiskPosition ::) (tryMove k from to restOfTheDisposition)

試圖編譯我收到以下錯誤：對tryMove的recurvise調用

When checking argument prf to Hanoi.tryMove: 
     Type mismatch between 
       So True (Type of Oh) 
     and 
       So (from /= to) (Expected type) 

     Specifically: 
       Type mismatch between 
         True 
       and 
         not (Hanoi.Peg implementation of Prelude.Interfaces.Eq, method == from to)

。如果我明確地傳遞{prf}在

tryMove : (diskNumber : Nat) -> (from: Peg) -> (to: Peg)-> {default Oh prf: So (from /= to)} -> Disposition diskNumber -> Maybe (Disposition diskNumber) 
tryMove Z from to [] = Nothing 
tryMove (S k) from to {prf} (smallestDiskPosition :: restOfTheDisposition) = 
     map (smallestDiskPosition ::) (tryMove k from to {prf} restOfTheDisposition)

它正確編譯。

爲什麼說Idris無法在歸納步驟中自動檢測證明，而能夠在正常調用函數的過程中做到這一點？

編輯：

這裏是一個完整的要點使用方法：https://gist.github.com/marcosh/d51479ea08e8522560713fd1e5ca9624

來源

2017-10-06 marcosh

您爲prf默認值（Oh），所以伊德里斯正在試圖通過進入Oh遞歸調用。 Oh有類型So True和伊德里斯預計prf是So (from /= to)型的，但是因爲你不破壞to和from，伊德里斯無法知道的from /= to的價值，這就是爲什麼你看到錯誤消息。

您可以將簽名更改爲包含{auto prf: So (from /= to)}或完全刪除prf參數，因爲您沒有真正使用它，只是將它傳遞給遞歸調用而不做任何修改。

來源

2017-10-06 10:33:14

感謝您的回答。我不明白一件事。 '因爲你沒有破壞，伊德里斯不知道從/ =到'的價值，你是什麼意思？ 'from'和'to'與最初的呼叫保持不變。如果他們一開始不同，爲什麼伊德里斯不能理解他們之後有所不同？此外，你是什麼意思破壞'到'和'從'？我怎麼能這樣做？ – marcosh

你傳遞了'So True'類型的'Oh'，其中Idris期望類型'So（from/= to）'的值，只要'from/= to'和'True'是，你就可以做到這一點在這種情況下，如果「from/= to」的計算結果爲「True」，則定義相等或更精確。但要評估'（/ =）'函數應用程序，你需要知道兩個參數究竟是什麼。伊德里斯不知道「從」和「到」是不相等的。模式匹配是您傳播信息的方式。所以，幫助Idris的一種非常難看的方法是在'from'和'to'上進行模式匹配 - 這會產生9個子句（其中3個是不可能的） –

伊德里斯 - 感性步

回答

相關問題