Sep 30, 2021

Idris2 FFI

Idris has a simple FFI, the following code is an example.%foreign "C:puts,libc" prim__puts : String -> PrimIO IntTo avoid duplicate typing, we usually would writelibc : String -> String libc fname = "C:" ++ fname ++ ",libc" %foreign libc "puts" prim__puts : String -> PrimIO IntThen we would like to wrap puts as more general type. Thus, we getputs : HasIO io => String -> io Int puts s = primIO $ prim__puts... more