I am trying to generate a Stream value in a monadic context. For example, the following code hangs in Idris (or segfaults):
import Control.Monad.State
count : State Int (Stream Int)
count = do
x <- get
put (x+1)
t <- count
pure (x :: t)
stream : List Int
stream = take 10 (evalState count 0)
However, similar code works in Haskell, using the lazy state monad:
import Control.Monad.State.Lazy
count :: State Int [Int]
count = do
x <- get
put (x+1)
t <- count
return (x : t)
stream :: [Int]
stream = take 10 (evalState count 0)
This is probably because of lazy pattern matching used in the bind operation of the state monad in Haskell. Is there something similar in Idris?