評估`從REPL

Question

IO`操作考慮：

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

看着它的類型，有什麼MkFFI C_Types String String簽名的含義是什麼？

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

然後我嘗試從REPL評估x：

*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) 

另外，爲什麼不中REPL 42打印出來？

Answer 1

看看它的類型，MkFFI C_Types String String簽名是什麼意思？

IO' type constructor通過其中可用的FFI進行參數化。它會根據例如您想要定位的後端。在這裏您可以訪問C FFI，即the default one IO picks。

您可以在REPL中使用:doc瞭解這些內容。例如。 :doc IO'產量：

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 

另外，爲什麼不中REPL 42打印出來？

我不知道該怎麼:exec x應該工作，但你可以在解釋使用:x x，而不是評估x並沒有得到合理的輸出：

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