How to pass function through a custom Idris FFI?

Question

I'm trying to implement the FFI part for my codegen, and although passing values like Int works, my biggest issue is figuring out how to pass a function.

So, in the docs there is this example with the JS FFI, that passes a function to the JS world, calls it there, and gets the result back, which is what I'm trying to implement. The code in the docs is this:

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

and the Idris code for the FFI binding is this one:

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

I don't have access to the mkForeign function, because it looks that is from the JS codegen RTS. So I tried to use foreign from Idris builtins:

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

Which errors in:

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)

Which I guess it is due to the last parameter of foreign , which has type

{auto fty : FTy f [] ty}

Documented as:

fty - an automatically-found proof that the Idris type works with the FFI in question

How does one satisfy this proof? I'm pretty lost at this point

Have you seen this?: docs.idris-lang.org/en/latest/reference/… The part of the docs you're looking at look out of date. Also, where is FFI_AHK coming from? — Joomy Korkut
@JoomyKorkut thanks for this, I haven't seen that page, it is very useful for what I'm trying to accomplish :) — Nick Tchayka

Nick Tchayka Nick Tchayka · Accepted Answer · 2020-03-15T16:41:11

The JavaScript FFI descriptor part of the docs was very useful in order to fix this.

What was needed was to provide an additional data type in order to wrap the functions so Idris can autogenerate the fty parameter of foreign.

The complete FFI definition of my code generator looks like this:

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

In order to write the twice function above, one can wrap the function type with AutoHotkeyFn and then do the same with the value of the function, by wrapping it in 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

How to pass function through a custom Idris FFI?

1 Answers