伊德里斯 - 感性步

证明考虑下面的函数伊德里斯 - 感性步

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个是不可能的） –

伊德里斯 - 感性步

回答

相关问题