问如何在Idris中编写一个真正懒惰的minimum版本？
EN

Stack Overflow用户

提问于 2017-10-10 11:14:13

回答 1查看 98关注 0票数 1

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，这样minimum 2 inf的计算结果是2，但是我的代码似乎不工作，它永远不会停止，“延迟”版本的minimum没有任何不同，那么如何编写一个真正的延迟版本的minimum呢？

idris

回答 1

Stack Overflow用户

发布于 2017-10-11 10:09:13

惰性Nat与同感Nat不同。Nat有两个构造函数，Z和S。S需要转换为惰性Nat。

您可以编写一个协同归纳的Nat，如下所示：

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

应与以下内容相同：

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

在使用codata时，请确保使用"total“关键字或使用"%default total”。这会使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

票数 4

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/46658084

复制

相似问题

问如何在Idris中编写一个真正懒惰的minimum版本？
EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问如何在Idris中编写一个真正懒惰的minimum版本？EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问如何在Idris中编写一个真正懒惰的minimum版本？
EN