标签: codata

有filter : (a -> Bool) -> List a -> List aList,但是没有filter : (a -> Bool) -> Stream a -> Stream aStream,为什么？

是否有一些替代方案可以完成类似的工作？

有一些解释在这里.直观地,我理解有限数据结构与流等无限数据结构的区别.然而,看到有关差异,特征,类型的其他解释是有趣的.

在阅读关于溪流的时候,我偶然发现了一些术语.

我发现Lazy并Inf非常接近:

Lazy和Inf密切相关(事实上,底层实现使用相同的类型).实践中唯一的区别在于整体检查,其中Lazy被删除(即通常检查术语是否终止,忽略懒惰注释),Inf使用生产力检查器,其中任何延迟的使用必须是构造函数保护.

如所描述的以上,底层实现Lazy和Inf是同一个,唯一的区别是大约整体检查.

我认为总是使用Inf似乎更自然,这更接近我们在Haskell中使用的懒惰,并想知道我们必须使用的生产场景是什么Lazy- 它总是进行深度整体检查？

这是一个核心递归算法，因为在每次迭代中，它调用自己的数据大于之前的数据：

iterate f x =  x : iterate f (f x)

它类似于尾递归累加器风格，但它的累加器是隐式的，而不是作为参数传递。如果不是因为懒惰，那将是无限的。那么 codata 只是 WHNF 中值构造函数的结果，有点像(a, thunk)？或者 codata 是范畴论中的一个数学术语，它在编程领域没有有用的表示？

后续问题：值递归只是核心递归的同义词吗？

我正在尝试CoNat从Jesper Cockx 和 Andreas Abel 的这篇论文中得到的定义：

open import Data.Bool
open import Relation.Binary.PropositionalEquality

record CoNat : Set where
  coinductive
  field iszero : Bool
        pred : .(iszero ? false) -> CoNat

open CoNat public

我定义zero和plus：

zero : CoNat
iszero zero = true
pred zero ()

plus : CoNat -> CoNat -> CoNat
iszero (plus m n)                                  = iszero m ? iszero n
pred (plus m n) _ with iszero m | inspect iszero m …

想象一下以下函数在Clojure中给出一个无限懒惰的fibonacci序列:

(def fib-seq
  (concat
   [0 1]
   ((fn rfib [a b]
        (lazy-cons (+ a b) (rfib b (+ a b)))) 0 1)))

user> (take 20 fib-seq)
(0 1 1 2 3 5 8 13 21 34 55 89 144 233 377 610 987 1597 2584 4181)

假设

1. 我们将codata的简洁定义视为"Codata是可能无限的价值所居住的类型".
2. 这个Clojure示例不使用静态类型系统(来自core.typed),所以对codata的任何描述都是'工作定义'

我的问题是 - 上面函数的哪个部分是'codata'.这是匿名函数吗？它是懒惰的序列吗？

换句话说：如果我们分别删除归纳和共归纳数据类型使用的终止检查和防护条件，归纳/共归纳和修复/共归纳之间是否不再有根本区别？

我所说的“根本差异”是指 Coq\xe2\x80\x93 核心演算的差异，而不是语法和证明搜索等方面的差异。

这似乎最终归结为一个关于构造微积分的问题。

注意：我知道一个定理证明者跳过了递归/核心递归的终止检查/防护可以证明False\xe2\x80\x93so，如果有帮助，请将其视为有关非完全编程的问题而不是证明。

我们不能以无限精度存储小数,但可能有某种方式来表示它们就像我们在haskell中表示无限列表一样.

我想到的第一个想法是通过类似于Codata的东西来表示十进制数,因此对于任何给定的自然数k,我们可以将精确的十进制数计算为k位.

但有一些明显的问题,想想数a = 0.333...和b = 0.666...,如果我们加在一起,我们得到了ans = 0.999...(数字序列),但我们永远无法知道是否a + b == 1在这种情况下.

我要的是,以某种方式定义十进制数,使之支持+,-,*,/,>,==运营,不管是什么+,-,*,/我们应用到这些十进制数字操作,我们得到新的十进制数,我们可以计算出它们给定任何自然数k精确到k位数.

我想知道:有什么想法可以解决这个问题吗？