sdf.idr

data Of : Type -> Type -> Type where
  ||| Streaming depends on the Lazyness of r currently
  (:>) : a -> Lazy r -> Of a r

data Stream : (f : Type -> Type) -> (m : Type -> Type) -> Type -> Type where
  Return : (1 _ : r) -> Stream f m r
  Effect : (1 _ : m (Stream f m r)) -> Stream f m r
  Step : (1 _ : f (Stream f m r)) -> Stream f m r
  ||| Fusion constructor
  ||| We don't have a serious rewrite system in idris2 yet so this does the job
  ||| of fusing as long as we're careful about using streamFold and Build
  ||| whenever we can.
  Build : (1 _ : (forall b. (r -> b) -> (m b -> b) -> (f b -> b) -> b)) -> Stream f m r

||| `map` to the (f)unctor of `Stream (f) m r`.
mapf : (Functor f, Monad m)
    => (forall x. f x -> g x) -> Stream f m r -> Stream g m r
mapf f s = Build (\r,eff,step => streamFold r eff (step . f) s)

||| `map` (s)tream _values_, i.e. `a` in `Stream (Of a) m r`.
||| The name is partly to remove clashing with Functor `map`.
maps : Monad m -- aka map
    => (a -> b) -> Stream (Of a) m r -> Stream (Of b) m r
maps f s = mapf (first f) s

||| `map` effectfully to the (f)unctor of `Stream (f) (m) r`.
mapfM : (Monad m, Functor f)
     => (forall x. f x -> m (g x)) -> Stream f m r -> Stream g m r
mapfM f s = Build (\r,eff,step => streamFold r eff (eff . map step . f) s)

||| `map` (s)tream _values_ effectfully, i.e. `a` in `Stream (Of a) m r`.
mapsM : Monad m
    => (a -> m b) -> Stream (Of a) m r -> Stream (Of b) m r
mapsM f s = mapfM (\(c :> g) => (:> g) <$> f c) s