3

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?

1
  • 1
    You would probably have to make your own lazy state monad. Idris has Lazy and Inf. Commented Dec 21, 2020 at 3:30

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.