idris-lang/Idris2

Unlawful `Monad` implementation for `Stream`

Closed this issue · 1 comments

> :module Data.Stream
> :doc Stream
data Prelude.Stream.Stream : Type -> Type
  An infinite stream.
  Totality: total
  Visibility: public export
  Constructor: (::) : a -> Inf (Stream a) -> Stream a
  Hints:
    Applicative Stream
    Functor Stream
    Monad Stream
    Zippable Stream

Given that we defined Monad Stream, the Applicative instance shouldn't have the zippy behaviour if we want the instance to be lawful.
And yet...

> :printdef Applicative Stream
pure : a -> Stream a
pure = repeat

(<*>) : Stream (a -> b) -> Stream a -> Stream b
(<*>) = zipWith apply

😱

I'm being daft 🤨