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