새로운 외부 함수 인터페이스

새로운 외부 함수 인터페이스 (New Foreign Function Interface)

Idris가 잠재적으로 서로 다른 플랫폼의 서로 다른 대상 언어로 컴파일하는 여러 백엔드를 갖게 된 이후로, 외부 함수 인터페이스(FFI, foreign function interface)가 C로 컴파일한다는 가정 아래 작성되었다는 문제가 있었어요. 그 결과, 여러 대상을 위한 일반 코드를 작성하거나, 코드가 컴파일된다면 예상된 대상에서 실행될 것이라고 확신하는 것조차 어려웠어요.

0.9.17부터 Idris는 여러 대상을 인식하는 새로운 외부 함수 인터페이스(FFI)를 갖게 돼요. 기본 코드 생성기로 작업하는 사용자들은 변경 없이 예전처럼 계속 프로그램을 작성해도 되지만, 외부 라이브러리에 대한 바인딩을 작성하거나, 백엔드를 작성하거나, 비-C 백엔드로 작업한다면 이 페이지가 설명하는 몇 가지 사항을 알아야 해요.

출처: 문서

본문

IO' 모나드와 main (The IO' monad, and main)

IO 모나드는 예전처럼 존재하지만, 이제는 C 백엔드(또는 더 정확히, 외부 함수 호출이 C와 호환되는 어떤 백엔드)에 특정해요. 추가로, 이제 FFI 기술자(descriptor)로 매개변수화된 IO' 모나드가 있어요:

data IO' : (lang : FFI) -> Type -> Type

Prelude는 C와 JavaScript/Node를 위한 두 개의 FFI 기술자를 자동으로 임포트되도록 정의하고, IO가 C FFI를 사용하고 JS_IO가 JavaScript FFI를 사용하도록 정의해요:

FFI_C  : FFI
FFI_JS : FFI

IO : Type -> Type
IO a = IO' FFI_C a

JS_IO : Type -> Type
JS_IO a = IO' FFI_JS a

예전처럼 Idris 프로그램의 진입점은 main이지만, main의 타입은 이제 IO'의 어떤 구현도 될 수 있어요. 예를 들어 다음 둘 다 유효해요:

main : IO ()
main : JS_IO ()

FFI 기술자는 어떤 타입들이 외부 언어와 Idris 사이에서 마샬링(marshalled)될 수 있는지, 그리고 외부 함수 호출의 "대상(target)"에 대한 세부 사항을 포함해요 (대개는 함수 이름의 String 표현이지만, 외부 라이브러리 파일이나 심지어 URL 같은 더 복잡한 것일 수도 있어요).

FFI 기술자 (FFI descriptors)

FFI 기술자는 타입이 마샬링될 수 있을 때 성립하는 술어(predicate)와, 외부 호출의 대상 타입을 포함하는 레코드예요:

record FFI where
     constructor MkFFI
     ffi_types : Type -> Type
     ffi_fn : Type

C에 대해서는 이것이 다음과 같아요:

||| Supported C integer types
public export
data C_IntTypes : Type -> Type where
    C_IntChar   : C_IntTypes Char
    C_IntNative : C_IntTypes Int
    C_IntBits8  : C_IntTypes Bits8
    C_IntBits16 : C_IntTypes Bits16
    C_IntBits32 : C_IntTypes Bits32
    C_IntBits64 : C_IntTypes Bits64

||| Supported C function types
public export
data C_FnTypes : Type -> Type where
    C_Fn : C_Types s -> C_FnTypes t -> C_FnTypes (s -> t)
    C_FnIO : C_Types t -> C_FnTypes (IO' FFI_C t)
    C_FnBase : C_Types t -> C_FnTypes t

||| Supported C foreign types
public export
data C_Types : Type -> Type where
    C_Str   : C_Types String
    C_Float : C_Types Double
    C_Ptr   : C_Types Ptr
    C_MPtr  : C_Types ManagedPtr
    C_Unit  : C_Types ()
    C_Any   : C_Types (Raw a)
    C_FnT   : C_FnTypes t -> C_Types (CFnPtr t)
    C_IntT  : C_IntTypes i -> C_Types i

||| A descriptor for the C FFI. See the constructors of `C_Types`
||| and `C_IntTypes` for the concrete types that are available.
%error_reverse
public export
FFI_C : FFI
    FFI_C = MkFFI C_Types String

외부 코드 연결하기 (Linking foreign code)

다음은 C 코드를 연결하는 예시예요.

%include C "mylib.h"
%link C "mylib.o"

Makefile 예시:

DEFAULT: mylib.o main.idr
    idris main.idr -o executableFile

clean:
    rm -f executableFile mylib.o main.ibc

외부 호출 (Foreign calls)

외부 함수를 호출하려면 foreign 함수를 사용해요. 예를 들어:

do_fopen : String -> String -> IO Ptr
do_fopen f m
   = foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m

foreign 함수는 FFI 설명, 함수 이름(여기서 FFI_C의 ffi_fn 필드로 주어진 타입), 그리고 남은 인자들의 예상 타입을 주는 함수 타입을 받아요. 여기서 우리는 C에서 char* 파일 이름과 char* 모드를 받고 파일 포인터를 반환하는 외부 함수 fileOpen을 호출하고 있어요. Idris String을 C char*으로, 그리고 그 반대로 변환하는 것은 C 백엔드의 몫이에요.

여기 주어진 인자 타입과 반환 타입은, foreign 호출이 유효하려면 FFI_C 설명의 fn_types 술어에 존재해야 해요.

주의: foreign의 인자들은 컴파일 타임에 알려져야 해요. foreign 호출은 정적으로 생성되기 때문이에요. 함수의 %inline 지시어는 이것을 돕기 위한 힌트를 주는 데 사용할 수 있어요. 예를 들어 외부 JavaScript 함수를 호출하는 축약:

%inline
jscall : (fname : String) -> (ty : Type) ->
          {auto fty : FTy FFI_JS [] ty} -> ty
jscall fname ty = foreign FFI_JS fname ty

C 콜백 (C callbacks)

함수 포인터를 받는 C 함수에 Idris 함수를 전달하는 것은 함수 타입에서 CFnPtr을 사용함으로써 가능해요. Idris 함수는 인자에서 MkCFnPtr로 전달돼요. 아래 예시는 비교 함수에 대한 포인터를 받는 C 표준 라이브러리 함수 qsort를 선언하는 것을 보여줘요.

myComparer : Ptr -> Ptr -> Int
myComparer = ...

qsort : Ptr -> Int -> Int -> IO ()
qsort data elems elsize = foreign FFI_C "qsort"
                (Ptr -> Int -> Int -> CFnPtr (Ptr -> Ptr -> Int) -> IO ())
                data elems elsize (MkCFnPtr myComparer)

C FFI에서 콜백에는 몇 가지 제한이 있어요. 외부 함수는 콜백으로 만들 함수를 인자로 받을 수 없어요. 이것은 컴파일 오류를 줄 거예요:

-- This does not work
example : (Int -> ()) -> IO ()
example f = foreign FFI_C "callbacker" (CFnPtr (Int -> ()) -> IO ()) f

콜백으로 사용되는 함수는 클로저(closure), 즉 부분 적용된 함수일 수 없다는 점을 주의하세요. 이것은 사용되는 메커니즘이 닫힌(closed-over) 값들을 C를 통해 전달할 수 없기 때문이에요. 콜백에 Idris 값을 전달하고 싶다면 그것들을 C를 통해 명시적으로 전달해야 해요. 비-기본(non-primitive) Idris 값은 Raw 타입을 통해 C에 전달될 수 있어요.

또 다른 큰 제한은 IO 함수를 지원하지 않는다는 것이에요. 그것들을 감싸기 위해 unsafePerformIO를 사용해요 (즉, IO 함수를 콜백으로 사용 가능하게 하려면 반환 타입을 IO r에서 r로 바꾸고, = do를 = unsafePerformIO $ do로 바꿔요).

두 개의 특별한 함수 이름이 있어요:

%wrapper는 Idris 함수를 감싸는 함수 포인터를 반환해요. 이것은 함수 포인터가 C 함수에 직접 받아지지 않고 데이터 구조에 삽입되어야 할 때 유용해요. %wrapper를 사용하는 foreign 선언은 IO Ptr을 반환해야 해요.

-- this returns the C function pointer to a qsort comparer
example_wrapper : IO Ptr
example_wrapper = foreign FFI_C "%wrapper" (CFnPtr (Ptr -> Ptr -> Int) -> IO Ptr)
                        (MkCFnPtr myComparer)

%dynamic은 C 함수 포인터를 인자들과 함께 호출해요. 이것은 C 함수가 C 함수 포인터를 반환하거나 데이터 구조가 C 함수 포인터를 포함할 때 유용해요. 예를 들어 함수 포인터의 구조체(struct)는 COM이나 Linux 커널 같은 객체 지향 C에서 흔해요. 함수 타입은 함수 포인터를 위해 시작 부분에 추가 Ptr을 포함해요. %dynamic은 첫 번째 인자의 함수를 호출하고 나머지 인자를 그것에 전달하는 의사-함수(pseudo-function)로 볼 수 있어요.

-- we have a pointer to a function with the signature int f(int), call it
example_dynamic : Ptr -> Int -> IO Int
example_dynamic fn x = foreign FFI_C "%dynamic" (Ptr -> Int -> IO Int) fn x

외부 이름이 &로 접두되면, 그것은 다음 이름을 가진 전역 변수에 대한 포인터로 취급돼요. 타입은 IO Ptr이어야 해요.

-- access the global variable errno
errno : IO Ptr
errno = foreign FFI_C "&errno" (IO Ptr)

외부 이름이 #로 접두되면, 이름은 문자 그대로 붙여넣어져요. 이것은 전처리기 정의(INT_MAX 같은)인 상수에 접근하는 데 유용해요.

%include C "limits.h"

-- access the preprocessor definition INT_MAX
intMax : IO Int
intMax = foreign FFI_C "#INT_MAX" (IO Int)

main : IO ()
main = print !intMax

C와의 더 복잡한 상호작용 (C 구조체의 필드를 읽고 설정하는 것 같은)을 위해서는, contrib 패키지에서 사용할 수 있는 C FFI 모듈이 있어요.

C 힙 (C heap)

Idris에는 객체가 할당될 수 있는 두 개의 힙이 있어요:

FP 힙	C 힙
Cheney 수집 (Cheney-collected)	표시-및-쓸기 수집 (Mark-and-sweep-collected)
가비지 컬렉션은 살아 있는 객체만 건드려요.	가비지 컬렉션은 등록된 모든 항목을 순회해야 해요.
데이터 생성자 같은 많은 작고 수명이 짧은 메모리 조각의 FP 스타일 빠른 할당에 이상적.	몇 개의 큰 버퍼의 C 스타일 할당에 이상적.
파이널라이저(finalizers)를 합리적으로 지원하는 것은 불가능해요.	항목에는 할당 해제 시 호출되는 파이널라이저가 있어요.
데이터는 항상 복사돼요 (가비지 수집, 데이터 수정, 관리 포인터 등록 시).	복사는 일어나지 않아요.
다양한 타입의 객체를 포함해요.	C 힙 항목을 포함해요: 파이널라이저를 가진 (void *) 포인터. 파이널라이저는 항목과 연관된 리소스를 할당 해제하는 루틴이에요.
고정된 객체 타입 집합.	데이터 포인터는 파이널라이저가 올바르게 정리하는 한 무엇이든 가리킬 수 있어요.
C 리소스와 임의 포인터에는 부적합.	C 리소스와 임의 포인터에 적합.
값들은 컴팩트한 메모리 블록을 형성해요.	항목들은 연결 리스트로 유지돼요.
어떤 Idris 값이든, 가장 특히 ManagedPtr.	항목들은 Idris 타입 CData로 표현돼요.
ManagedPtr의 데이터는 C에서 할당되고, 그 다음 버퍼가 FP 힙으로 복사돼요.	데이터는 C에서 할당되고, 포인터가 C 힙으로 복사돼요.
C 코드에서 (VM에 대한 참조 없이) 할당과 재할당은 불가능해요. 대신 모든 것이 복사돼요.	C에서 자유롭게 할당하고 재할당하며, 할당된 항목을 FFI에 등록해요.

FP 힙은 기본 힙이에요. 그것은 C 힙의 항목에 대한 참조인 타입 CData의 값을 포함할 수 있어요. C 힙 항목은 (void *) 포인터와 대응하는 파이널라이저를 포함해요. C 힙 항목이 FP 힙에서 더 이상 참조되지 않으면, 그것은 사용되지 않는 것으로 표시되고 다음 GC 스윕이 그 파이널라이저를 호출해 할당 해제해요.

CData에 대한 타입과 FFI 이외의 Idris 인터페이스는 없어요.

C 코드에서의 사용 (Usage from C code)

• 코드에서 강제되지는 않지만, CData는 불투명하도록 의도됐으며 비-RTS 코드(라이브러리나 C 바인딩 같은)는 그 (void *) 필드인 data에만 접근해야 해요.
• 포인터 데이터(realloc 호출 후 같은)와 그것이 가리키는 메모리 둘 다 변경해도 괜찮아요. 그러나 이것이 Idris의 참조 투명성(referential transparency)을 깨뜨려서는 안 된다는 점을 명심하세요.
• 경고! cdata_allocate나 cdata_manage를 호출하면, 결과 CData 객체가 RTS에 의해 C 힙에 삽입되도록 FFI 함수에서 반환되어야 해요. 그렇지 않으면 메모리가 누출돼요.

some_allocating_fun : Int -> IO CData
some_allocating_fun i = foreign FFI_C "some_allocating_fun" (Int -> IO CData) i

other_fun : CData -> Int -> IO Int
other_fun cd i = foreign FFI_C "other_fun" (CData -> Int -> IO Int) cd i

#include "idris_rts.h"

static void finalizer(void * data)
{
    MyStruct * ptr = (MyStruct *) data;
    free_something(ptr->something);
    free(ptr);
}

CData some_allocating_fun(int arg)
{
    size_t size = sizeof(...);
    void * data = (void *) malloc(size);
    // ...
    return cdata_manage(data, size, finalizer);
}

int other_fun(CData cd, int arg)
{
    int result = foo(cd->data);
    return result;
}

Raw 타입 생성자는 값의 런타임 표현에 접근하거나 반환하게 해줘요. 예를 들어, C 코드에서 생성된 문자열을 Idris 값으로 복사하고 싶다면, String 대신 Raw String을 반환하고 MKSTR 또는 MKSTRlen을 사용해 복사하길 원할 거예요.

getString : () -> IO (Raw String)
getString () = foreign FFI_C "get_string" (IO (Raw String))

const VAL get_string ()
{
    char * c_string = get_string_allocated_with_malloc()
    const VAL idris_string = MKSTR(get_vm(), c_string);
    free(c_string);
    return idris_string
}

FFI 구현 (FFI implementation)

외부 라이브러리에 대한 바인딩을 작성하려면, foreign이 어떻게 작동하는지에 대한 세부 사항은 필요하지 않아요: 간단히 foreign이 FFI 기술자, 함수 이름, 그리고 그 타입을 받는다는 것을 알면 돼요. 그러나 조금 더 깊이 보는 것은 유익해요:

foreign의 타입은 다음과 같아요:

foreign : (ffi : FFI)
       -> (fname : ffi_fn f)
       -> (ty : Type)
       -> {auto fty : FTy ffi [] ty}
       -> ty

여기서 중요한 인자는 묵시적 fty로, 주어진 타입이 FFI 설명 ffi에 따라 유효하다는 증명(FTy)을 포함해요:

data FTy : FFI -> List Type -> Type -> Type where
     FRet : ffi_types f t -> FTy f xs (IO' f t)
     FFun : ffi_types f s -> FTy f (s :: xs) t -> FTy f xs (s -> t)

이것이 FFI 기술자의 ffi_types 필드를 사용한다는 점을 주목하세요 — FRet와 FFun에 대한 이 인자들은 타입이 이 FFI에서 유효하다는 명시적 증명을 줘요. 예를 들어, 위의 do_fopen은 foreign의 fty 인자로 다음 묵시적 증명을 구축해요:

FFun C_Str (FFun C_Str (FRet C_Ptr))

외부 호출 컴파일 (Compiling foreign calls)

(이 섹션은 Idris 내부에 대한 어느 정도의 지식을 가정해요.)

백엔드를 작성할 때, 이제 우리는 foreign을 컴파일하는 방법을 알아야 해요. 여기서는 foreign 호출이 중간 표현(IR)에 도달하는 방법의 세부 사항은 건너뛸게요. 다만 prelude 패키지의 IO.idr을 보면 조금 더 자세히 볼 수 있어요 — foreign 호출은 기본 함수 mkForeignPrim으로 구현돼요. Lang.hs에 정의된 IR의 중요한 부분은 다음 생성자예요:

data LExp = ...
          | LForeign FDesc -- Function descriptor
                     FDesc -- Return type descriptor
                     [(FDesc, LExp)]

그래서 foreign 호출은 IR에서 LForeign 생성자로 나타나는데, 그것은 함수 기술자(FFI 기술자의 ffi_fn 필드로 주어진 타입의), 반환 타입 기술자(FTy의 응용으로 주어진), 그리고 타입 기술자를 가진 인자 목록(FTy의 응용으로도 주어진)을 받아요.

FDesc는 어떤 인자들에 대한 이름의 응용을 설명하며, 실제로는 LExp의 단순화된 부분 집합이에요:

data FDesc = FCon Name
           | FStr String
           | FUnknown
           | FApp Name [FDesc]

역함수화된, 단순화된, 그리고 바이트코드 형태 같은 더 낮은 수준의 IR에도 대응하는 구조가 있어요.

우리의 do_fopen 예시는 LExp 형태로 다음과 같이 도착해요:

LForeign (FStr "fileOpen") (FCon (sUN "C_Ptr"))
         [(FCon (sUN "C_Str"), f), (FCon (sUN "C_Str"), m)]

(f와 m이 인자들의 LExp 표현을 나타낸다고 가정해요.) 이 정보는 어떤 백엔드든 인자와 반환 값을 적절히 마샬링하기에 충분해야 해요.

주의: FDesc를 처리할 때, 지워지지 않은 묵시적 인자가 있을 수 있다는 점을 유의하세요. 예를 들어, C_IntT는 묵시적 인자 i를 가지므로 FDesc에서 FApp (sUN "C_IntT") [i, t] 형태의 무언가로 나타나는데, 여기서 i는 묵시적 인자(무시할 수 있음)이고 t는 정수 타입의 기술자예요. 실제로 이것이 어떻게 작동하는지 보려면 CodegenC.hs, 특히 toFType 함수를 보세요.

JavaScript FFI 기술자 (JavaScript FFI descriptor)

JavaScript FFI 기술자는 함수를 마샬링하는 것을 지원하기 때문에 조금 더 복잡해요. 그것은 다음과 같이 정의돼요:

mutual
  data JsFn t = MkJsFn t

  data JS_IntTypes  : Type -> Type where
       JS_IntChar   : JS_IntTypes Char
       JS_IntNative : JS_IntTypes Int

  data JS_FnTypes : Type -> Type where
       JS_Fn     : JS_Types s -> JS_FnTypes t -> JS_FnTypes (s -> t)
       JS_FnIO   : JS_Types t -> JS_FnTypes (IO' l t)
       JS_FnBase : JS_Types t -> JS_FnTypes t

  data JS_Types : Type -> Type where
       JS_Str   : JS_Types String
       JS_Float : JS_Types Double
       JS_Ptr   : JS_Types Ptr
       JS_Unit  : JS_Types ()
       JS_FnT   : JS_FnTypes a -> JS_Types (JsFn a)
       JS_IntT  : JS_IntTypes i -> JS_Types i

함수 타입을 JsFn으로 감싸는 이유는 FTy를 구축할 때 증명 검색(proof search)을 돕기 위한 것이에요. 우리는 결국 증명 검색을 개선하길 바라지만, 지금으로서는 인덱스들이 분리되어 있으면 훨씬 더 안정적으로 작동해요! 이것을 사용하는 예시는 IdrisScript에서 시간 제한(timeouts)을 설정할 때 나타나요:

setTimeout : (() -> JS_IO ()) -> (millis : Int) -> JS_IO Timeout
setTimeout f millis = do
  timeout <- jscall "setTimeout(%0, %1)"
                    (JsFn (() -> JS_IO ()) -> Int -> JS_IO Ptr)
                    (MkJsFn f) millis
  pure $ MkTimeout timeout

더 알아보기 (Learn more)

• Idris 참조 문서 목차