Evaluating "IO" actions from the REPL
Given:
*lecture2> :let x = (the (IO Int) (pure 42))
Looking at its type, what does the signature mean MkFFI C_Types String String
?
*lecture2> :t x
x : IO' (MkFFI C_Types String String) Int
Then I tried 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 it 42
print to the REPL?
source to share
Looking at its type, what does the signature mean
MkFFI C_Types String String
?
The type constructor is specified by the FFI parameter available inside it. This will differ depending on, for example, the backend you want to target. Here you have access to C FFI, which is selected by default . IO'
IO
You can find out about this using :doc
the REPL. For example. :doc IO'
gives:
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 isn't 42 showing up in the REPL editor?
I don't know how it :exec x
should work, but you can evaluate x
in the interpreter by using instead :x x
and this gives a reasonable result:
Idris> :x x
MkIO (\w => prim_io_pure 42) : IO' (MkFFI C_Types String String) Int
source to share