如何在 agda 中使用流？

Question

我已经在 Agda 中编写了流数据类型和一个头部操作。现在我想检查头部操作是否正确。

所以我将输入流设为 1 :: 2 :: 3 :: 。 . .但是 agda 不接受这个作为流。

所以我的问题是如何定义流？？

请帮忙。

Answer 1

有几种可能。

使用Data.Stream 模块，您可以像这样定义一个无限序列1 2 3 1 2 3 1 2 3 ...：

open import Data.Stream
open import Coinduction

stream : Stream ℕ
stream = 1 ∷ ♯ (2 ∷ ♯ (3 ∷ ♯ stream))

使用Data.Colist 模块，您可以定义有限和无限序列：

open import Data.Colist
open import Coinduction

colist-fin : Colist ℕ
colist-fin = 1 ∷ ♯ (2 ∷ ♯ (3 ∷ ♯ []))

colist-inf : Colist ℕ
colist-inf = 1 ∷ ♯ (2 ∷ ♯ (3 ∷ ♯ colist-inf))

您还可以将Stream 数据类型定义为互感记录：

{-# OPTIONS --copatterns #-}

record Stream {α} (A : Set α) : Set α where
  coinductive
  constructor _∷_
  field
    head : A
    tail : Stream A
open Stream

zeros : Stream ℕ
head zeros = 0
tail zeros = zeros

但是，copatterns 不能很好地与 Agda 的其余部分配合使用（摘自发行说明）：

 Copatterns are yet experimental and the following does not work:
* Copatterns and 'with' clauses.
* Compilation of copatterns to Haskell, JS, or Epic.
* Projections generated by
open R {{...}}
are not handled properly on lhss yet.
* Conversion checking is slower in the presence of copatterns,
since stuck definitions of record type do no longer count
as neutral, since they can become unstuck by applying a projection.
Thus, comparing two neutrals currently requires comparing all
they projections, which repeats a lot of work.