Lazy State monad in Idris

Question

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?

Lazy State monad in Idris

0 Answers