如何在 Idris 中编写一个非常懒惰的 minimum 版本？答案

【问题标题】：How to write a really lazy version of minimum in Idris?如何在 Idris 中编写一个非常懒惰的 minimum 版本？
【发布时间】：2018-03-21 08:23:56
【问题描述】：

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，但我的代码似乎不起作用，它永远不会停止，最小的“惰性”版本没有任何不同，那么如何写一个真正懒惰的minimum呢？

【问题讨论】：

标签： idris

【解决方案1】：

懒惰的 Nat 与 Coinductive Nat 不同。 Nat 有 2 个构造函数，Z 和 S。需要将 S 转换为 Lazy Nat。

你可以写一个像这样的 Coinductive 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

【讨论】：

非常感谢，这解决了我的问题。但我发现在 Idris 中做一些懒惰的事情花费了我们很多时间，以至于人们很少会这样做，即使 Idris 提供了语法级别的概率。