具有单子效果的流类型

Question

是否有一个标准类型（尤其是在 stdlib 中）用于

Stream

类型（我的意思是潜在的无限惰性序列），它允许在访问下一个元素时产生效果？像这样的伪代码（对于 monad

m

，元素类型

a

）

m (a, m (a, m (a, m (a, ...

我尝试从 stdlib 修改

Stream

但一直在获取

Error: StreamM is not total, not strictly positive

我很难记住确切的实现方式，但这里有一个没有

Monad

data StreamM : (Type -> Type) -> Type -> Type where
  (::) : a -> Inf (m (StreamM m a)) -> StreamM m a

我对 codata 的了解很少。

上下文

我正在生成一个唯一命名的值流，其中每个值都取决于所有先前的值（和其他一些东西）。 monad

m

生成名称。