如何通过自定义Idris FFI传递功能？

Question

[我正在尝试为我的代码源实现FFI部分，尽管传递Int之类的值有效，但是我最大的问题是弄清楚如何传递函数。

所以，in the docs there is this example with the JS FFI，它将一个函数传递给JS世界，在那调用它，然后返回结果，这就是我要实现的目标。文档中的代码是这样的：

function twice(f, x) {
  return f(f(x));
}

和用于FFI绑定的Idris代码是这个：

twice : (Int -> Int) -> Int -> IO Int
twice f x = mkForeign (
  FFun "twice(%0,%1)" [FFunction FInt FInt, FInt] FInt
) f x

我无权访问mkForeign函数，因为它看起来是从JS代码生成的RTS中获取的。因此，我尝试使用Idris内置程序中的foreign：

twice : (Int -> Int) -> Int -> IO Int
twice =
  foreign FFI_AHK "twice"
    ((Int -> Int) -> Int -> IO Int)

哪个错误：

When checking right hand side of twice with expected type
        (Int -> Int) -> Int -> IO Int
When checking argument fty to function foreign:
        Can't find a value of type
                FTy FFI_AHK [] ((Int -> Int) -> Int -> IO Int)

我想这是由于foreign的最后一个参数具有类型

{auto fty : FTy f [] ty}

记录为：

fty-Idris类型可与相关FFI一起使用的自动发现的证明

一个人如何满足这一证明？我现在很迷路

Answer 1

The JavaScript FFI descriptor部分文档对于解决此问题非常有用。

[需要提供其他数据类型以包装函数，以便Idris可以自动生成fty的foreign参数。

我的代码生成器的完整FFI定义如下：

mutual
  public export
  data AutoHotkeyFn t = MkAutoHotkeyFn t

  public export
  data AHK_FnTypes : Type -> Type where
    AHK_Fn : AHK_Types s -> AHK_FnTypes t -> AHK_FnTypes (s -> t)
    AHK_FnIO : AHK_Types t -> AHK_FnTypes (IO' l t)
    AHK_FnBase : AHK_Types t -> AHK_FnTypes t

  public export
  data AHK_Types : Type -> Type where
    AHK_Str    : AHK_Types String
    AHK_Int    : AHK_Types Int
    AHK_Float  : AHK_Types Double
    AHK_Unit   : AHK_Types ()
    AHK_Raw    : AHK_Types (Raw a)
    AHK_FnT    : AHK_FnTypes t -> AHK_Types (AutoHotkeyFn t)

  public export
  data AHK_Foreign
    = AHK_DotAccess String String
    | AHK_Function String

  public export
  FFI_AHK : FFI
  FFI_AHK = MkFFI AHK_Types AHK_Foreign String

为了编写上面的twice函数，可以用AutoHotkeyFn包装函数类型，然后通过将其包装在MkAutoHotkeyFn中来对函数的值进行相同处理：

twice : (Int -> Int) -> Int -> AHK_IO Int
twice f x =
  foreign FFI_AHK (AHK_Function "twice")
    (AutoHotkeyFn (Int -> Int) -> Int -> AHK_IO Int)
    (MkAutoHotkeyFn f)
    x