は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でパラメータ化されています。例えば、それに応じて異なります。ターゲットとするバックエンドここでは、the default one IO picksであるC FFIにアクセスできます。

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 

を