idris2 FFI

Idris has a simple FFI, the following code is an example.

%foreign "C:puts,libc"
prim__puts : String -> PrimIO Int

To avoid duplicate typing, we usually would write

libc : String -> String
libc fname = "C:" ++ fname ++ ",libc"

%foreign libc "puts"
prim__puts : String -> PrimIO Int

Then we would like to wrap puts as more general type. Thus, we get

puts : HasIO io => String -> io Int
puts s = primIO $ prim__puts s