Utils.Streaming

(source)

References:
- https://github.com/MarcelineVQ/idris2-streaming
- https://hackage.haskell.org/package/streaming

Definitions

data Of : Type -> Type -> Type

Totality: total
Visibility: public export
Constructor:

(:>) : a -> Lazy b -> Of a b

Hints:

Bifunctor Of
Functor (Of a)

data Stream : (Type -> Type) -> (Type -> Type) -> Type -> Type

  The `Stream` type

Totality: not strictly positive
Visibility: public export
Constructors:

Step : Inf (f (Stream f m r)) -> Stream f m r
Effect : Inf (m (Stream f m r)) -> Stream f m r
Return : r -> Stream f m r
Build : ((r -> b) -> (m b -> b) -> (f b -> b) -> b) -> Stream f m r

Hints:

(Functor f, Monad m) => Applicative (Stream f m)
(Functor f, Monad m) => Functor (Stream f m)
(HasIO m, Monad (Stream f m)) => HasIO (Stream f m)
(Functor f, Monad m) => Monad (Stream f m)
MonadTrans (Stream f)

wrap : f (Stream f m r) -> Stream f m r

  Wrap a new layer of a `Stream`

Visibility: export

effect : m (Stream f m r) -> Stream f m r

  Wrap a new effect layer of a `Stream`

Visibility: export

build : ((r -> b) -> (m b -> b) -> (f b -> b) -> b) -> Stream f m r

Visibility: export

fold : (Functor f, Monad m) => (r -> b) -> (m b -> b) -> (f b -> b) -> Stream f m r -> b

Visibility: export

destroy : (Functor f, Monad m) => (f a -> a) -> (m a -> a) -> (r -> a) -> Stream f m r -> a

Visibility: export

unfold : (Functor f, Monad m) => (a -> m (Either r (f a))) -> a -> Stream f m r

  Unfold a `Stream`

Visibility: public export

inspect : (Functor f, Monad m) => Stream f m r -> m (Either r (f (Stream f m r)))

Visibility: export

hoist : (Functor f, Monad m) => (m a -> n a) -> Stream f m r -> Stream f n r

Visibility: export

yield : Monad m => a -> Stream (Of a) m ()

Visibility: export

run : Monad m => Stream m m r -> m r

Visibility: export

toList : Monad m => Stream (Of a) m r -> m (List a, r)

  Turns a `Stream` into a list

Visibility: public export

toList_ : Monad m => Stream (Of a) m r -> m (List a)

  `toList` but discards the result

Visibility: public export

fromList : r -> List a -> Stream (Of a) m r

  Construct a `Stream` from a `List` with a result type

Visibility: public export

fromList_ : List a -> Stream (Of a) m ()

  `fromList` but discards the result

Visibility: public export

cons : a -> Stream (Of a) m r -> Stream (Of a) m r

  Concatenate an element into a `Stream`

Visibility: public export
Fixity Declaration: infixr operator, level 5

next : Monad m => Stream (Of a) m r -> m (Either r (a, Stream (Of a) m r))

Visibility: export

mapf : (Functor f, Monad m) => (f x -> g x) -> Stream f m r -> Stream g m r

Visibility: export

mapfM : (Monad m, Functor f) => (f x -> m (g x)) -> Stream f m r -> Stream g m r

Visibility: export

maps : Monad m => (a -> b) -> Stream (Of a) m r -> Stream (Of b) m r

Visibility: export

mapsM : Monad m => (a -> m b) -> Stream (Of a) m r -> Stream (Of b) m r

Visibility: export

fors : Monad m => (a -> m x) -> Stream (Of a) m r -> m r

Visibility: export

takeStream : Monad m => Nat -> Stream (Of a) m r -> m (List a, Either r (Stream (Of a) m r))

Visibility: export

chunksOf : Monad m => (n : Nat) -> {auto 0 _ : NonZero n} -> Stream (Of a) m r -> Stream (Of (List a)) m r

  Split the stream into stream of sublist of length at most n

Visibility: export

consume : Monad m => Stream (Of a) m r -> m ()

  Consume all the content in the stream

Visibility: export