Unlawful `Monad` implementation for `Stream`
Closed this issue · 1 comments
gallais commented
> :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
😱
gallais commented
I'm being daft 🤨