流(无限列表)单声道模拟了什么效果? [英] What effects are modeled by the stream (infinite list) monad?

问题描述

各种monad实例对不同类型的效果进行建模:例如，Maybe对局部性建模，List非确定性建模，Reader只读状态.我想知道是否对流数据类型(或无限列表或共同列表)的单子实例data Stream a = Cons a (Stream a)有如此直观的解释(请参见其单子实例定义下方).我在很少

Various instances of monads model different type of effects: for example, Maybe models partiality, List non-determinism, Reader read-only state. I would like to know if there is such an intuitive explanation for the monad instance of the stream data type (or infinite list or co-list), data Stream a = Cons a (Stream a) (see below its monad instance definition). I've stumbled upon the stream monad on a few different occasions and I would like to understand better its uses.

data Stream a = Cons a (Stream a)

instance Functor Stream where
    fmap f (Cons x xs) = Cons (f x) (fmap f xs)

instance Applicative Stream where
    pure a                      = Cons a (pure a)
    (Cons f fs) <*> (Cons a as) = Cons (f a) (fs <*> as)

instance Monad Stream where
    xs >>= f = diag (fmap f xs)

diag :: Stream (Stream a) -> Stream a
diag (Cons xs xss) = Cons (hd xs) (diag (fmap tl xss))
    where
        hd (Cons a _ ) = a
        tl (Cons _ as) = as

P.S .:我不确定我的语言是否非常准确(尤其是在使用效果"一词时)，请随时纠正我.

P.S.: I'm not sure if I'm very precise in my language (especially when using the word "effect"), so feel free to correct me.

推荐答案

Stream单子与Reader Natural同构(Natural:自然数)，这意味着Stream和保留其单子结构.

The Stream monad is isomorphic to Reader Natural (Natural: natural numbers), meaning that there is a bijection between Stream and Reader Natural which preserves their monadic structure.

Stream a和Reader Natural a(Natural -> a)都可以视为表示由整数索引的a的无限集合.

Both Stream a and Reader Natural a (Natural -> a) can be seen as representing infinite collections of a indexed by integers.

fStream = Cons a0 (Cons a1 (Cons a2 ...))

fReader = \i -> case i of
  0 -> a0
  1 -> a1
  2 -> a2
  ...

它们的Applicative和Monad实例均按索引构成元素.显示Applicative的直觉更加容易.下面，我们显示了a0, a1, ...的A流和b0, b1, ...的B流及其组成AB = liftA2 (+) A B，以及等效的函数表示.

Their Applicative and Monad instances both compose elements index-wise. It's easier to show the intuition for Applicative. Below, we show a stream A of a0, a1, ..., and B of b0, b1, ..., and their composition AB = liftA2 (+) A B, and an equivalent presentation of functions.

fStreamA  = Cons  a0     (Cons  a1     ...)
fStreamB  = Cons     b0  (Cons     b1  ...)
fStreamAB = Cons (a0+b0) (Cons (a1+b1) ...)
fStreamAB = liftA2 (+) fStreamA fStreamB

-- lambda case "\case" is sugar for "\x -> case x of"
fReaderA = \case 0 -> a0    ; 1 -> a1    ; ...
fReaderB = \case 0 ->    b0 ; 1 -> b1    ; ...
fReaderC = \case 0 -> a0+b0 ; 1 -> a1+b1 ; ...
fReaderC = liftA2 (+) fReaderA fReaderB = \i -> fReaderA i + fReaderB i

正式

双射:

import Numeric.Natural  -- in the base library

-- It could also be Integer, there is a bijection Integer <-> Natural
type ReaderN a = Natural -> a

tailReader :: ReaderN a -> ReaderN a
tailReader r = \i -> r (i+1)

toStream :: ReaderN a -> Stream a
toStream r = Cons (r 0) (toStream (tailReader r))

fromStream :: Stream a -> ReaderN a
fromStream (Cons a s) = \i -> case i of
  0 -> a
  i -> fromStream s (i-1)

toStream和fromStream是双射，表示它们满足以下方程式:

toStream and fromStream are bijections, meaning that they satisfy these equations:

toStream (fromStream s) = s :: Stream a
fromStream (toStream r) = r :: ReaderN a

同构"是一个笼统的概念；同构的两件事通常意味着存在满足某些方程的双射，这取决于所考虑的结构或界面.在这种情况下，我们正在谈论单子的结构，如果存在满足这些方程的双射，则说两个单子是同构的.

"Isomorphism" is a general notion; two things being isomorphic usually means that there is a bijection satisfying certain equations, which depend on the structure or interface being considered. In this case, we are talking about the structure of monads, and we say that two monads are isomorphic if there is a bijection which satisfies these equations:

toStream (return a) = return a
toStream (u >>= k) = toStream u >>= (toStream . k)

这个想法是，无论我们在双射之前或之后应用函数return和(>>=)，我们都会得到相同的结果. (然后，可以从这两个方程以及上面的另两个方程中导出使用fromStream的相似方程).

The idea is that we get the same result whether we apply the functions return and (>>=) "before or after" the bijection. (The similar equations using fromStream can then be derived from these two equations and the other two above).

这篇关于流(无限列表)单声道模拟了什么效果?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！