외부 함수 인터페이스

외부 함수 인터페이스 (Foreign Function Interface)

• 컴파일러 프래그마 (Compiler Pragmas)
• Haskell FFI
• JavaScript FFI

컴파일러 프래그마 (Compiler Pragmas)

FFI에 사용되는 백엔드 일반적(backend-generic) 프래그마가 두 개 있어요:

{-# COMPILE <Backend> <Name> <Text> #-}
{-# FOREIGN <Backend> <Text> #-}

COMPILE 프래그마는 어떤 정보 <Text>를 같은 모듈에 정의된 이름 <Name>과 결부시키고, FOREIGN 프래그마는 <Text>를 현재 최상위 모듈과 결부시켜요. 이 정보는 컴파일 중에 특정 백엔드에 의해 해석돼요 (아래 참고). 이 프래그마들은 Agda 2.5.3에서 추가됐어요.

Haskell FFI

참고: 이 섹션은 GHC 백엔드에 적용돼요.

FOREIGN 프래그마 (The FOREIGN pragma)

GHC 백엔드는 FOREIGN 프래그마를 인라인 Haskell 코드로 해석하며, 컴파일된 모듈에 추가될 임의의 코드(import 문 포함)를 포함할 수 있어요. 예를 들어:

{-# FOREIGN GHC import Data.Maybe #-}

{-# FOREIGN GHC
  data Foo = Foo | Bar Foo

  countBars :: Foo -> Integer
  countBars Foo = 0
  countBars (Bar f) = 1 + countBars f
#-}

COMPILE 프래그마 (The COMPILE pragma)

GHC 백엔드가 인식하는 COMPILE 주석에는 네 가지 형태가 있어요:

{-# COMPILE GHC <Name> = <HaskellCode> #-}
{-# COMPILE GHC <Name> = type <HaskellType> #-}
{-# COMPILE GHC <Name> = data <HaskellData> (<HsCon1> | .. | <HsConN>) #-}
{-# COMPILE GHC <Name> as <HaskellName> #-}

처음 세 개는 주어진 Agda 정의를 어떻게 컴파일할지 컴파일러에게 알려주고, 마지막 것은 특정 Haskell 이름 아래에 Agda 정의를 노출시켜 Agda 라이브러리가 Haskell에서 사용될 수 있게 해요.

Agda에서 Haskell 타입 사용하기 (Using Haskell Types from Agda)

Agda에서 Haskell 함수를 사용하려면 그 타입이 Agda 타입에 매핑되어야 해요. 이 매핑은 COMPILE 프래그마의 type과 data 형태로 구성할 수 있어요.

불투명 타입 (Opaque types)

불투명 Haskell 타입은 Agda 타입을 postulate하고 그것을 COMPILE 프래그마의 type 형태로 Haskell 타입과 결부시켜 Agda에 노출돼요:

{-# FOREIGN GHC import qualified System.IO #-}

postulate FileHandle : Set
{-# COMPILE GHC FileHandle = type System.IO.Handle #-}

이것은 Agda 타입 FileHandle이 Haskell 타입 System.IO.Handle에 대응함을 컴파일러에게 알려주고, 파일 핸들을 사용하는 함수가 Agda에서 사용되게 해줘요.

데이터 타입 (Data types)

비-불투명 Haskell 데이터 타입은 COMPILE 프래그마의 data 형태로 Agda 데이터 타입에 매핑될 수 있어요:

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just    : A → Maybe A

{-# COMPILE GHC Maybe = data Maybe (Nothing | Just) #-}

컴파일러는 Agda 생성자의 타입이 대응하는 Haskell 생성자의 타입과 일치하는지, 그리고 어느 쪽에서도 생성자가 빠뜨려지지 않았는지 확인해요.

레코드 타입 (Record types)

COMPILE 프래그마의 data 형태는 Agda의 레코드 타입에서도 동작해요:

import Agda.Builtin.List
{-# FOREIGN GHC import Data.Tree #-}

record Tree (A : Set) : Set where
  inductive
  constructor node
  field root-label : A
  field sub-forest : Agda.Builtin.List.List (Tree A)

{-# COMPILE GHC Tree = data Tree (Node) #-}

내장 타입 (Built-in Types)

GHC 백엔드는 특정 Agda 내장 타입을 특수 Haskell 타입으로 컴파일해요. Agda 내장 타입과 Haskell 타입의 매핑은 다음과 같아요:

Agda 내장	Haskell 타입
NAT	Integer
INTEGER	Integer
STRING	Data.Text.Text
CHAR	Char
BOOL	Bool
FLOAT	Double

경고: Agda 자연수를 정수로 조작하는 Haskell 코드는 음수 값을 피하도록 주의해야 해요.

경고: Agda FLOAT 값은 하나의 논리적 NaN 값만 가져요. 런타임에는 여러 다른 NaN 표현이 존재할 수 있어요. 그러한 모든 NaN 값은 FFI 호출에 의해 동등하게 취급되어야 해요.

Agda에서 Haskell 함수 사용하기 (Using Haskell functions from Agda)

Haskell 타입과 Agda 타입 사이에 적절한 매핑이 설정되면, 타입이 Agda 타입에 매핑되는 Haskell 함수를 COMPILE 프래그마로 Agda 코드에 노출할 수 있어요:

open import Agda.Builtin.IO
open import Agda.Builtin.String
open import Agda.Builtin.Unit

{-# FOREIGN GHC
  import qualified Data.Text.IO as Text
  import qualified System.IO as IO
#-}

postulate
  stdout    : FileHandle
  hPutStrLn : FileHandle → String → IO ⊤
{-# COMPILE GHC stdout    = IO.stdout #-}
{-# COMPILE GHC hPutStrLn = Text.hPutStrLn #-}

컴파일러는 주어진 Haskell 코드의 타입이 Agda 함수의 타입과 일치하는지 확인해요. COMPILE 프래그마는 런타임 동작에만 영향을 준다는 점에 유의하세요 — 타입 체킹 시점에는 함수들이 postulate로 취급돼요.

경고: 정의된(비-postulate) Agda 함수에 Haskell 정의를 주는 것이 가능해요. 이 경우 Agda 정의는 타입 체킹 시점에 사용되고 Haskell 정의는 런타임에 사용돼요. 하지만 Agda 코드와 Haskell 코드가 동일하게 동작하는지 보장하는 검사는 없으며, 불일치는 정의되지 않은 동작으로 이어질 수 있어요. 이 기능은 Haskell 함수에 대한 호출을 포함하는 코드에 대해, 당신이 Haskell 코드 동작의 올바른 Agda 모델을 가지고 있다는 가정 아래 추론할 수 있게 해줘요.

Haskell에서 Agda 함수 사용하기 (Using Agda functions from Haskell)

Agda 2.3.4부터 Agda 함수는 COMPILE 프래그마의 as 형태로 Haskell 코드에 노출될 수 있어요:

module IdAgda where

  idAgda : ∀ {A : Set} → A → A
  idAgda x = x

  {-# COMPILE GHC idAgda as idAgdaFromHs #-}

이것은 Agda 함수 idAgda가 idAgdaFromHs라는 Haskell 함수로 컴파일되어야 함을 컴파일러에게 알려줘요. 이 프래그마가 없으면 함수는 예측할 수 없는 이름의 Haskell 함수로 컴파일되어서 Haskell에서 호출될 수 없어요. idAgdaFromHs의 타입은 idAgda의 번역된 타입이 될 거예요.

컴파일되고 내보내진 함수 idAgdaFromHs는 그런 다음 다음과 같이 Haskell에서 임포트하고 호출할 수 있어요:

-- 파일 UseIdAgda.hs
module UseIdAgda where

import MAlonzo.Code.IdAgda (idAgdaFromHs)
-- idAgdaFromHs :: () -> a -> a

idAgdaApplied :: a -> a
idAgdaApplied = idAgdaFromHs ()

다형 함수 (Polymorphic functions)

Agda는 단형(monomorphic) 언어이므로, 다형 함수는 타입을 인자로 취하는 함수로 모델링돼요. 이 인자들은 컴파일된 코드에도 존재하므로, 다형 Haskell 함수를 호출할 때 그것들을 명시적으로 버려야 해요. 예를 들어:

postulate
  ioReturn : {A : Set} → A → IO A

{-# COMPILE GHC ioReturn = \ _ x -> return x #-}

이 경우 컴파일된 ioReturn 호출은 여전히 A를 인자로 가지므로, 컴파일된 정의는 첫 번째 인자를 무시한 다음 다형 Haskell return 함수를 호출해요.

레벨 다형 타입 (Level-polymorphic types)

레벨 다형 타입은 다형 함수와 비슷한 문제에 직면해요. Haskell은 유니버스 레벨이 없으므로 Agda 타입은 대응하는 Haskell 타입보다 더 많은 인자를 가질 거예요. 이것은 적절한 수의 팬텀 인자를 가진 Haskell 타입 동의어를 정의하면 해결할 수 있어요. 예를 들어:

data Either {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  left  : A → Either A B
  right : B → Either A B

{-# FOREIGN GHC type AgdaEither a b = Either #-}
{-# COMPILE GHC Either = data AgdaEither (Left | Right) #-}

타입 클래스 제약 처리하기 (Handling typeclass constraints)

(현재) 타입 클래스 제약이 있는 Haskell 타입을 Agda 타입에 매핑하는 방법은 없어요. 이것은 클래스 제약이 있는 함수가 Agda에서 사용될 수 없음을 의미해요. 하지만 이것은 클래스 제약을 Haskell 데이터 타입에 감싸고 명시적 딕셔너리 전달을 사용하는 Haskell 함수를 제공하면 해결할 수 있어요.

예를 들어 Haskell에 간단한 GUI 라이브러리가 있다고 가정해 봐요:

module GUILib where
  class Widget w
  setVisible :: Widget w => w -> Bool -> IO ()

  data Window
  instance Widget Window
  newWindow :: IO Window

이 라이브러리를 Agda에서 사용하기 위해 먼저 위젯 딕셔너리의 Haskell 타입을 정의하고 이것을 Agda 타입 Widget에 매핑해요:

{-# FOREIGN GHC import GUILib #-}
{-# FOREIGN GHC data WidgetDict w = Widget w => WidgetDict #-}

postulate
  Widget : Set → Set
{-# COMPILE GHC Widget = type WidgetDict #-}

그런 다음 setVisible을 Widget 인스턴스 인자를 취하는 Agda 함수로 노출할 수 있어요:

postulate
  setVisible : {w : Set} {{_ : Widget w}} → w → Bool → IO ⊤
{-# COMPILE GHC setVisible = \ _ WidgetDict -> setVisible #-}

Agda Widget 인자가 Haskell 쪽의 WidgetDict 인자에 대응한다는 점에 유의하세요. Haskell 코드에서 WidgetDict 생성자에 매칭하면 묶인 딕셔너리가 setVisible 호출에 사용 가능해져요.

창 타입과 함수는 예상대로 매핑되고, Widget Window Haskell 인스턴스를 WidgetDict에 묶는 Agda 인스턴스도 추가해요:

postulate
  Window    : Set
  newWindow : IO Window
  instance WidgetWindow : Widget Window
{-# COMPILE GHC Window       = type Window #-}
{-# COMPILE GHC newWindow    = newWindow #-}
{-# COMPILE GHC WidgetWindow = WidgetDict #-}

그런 다음 다음과 같은 코드를 쓸 수 있어요:

openWindow : IO Window
openWindow = newWindow         >>= λ w →
             setVisible w true >>= λ _ →
             return w

JavaScript FFI

JavaScript 백엔드는 다음 형태의 COMPILE 프래그마를 인식해요:

{-# COMPILE JS <Name> = <JsCode> #-}

여기서 <Name>은 postulate, 생성자 또는 데이터 타입이에요. 데이터 타입의 코드는 패턴 매칭을 컴파일하는 데 사용되며, 데이터 타입의 값과 생성자 이름으로 인덱스된 함수(케이스 분기에 해당)의 테이블을 취하는 함수여야 해요. 예를 들어 이것은 List 타입의 컴파일된 코드로, 리스트를 JavaScript 배열로 컴파일해요:

data List {a} (A : Set a) : Set a where
  []  : List A
  _∷_ : (x : A) (xs : List A) → List A

{-# COMPILE JS List = function(x,v) {
    if (x.length < 1) {
      return v["[]"]();
    } else {
      return v["_∷_"](x[0], x.slice(1));
    }
  } #-}
{-# COMPILE JS []  = Array() #-}
{-# COMPILE JS _∷_ = function (x) { return function(y) { return [x].concat(y); }; } #-}

더 알아보기 (Learn more)

• Agda 문서: 외부 함수 인터페이스 원문