Evaluating `IO` Actions from REPL

Question

Given:

*lecture2> :let x = (the (IO Int) (pure 42))

Looking at its type, what's the meaning of the MkFFI C_Types String String signature?

*lecture2> :t x
x : IO' (MkFFI C_Types String String) Int

I then attempted to evaluate x from the REPL:

*lecture2> :exec x
main:When checking argument value to function Prelude.Basics.the:
        Type mismatch between
                IO Int (Type of x)
        and
                Integer (Expected type)

Also, why doesn't 42 print out in the REPL?

Answer 1

Looking at its type, what's the meaning of the MkFFI C_Types String String signature?

The IO' type constructor is parametrised over the FFI that is available within it. It'll be different depending on e.g. the backend you want to target. Here you have access to the C FFI which is the default one IO picks.

You can find out about these things by using :doc in the REPL. E.g. :doc IO' yields:

Data type IO' : (lang : FFI) -> Type -> Type
    The IO type, parameterised over the FFI that is available within it.

Constructors:
    MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a

Also, why doesn't 42 print out in the REPL?

I don't know how :exec x is supposed to work but you can evaluate x in an interpreter by using :x x instead and that does yield a sensible output:

Idris> :x x
MkIO (\w => prim_io_pure 42) : IO' (MkFFI C_Types String String) Int