Notes on Idris (2017)

Re:Notes on Idris (2017) by cannam on Sunday June 10, 2018 @01:22PM (#17279073)

Thank you! This is a really nice comment that gives plenty to think about. It's delightful that, two days later, you actually have expanded in compelling detail on what initially looked to be something of a throwaway remark.

I think that Idris tries to make the evaluation/execution distinction a bit more apparent. In particular, when you enter something effectful at the REPL, only the evaluation happens automatically and the result is printed in an internal form. This is confusing at first, but you can see that there's something tantalisingly interesting going on.

[ Parent | on HN ]

Re:Notes on Idris (2017) by kqr on Sunday June 10, 2018 @04:24PM (#17279984)

No problem whatsoever! I only wish I could have done it better.

I do like the way the Idris REPL does that, from your description. Didn't know that. How do you run it for effects?

[ Parent | on HN ]

Re:Notes on Idris (2017) by cannam on Monday June 11, 2018 @04:18AM (#17282671)

Using the :exec REPL command.

  Idris> putStrLn "Hello, world!"
  io_bind (prim_write "Hello, world!\n")
          (\__bindx => io_pure ()) : IO ()
  Idris> :exec putStrLn "Hello, world!"
  Hello, world!

[ Parent | on HN ]