Как передать функцию через пользовательский Idris FFI? - PullRequest
Новая
       30

Как передать функцию через пользовательский Idris FFI?

1 голос
/ 15 марта 2020

Я пытаюсь реализовать часть FFI для моего codegen, и хотя передача значений типа Int работает, моя самая большая проблема - выяснить, как передать функцию.

Итак, в в документах есть этот пример с JS FFI , который передает функцию в мир JS, вызывает ее и возвращает результат, что я и пытаюсь реализовать. Код в документации выглядит следующим образом: 

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

, а код Idris для привязки FFI следующий: 

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

У меня нет доступа к функции mkForeign потому что, похоже, это из JS codegen RTS. Поэтому я попытался использовать foreign из встроенных Idris: 

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

Как можно удовлетворить это доказательство? Я довольно потерян в этот момент

1 Ответ

1 голос
/ 15 марта 2020

Часть документов JavaScript FFI документов была очень полезна для исправления этой проблемы.

Требовалось предоставить дополнительный тип данных для переноса функций поэтому 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
...