improved repl

[kuribas]

The current idris repl only allows for evaluating pure functions. Having an interactive repl is very useful for exploring new ideas, and for iterative programming, where you test out your code as you write it.

This also means that pure code which uses side effects under the hood (unsafePerformIO), cannot be evaluated at the repl. Currently you can execute side effectful functions using :exec, but you cannot bind the result. This is useful for example to load data from a file, and then test functions on the contents of that file, for example loading xml data and testing a parser on it.

This could be done the way it is in ghci, whenever the repl encounters a IO value at toplevel, it will evaluate it, and display the result. You can also use monad do notation at toplevel, where it will then execute the IO action, and bind the result, which can then be used later for testing functions.

Example from haskell ghci:

> :t 4
4 :: Num a => a
> 4
4
> :t putStrLn "hello world"
putStrLn "hello world" :: IO ()
> putStrLn "hello world"
hello world
> x <- getLine
Kristof
>  putStrLn $ "hello " ++ x
hello Kristof

[kuribas]

Closing this because this is not an emacs issue, but should be developed on the idris implementation.

[gallais]

You can use :exec to run IO code in the REPL.

[kuribas]

But I cannot bind a result using :exec