idris - Evaluating `IO` Actions from REPL -

given:

*lecture2> :let x = (the (io int) (pure 42)) 

looking @ type, what's meaning of mkffi c_types string string signature?

*lecture2> :t x x : io' (mkffi c_types string string) int 

i attempted evaluate x repl:

*lecture2> :exec x main:when checking argument value function prelude.basics.the:         type mismatch between                 io int (type of x)         ,                 integer (expected type) 

also, why doesn't 42 print out in repl?

looking @ type, what's meaning of mkffi c_types string string signature?

the io' type constructor parametrised on ffi available within it. it'll different depending on e.g. backend want target. here have access c ffi the default 1 io picks.

you can find out these things using :doc in repl. e.g. :doc io' yields:

data type io' : (lang : ffi) -> type -> type     io type, parameterised on ffi available within it.  constructors:     mkio : (world -> primio (worldres a)) -> io' lang 

also, why doesn't 42 print out in repl?

i don't know how :exec x supposed work can evaluate x in interpreter using :x x instead , yield sensible output:

idris> :x x mkio (\w => prim_io_pure 42) : io' (mkffi c_types string string) int