FFI 概述

外部函数使用 %foreign 指令声明，它采用以下一般形式：

%foreign [specifiers]
name : t

说明符是一个 Idris String ，它表示外部函数是用哪种语言编写的，它被称为什么，以及在哪里可以找到它。可能有多个说明符，并且代码生成器可以自由选择它理解的任何说明符 - 甚至完全忽略说明符并使用自己的方法。通常，说明符的形式为“Language:name,library”。例如，在 C 中：

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

由特定的代码生成器决定如何定位函数和库。在本文档中，我们将假设默认的 Chez Scheme 代码生成器（示例也适用于 Racket 或 Gambit 代码生成器）并且外部语音是 C。

C 函数的 FFI 声明也可以选择性地接受一个 C 头文件，该文件将被 #include 到由 Idris2 编译器生成的 C 代码中。例如：

%foreign "C:idris2_resetRawMode, libidris2_support, idris_support.h"
idris2_resetRawMode : (1 x : %World) -> IORes ()

FFI 声明可以在另一个文件中使用 %foreign_impl 编译指令进行扩展。当使用第三方后端时，此编译指令可用于填充标准库中未处理的情况。对于给定后端的多个声明，将使用最后加载的模块中的声明。

%foreign_impl Prelude.IO.prim__fork "javascript:lambda:(proc) => { throw new Error() }"

Scheme 详情

可以编写 Scheme 外部说明符以针对特定目标的口味。

以下示例显示了一个外部声明，它以特定于代码生成器选择的方式分配内存。在此示例中，不存在匹配每种风味的通用方案说明符，例如 scheme:foo ，所以它只会匹配列出的特定口味：

%foreign "scheme,chez:foreign-alloc"
         "scheme,racket:malloc"
         "C:malloc,libc"
allocMem : (bytes : Int) -> PrimIO AnyPtr

备注

如果您的后端（代码生成器）未指定但定义了 C FFI，它将能够使用 C:malloc,libc 说明符。

C 旁注

C 语言说明符用于任何后端都可以使用的通用函数，而后端又可以将 FFI 输出到 C。例如，Scheme。

常见的 C 函数不进行自动内存管理，将其推迟到各个后端。

标准 C 后端称为“RefC”，并使用 RefC 语言说明符。

Javascript 详情

Javascript 外部说明符可以针对 browser、node 或 javascript 编写。前两者互斥，而 javascript FFI 说明符在构建浏览器版本和 NodeJS 版本时都适用。

Javascript 说明符必须进一步指定为 lambda、support 或 stringIterator。

因此，语法是 node:lambda:some_func``（用于 NodeJS 特定的 FFI 和执行名为 ``some_func 的函数的 lambda）。

使用 support 选项时，还需要指定支持文件的名称。Idris 将在 js 子文件夹下的所有 data 目录中查找具有此名称的文件。这些文件名应该为您的项目所独有，这样它们就不会与可执行文件构建过程中其他项目的支持文件发生冲突。假设您的包名为 "http-idris"，并且在 Idris 代码中有类似 node:support:http_request,http_idris 的 FFI 说明符。您应该确保作用域内的 data 目录有一个包含 http_idris.js 文件的 js 目录。另一个重要说明是，此文件中的函数必须以 http_idris_ 为前缀；因此，我们在示例中引用的函数在 http_idris.js 支持文件中需要命名为 http_idris_http_request。

FFI 示例

作为一个运行示例，我们将使用一个小的 C 文件。将以下内容保存到文件 smallc.c

#include <stdio.h>

int add(int x, int y) {
    return x+y;
}

int addWithMessage(char* msg, int x, int y) {
    printf("%s: %d + %d = %d\n", msg, x, y, x+y);
    return x+y;
}

然后，将其编译为共享库：

cc -shared smallc.c -o libsmall.so

我们现在可以编写一个 Idris 程序来调用其中的每一个函数。首先，我们将编写一个小程序，它使用 add 将两个整数相加：

%foreign "C:add,libsmall"
add : Int -> Int -> Int

main : IO ()
main = printLn (add 70 24)

%foreign 说明符声明 add 是用 C 语言编写的，在 libsmall 库中名为 add 。只要运行时能够找到 libsmall.so （实际上它会在当前目录和系统库路径中查找），我们就可以在 REPL 中运行它：

Main> :exec main
94

请注意，确保 Idris 函数和 C 函数具有相应的类型是程序员的责任。机器没有办法检查这个！如果你弄错了，你会得到不可预测的行为。

由于 add 没有副作用，我们给它一个 Int 返回类型。但是如果这个函数对外界有一些影响，比如 addWithMessage 呢？在这种情况下，我们使用 PrimIO Int 来表示它返回一个原语 IO 操作：

%foreign "C:addWithMessage,libsmall"
prim__addWithMessage : String -> Int -> Int -> PrimIO Int

在内部， PrimIO Int 是一个函数，它获取世界的当前（线性）状态，并返回一个带有更新的世界状态的 Int 。通常，Idris 程序中的 IO 操作被定义为 HasIO 接口的实例。我们可以使用 primIO 将原语操作转换为 HasIO 中可用的操作：

primIO : HasIO io => PrimIO a -> io a

因此，我们可以如下扩展我们的程序：

addWithMessage : HasIO io => String -> Int -> Int -> io Int
addWithMessage s x y = primIO $ prim__addWithMessage s x y

main : IO ()
main
    = do printLn (add 70 24)
         addWithMessage "Sum" 70 24
         pure ()

程序员可以通过 PrimIO 声明哪些函数是纯函数，哪些有副作用。执行以下内容：

Main> :exec main
94
Sum: 70 + 24 = 94

我们已经看到了两个外部函数的说明符：

%foreign "C:add,libsmall"
%foreign "C:addWithMessage,libsmall"

它们都具有相同的形式： "C:[name],libsmall" ，所以我们可以不写具体的 String ，而是写一个函数来计算说明符，并使用它来代替现在的字符串：

libsmall : String -> String
libsmall fn = "C:" ++ fn ++ ",libsmall"

%foreign (libsmall "add")
add : Int -> Int -> Int

%foreign (libsmall "addWithMessage")
prim__addWithMessage : String -> Int -> Int -> PrimIO Int

原语 FFI 类型

可以传递给外部函数和从外部函数返回的类型仅限于可以合理假设任何后端都可以处理的类型。在实践中，这意味着大多数原语类型，以及有限的其他类型。参数类型可以是以下任何原语：

Int
Char
Double （在 C 中为 double ）
Bits8
Bits16
Bits32
Bits64
String (在 C 中作为 char*)
Ptr t 和 AnyPtr （在 C 中都是 void* ）

返回类型可以是上述任何一种，加上：

()
PrimIO t ，其中 t 是除了 PrimIO 之外的有效返回类型。

处理 String 会导致一些复杂性，原因有很多：

字符串可以有多种编码。在 Idris 运行时，字符串被编码为 UTF-8，但 C 不做任何假设。
谁负责释放由 C 函数分配的字符串并不总是很清楚。
在 C 中，字符串可以是 NULL ，但 Idris 字符串总是有一个值。

因此，当将 String 传入和传出 C 时，请记住以下几点：

C 函数返回的 char* 将被复制到 Idris 堆，并且 Idris 运行时立即对返回的 char* 调用 free 函数。
如果 char* 在 C 中可能是 NULL ，请使用 Ptr String 而不是 String 。

当使用 Ptr String 时，该值将作为 void* 传递，因此 Idris 代码不能直接访问。这是为了防止意外尝试将 NULL 用作 String 。尽管如此，您仍然可以使用它们并通过以下形式的外部函数转换为 String ：

char* getString(void *p) {
    return (char*)p;
}

void* mkString(char* str) {
    return (void*)str;
}

int isNullString(void* str) {
    return str == NULL;
}

例如，请参阅示例示例：最简 Readline 绑定绑定。

此外，外部函数可以接受*回调*，并接受和返回 C struct 指针。

回调

在 C 语言中，函数接受 callback 是很有用的，它是在完成一些工作后调用的函数。例如，我们可以编写一个函数，该函数接受一个回调，该回调接受一个 char* 和一个 int 并返回一个 char* ，在 C 语言中，如下所示（添加到 smallc. c 上面）：

typedef char*(*StringFn)(char*, int);

char* applyFn(char* x, int y, StringFn f) {
    printf("Applying callback to %s %d\n", x, y);
    return f(x, y);
}

然后，我们可以通过将其声明为 %foreign 函数并将其包装在 HasIO 接口中来从 Idris 访问它，其中 C 函数调用 Idris 函数作为回调：

%foreign (libsmall "applyFn")
prim__applyFn : String -> Int -> (String -> Int -> String) -> PrimIO String

applyFn : HasIO io =>
          String -> Int -> (String -> Int -> String) -> io String
applyFn c i f = primIO $ prim__applyFn c i f

例如，我们可以尝试如下：

pluralise : String -> Int -> String
pluralise str x
    = show x ++ " " ++
             if x == 1
                then str
                else str ++ "s"

main : IO ()
main
    = do str1 <- applyFn "Biscuit" 10 pluralise
         putStrLn str1
         str2 <- applyFn "Tree" 1 pluralise
         putStrLn str2

作为一种变体，回调可能会产生副作用：

%foreign (libsmall "applyFn")
prim__applyFnIO : String -> Int -> (String -> Int -> PrimIO String) ->
                 PrimIO String

由于有回调，这对于提升到 HasIO 函数有点复杂，但是我们可以使用 toPrim : IO a -> PrimIO a 来做到这一点：

applyFnIO : HasIO io =>
            String -> Int -> (String -> Int -> IO String) -> io String
applyFnIO c i f = primIO $ prim__applyFnIO c i (\s, i => toPrim $ f s i)

请注意，回调显式的被包裹在 IO 中，因为 HasIO 没有提取原语 IO 操作的通用方法。

例如，我们可以扩展上面的 pluralise 示例以在回调中打印一条消息：

pluralise : String -> Int -> IO String
pluralise str x
    = do putStrLn "Pluralising"
         pure $ show x ++ " " ++
                if x == 1
                   then str
                   else str ++ "s"

main : IO ()
main
    = do str1 <- applyFnIO "Biscuit" 10 pluralise
         putStrLn str1
         str2 <- applyFnIO "Tree" 1 pluralise
         putStrLn str2

结构体

许多 C API 传递更复杂的数据结构，如 struct 。我们并不打算在我们支持的 C 类型中完全通用，因为这会使编写跨多个后端可移植的代码变得更加困难。但是，能够直接访问 struct 通常会很有用。例如，将以下内容添加到 smallc.c 的顶部，并重新构建 libsmall.so ：

#include <stdlib.h>

typedef struct {
    int x;
    int y;
} point;

point* mkPoint(int x, int y) {
    point* pt = malloc(sizeof(point));
    pt->x = x;
    pt->y = y;
    return pt;
}

void freePoint(point* pt) {
    free(pt);
}

我们可以通过导入 System.FFI 并使用 Struct 类型在 Idris 中定义一个访问 point 的类型，如下所示：

Point : Type
Point = Struct "point" [("x", Int), ("y", Int)]

%foreign (libsmall "mkPoint")
mkPoint : Int -> Int -> Point

%foreign (libsmall "freePoint")
prim__freePoint : Point -> PrimIO ()

freePoint : Point -> IO ()
freePoint p = primIO $ prim__freePoint p

现在 Idris 中的 Point 类型对应 C 中的 point*。

重要：Struct 类型必须定义 C struct 的所有字段。部分定义将导致内存访问错误。

可以使用以下方法读取和写入字段，这些方法也来自 System.FFI ：

getField : Struct s fs -> (n : String) ->
           FieldType n ty fs => ty
setField : Struct s fs -> (n : String) ->
           FieldType n ty fs => ty -> IO ()

请注意，字段是按名称访问的，并且必须在结构中可用，给定约束 FieldType n ty fs ，它指出结构字段 fs 中名为 n 的字段具有类型 ty 。因此，我们可以通过如下所示直接访问字段来显示 Point ：

showPoint : Point -> String
showPoint pt
    = let x : Int = getField pt "x"
          y : Int = getField pt "y" in
          show (x, y)

而且，作为一个完整的例子，我们可以初始化、更新、显示和删除一个 Point ，如下所示：

main : IO ()
main = do let pt = mkPoint 20 30
          setField pt "x" (the Int 40)
          putStrLn $ showPoint pt
          freePoint pt

Struct 的字段类型可以是以下任何一种：

Int
Char
Double (C 中为 double)
Bits8
Bits16
Bits32
Bits64
Ptr a 或 AnyPtr （C 中的 void* ）
另一个 Struct ，在C中它是指向 struct 的指针

请注意，这不包括 String 或函数类型！这主要是因为 Chez 后端不直接支持这些。但是，您可以使用另一种指针类型并进行转换。例如，假设你在 C 中有：

typedef struct {
    char* name;
    point* pt;
} namedpoint;

您可以在 Idris 中将其表示为：

NamedPoint : Type
NamedPoint
    = Struct "namedpoint"
               [("name", Ptr String),
               ("pt", Point)]

也就是说，直接使用 Ptr String 而不是 String 。然后你可以在 C 中的 void* 和 char* 之间进行转换：

char* getString(void *p) {
    return (char*)p;
}

...并在 Idris 中使用它转换为 String ：

%foreign (pfn "getString")
getString : Ptr String -> String

决赛选手

在某些库中，外部函数创建一个指针，调用者负责释放它。在这种情况下，您可以对 free 进行显式的外部调用。然而，这并不总是方便的，甚至是不可能的。相反，您可以使用 Prelude 中定义的 onCollect （或其无类型变体 onCollectAny ）要求 Idris 运行时负责在指针不再可访问时释放它：

onCollect : Ptr t -> (Ptr t -> IO ()) -> IO (GCPtr t)
onCollectAny : AnyPtr -> (AnyPtr -> IO ()) -> IO GCAnyPtr

当传递给外部函数时， GCPtr t 的行为与 Ptr t 完全相同（类似地， GCAnyPtr 的行为类似于 AnyPtr ）。然而，外部函数不能返回 GCPtr ，因为我们不能再假设指针完全由 Idris 运行时管理。

当垃圾收集器确定指针不再可访问时，或者在执行结束时调用终结器。

请注意，并非所有后端都支持终结器，因为它们依赖于特定后端运行时系统提供的设施。 Chez Scheme 和 Racket 后端肯定支持它们。