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