여러 가지

여러 가지 (Miscellany)

이 절에서는 다양한 추가 기능을 논의해요:

  • auto, implicit, default 인자;

  • 리터레이트 프로그래밍(literate programming);

  • 외부 함수 인터페이스를 통한 외부 라이브러리와의 인터페이싱;

  • 인터페이스;

  • 타입 제공자(type providers);

  • 코드 생성; 그리고

  • 우주 계층(universe hierarchy).

출처: 문서

본문

묵시적 인자 (Implicit arguments)

우리는 이미 묵시적 인자를 봤어요. 이는 타입 검사기가 추론할 수 있을 때 인자를 생략할 수 있게 해줘요. 예:

index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a

자동 묵시적 인자 (Auto implicit arguments)

다른 상황에서는 타입 검사로가 아니라 컨텍스트에서 적절한 값을 검색하거나, 증명을 구성함으로써 인자를 추론하는 것이 가능할 수 있어요. 예를 들어 리스트가 비어 있지 않다는 증명을 요구하는 다음 head 정의가 있어요:

isCons : List a -> Bool
isCons [] = False
isCons (x :: xs) = True

head : (xs : List a) -> (isCons xs = True) -> a
head (x :: xs) _ = x

리스트가 그 값이 알려져 있거나 컨텍스트에 이미 증명이 존재해 정적으로 비어 있지 않은 것으로 알려져 있다면, 그 증명은 자동으로 구성될 수 있어요. 자동 묵시적 인자는 이것이 조용히 일어나게 해요. head를 다음과 같이 정의해요:

head : (xs : List a) -> {auto p : isCons xs = True} -> a
head (x :: xs) = x

묵시적 인자의 auto 주석은 Idris가 적절한 타입의 값을 검색해 묵시적 인자를 채우려 시도할 것임을 의미해요. 다음을 순서대로 시도할 거예요:

  • 정확히 올바른 타입의 지역 변수, 즉 패턴 매치나 let 바인딩에서 묶인 이름들.

  • 요구되는 타입의 생성자들. 그것들이 인자를 갖는다면 최대 깊이 100까지 재귀적으로 검색함.

  • 함수 타입을 가진 지역 변수들, 인자들을 재귀적으로 검색함.

  • %hint 주석으로 표시된 적절한 반환 타입의 어떤 함수든.

증명이 발견되지 않는 경우, 일반적인 방식으로 명시적으로 제공될 수 있어요:

head xs {p = ?headProof}

기본 묵시적 인자 (Default implicit arguments)

Idris가 주어진 타입의 값을 자동으로 찾게 하는 것 외에도, 때로는 특정 기본 값을 가진 묵시적 인자를 갖고 싶을 때가 있어요. Idris에서는 default 주석을 사용해 이렇게 할 수 있어요. 이것은 주로 auto가 실패하거나 도움이 안 되는 값을 찾을 때 자동으로 증명을 구성하는 것을 돕기 위한 것이지만, 증명을 포함하지 않는 더 단순한 경우를 먼저 고려하는 것이 더 쉬울 수 있어요.

n번째 피보나치 수를 계산하고 싶다면 (0번째 피보나치 수를 0으로 정의하며), 다음과 같이 작성할 수 있어요:

fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat
fibonacci {lag} Z = lag
fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n

이 정의 후에, fibonacci 5는 fibonacci {lag=0} {lead=1} 5와 동등하며, 5번째 피보나치 수를 반환해요. 이것이 작동하긴 하지만 default 주석의 의도된 용도가 아니라는 점을 유의하세요. 이것은 설명 목적으로만 여기 포함됐어요. 보통 default는 커스텀 증명 탐색 스크립트 같은 것을 제공하는 데 사용돼요.

묵시적 변환 (Implicit conversions)

Idris는 묵시적 변환의 생성을 지원해요. 이는 용어를 타입적으로 올바르게 만드는 데 필요할 때 값을 한 타입에서 다른 타입으로 자동 변환할 수 있게 해줘요. 이는 편의를 높이고 장황함을 줄이기 위한 것이에요. 인위적이지만 단순한 예는 다음과 같아요:

implicit intString : Int -> String
intString = show

test : Int -> String
test x = "Number " ++ x

일반적으로 Int를 String에 붙일 수는 없지만, 묵시적 변환 함수 intString이 x를 String으로 변환할 수 있으므로 test의 정의는 타입적으로 올바르게 돼요. 묵시적 변환은 다른 함수처럼 구현되지만 implicit 수정자가 주어지고, 하나의 명시적 인자로 제한돼요.

한 번에 하나의 묵시적 변환만 적용될 거예요. 즉, 묵시적 변환은 연결(chain)될 수 없어요. 하지만 위와 같은 단순 타입의 묵시적 변환은 권장되지 않아요! 더 흔하게, 묵시적 변환은 임베디드 도메인 특화 언어에서 장황함을 줄이거나 증명의 세부 사항을 숨기는 데 사용될 거예요. 그런 예는 이 튜토리얼의 범위를 넘어요.

리터레이트 프로그래밍 (Literate programming)

Haskell처럼 Idris는 리터레이트 프로그래밍을 지원해요. 파일에 .lidr 확장자가 있으면 리터레이트 파일로 가정돼요. 리터레이트 프로그램에서, 줄이 큰 따옴표보다 큰 기호 >로 시작하지 않는 한 모든 것이 주석으로 가정돼요. 예를 들어:

> module literate

This is a comment. The main program is below

> main : IO ()
> main = putStrLn "Hello literate world!\n"

추가 제한이 있는데, 프로그램 줄(>로 시작하는)과 주석 줄(다른 문자로 시작하는) 사이에는 반드시 빈 줄이 있어야 해요.

외부 함수 호출 (Foreign function calls)

실용적인 프로그래밍을 위해, 특히 운영 체제, 파일 시스템, 네트워킹 등과 인터페이싱할 때 외부 라이브러리를 사용할 수 있어야 하는 경우가 종종 있어요. Idris는 이를 위해 프렐류드의 일부로 가벼운 외부 함수 인터페이스(foreign function interface)를 제공해요. 이를 위해 C와 gcc 컴파일러에 대한 어느 정도의 지식을 가정해요. 먼저, 처리할 수 있는 외부 타입을 기술하는 데이터 타입을 정의해요:

data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit

이 각각은 C 타입에 직접 대응해요. 각각: int, double, char, char*, void*, void. 구체적인 Idris 타입으로의 번역도 있으며, 다음 함수로 기술돼요:

interpFTy : FTy -> Type
interpFTy FInt    = Int
interpFTy FFloat  = Double
interpFTy FChar   = Char
interpFTy FString = String
interpFTy FPtr    = Ptr
interpFTy FUnit   = ()

외부 함수는 입력 타입 목록과 반환 타입으로 기술되며, 이는 Idris 타입으로 변환될 수 있어요:

ForeignTy : (xs:List FTy) -> (t:FTy) -> Type

외부 함수는 불순(impure)하다고 가정되므로, ForeignTy는 IO 타입을 만들어요. 예를 들어:

Idris> ForeignTy [FInt, FString] FString
Int -> String -> IO String : Type

Idris> ForeignTy [FInt, FString] FUnit
Int -> String -> IO () : Type

함수의 이름, 인자 타입 목록, 반환 타입을 줘 외부 함수에 대한 호출을 만들어요. 내장 구성물 mkForeign는 이 설명을 Idris가 호출할 수 있는 함수로 변환해요:

data Foreign : Type -> Type where
    FFun : String -> (xs:List FTy) -> (t:FTy) ->
           Foreign (ForeignTy xs t)

mkForeign : Foreign x -> x

컴파일러가 완전한 외부 함수 호출을 만들기 위해 mkForeign가 완전히 적용되기를 기대한다는 점을 유의하세요. 예를 들어 putStr 함수는 런타임 시스템에 정의된 외부 함수 putStr에 대한 호출로 다음과 같이 구현돼요:

putStr : String -> IO ()
putStr x = mkForeign (FFun "putStr" [FString] FUnit) x

include와 linker 지시어 (Include and linker directives)

외부 함수 호출은 Idris 값 표현과 C 표현 사이의 적절한 변환과 함께 C 함수에 대한 호출로 직접 번역돼요. 종종 이것은 추가 라이브러리를 링크하거나, 추가 헤더·객체 파일이 필요하게 돼요. 이것은 다음 지시어를 통해 가능해요:

  • %lib target x — libx 라이브러리를 포함함. target이 C라면 이는 gcc에 -lx 옵션을 전달하는 것과 동등. target이 Java라면 라이브러리는 maven을 위한 groupId:artifactId:packaging:version 종속성 좌표로 해석될 거임.

  • %include target x — 주어진 백엔드 target에 대해 헤더 파일을 사용하거나 x를 import함.

  • %link target x.o — 주어진 백엔드 target을 사용할 때 객체 파일 x.o와 링크함.

  • %dynamic x.so — 공유 객체 x.so로 인터프리터를 동적으로 링크함.

외부 함수 호출 테스트하기 (Testing foreign function calls)

보통 Idris 인터프리터(타입 검사와 REPL에 사용되는)는 IO 동작을 수행하지 않아요. 게다가 C 코드를 생성하지도 기계 코드로 컴파일하지도 않으므로, %lib, %include, %link 지시어는 효과가 없어요. IO 동작과 FFI 호출은 특수 REPL 명령 :x EXPR으로 테스트할 수 있고, C 라이브러리는 :dynamic 명령이나 %dynamic 지시어를 사용해 인터프리터에서 동적으로 로드될 수 있어요. 예를 들어:

Idris> :dynamic libm.so
Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)
0.9995736030415051 : Double

타입 제공자 (Type Providers)

F#의 타입 제공자에서 영감을 받은 Idris 타입 제공자는, 우리의 타입이 Idris 밖의 세계에 있는 "무언가에 관한 것"이 되게 하는 수단이에요. 예를 들어, 데이터베이스 스키마를 나타내는 타입과 그것에 대해 검사되는 쿼리가 주어졌을 때, 타입 제공자는 타입 검사 중에 실제 데이터베이스의 스키마를 읽을 수 있어요.

Idris 타입 제공자는 Idris의 일반적인 실행 의미론을 사용해 IO 동작을 실행하고 결과를 추출해요. 이 결과는 컴파일된 코드의 상수로 저장돼요. 그것은 타입일 수 있으며, 그 경우 다른 타입처럼 사용돼요. 또는 값일 수 있으며, 그 경우 타입의 인덱스로 포함해 다른 값처럼 사용될 수 있어요.

타입 제공자는 아직 실험적인 확장이에요. 확장을 활성화하려면 %language 지시어를 사용해요:

%language TypeProviders

어떤 타입 t에 대한 제공자 p는 단순히 타입 IO (Provider t)의 식이에요. %provide 지시어는 타입 검사기가 동작을 실행하고 결과를 이름에 묶게 해요. 이것은 아마 간단한 예로 가장 잘 설명될 거예요. 타입 제공자 fromFile은 텍스트 파일을 읽어요. 파일이 문자열 Int로 구성되어 있으면 타입 Int가 제공될 거예요. 그렇지 않으면 타입 Nat를 제공할 거예요.

strToType : String -> Type
strToType "Int" = Int
strToType _ = Nat

fromFile : String -> IO (Provider Type)
fromFile fname = do Right str <- readFile fname
                      | Left err => pure (Provide Void)
                    pure (Provide (strToType (trim str)))

그 다음 %provide 지시어를 사용해요:

%provide (T1 : Type) with fromFile "theType"

foo : T1
foo = 2

theType이라는 파일이 단어 Int로 구성되어 있다면 foo는 Int가 될 거예요. 그렇지 않으면 Nat가 될 거예요. Idris가 지시어를 만나면, 먼저 제공자 식 fromFile theType이 타입 IO (Provider Type)을 갖는지 검사해요. 다음으로 제공자를 실행해요. 결과가 Provide t이면 T1이 t로 정의돼요. 그렇지 않으면 그 결과는 오류예요.

우리의 데이터 타입 Provider t는 다음 정의를 가져요:

data Provider a = Error String
                | Provide a

우리는 이미 Provide 생성자를 봤어요. Error 생성자는 타입 제공자가 유용한 오류 메시지를 반환하게 해줘요. 이 절의 예는 의도적으로 단순했어요. 정적으로 검사되는 SQLite 바인딩을 포함한 더 복잡한 타입 제공자 구현은 외부 컬렉션 [1]에서 구할 수 있어요.

C 타겟 (C Target)

Idris의 기본 타겟은 C예요. 컴파일:

$ idris hello.idr -o hello

는 다음과 동등해요:

$ idris --codegen C hello.idr -o hello

위 명령을 사용하면 임시 C 소스가 생성되고, 그것이 hello라는 실행 파일로 컴파일돼요.

생성된 C 코드를 보려면 다음으로 컴파일해요:

$ idris hello.idr -S -o hello.c

최적화를 켜려면 아래와 같이 코드 안에서 %flag C 프라그마를 사용해요:

module Main
%flag C "-O3"

factorial : Int -> Int
factorial 0 = 1
factorial n = n * (factorial (n-1))

main : IO ()
main = do
     putStrLn $ show $ factorial 3

생성된 C를 디버깅 정보로 컴파일하려면, 예를 들어 gdb를 사용해 Idris 프로그램의 세그멘테이션 결함을 디버깅하려면, %flag C 프라그마를 사용해 디버깅 기호를 포함해요:

%flag C "-g"

JavaScript 타겟 (JavaScript Target)

Idris는 브라우저에서와 NodeJS 환경 등에서 실행될 수 있는 JavaScript 코드를 만들 수 있어요. FFI를 사용해 JavaScript 생태계와 통신할 수 있어요.

코드 생성 (Code Generation)

코드 생성은 두 개의 별도 타겟으로 나뉘어요. 브라우저에서 실행되도록 맞춰진 코드를 생성하려면 다음 명령을 발행해요:

$ idris --codegen javascript hello.idr -o hello.js

결과 파일은 다른 JavaScript 코드처럼 HTML에 임베드될 수 있어요.

NodeJS용 코드 생성은 약간 달라요. Idris는 node로 직접 실행될 수 있는 JavaScript 파일을 출력해요.

$ idris --codegen node hello.idr -o hello
$ ./hello
Hello world

JavaScript 코드 생성기가 console.log를 사용해 stdout에 텍스트를 쓴다는 점을 고려하세요. 즉 각 문자열 끝에 자동으로 새 줄을 추가한다는 뜻이에요. 이 동작은 NodeJS 코드 생성기에서는 나타나지 않아요.

FFI 사용하기 (Using the FFI)

유용한 애플리케이션을 작성하려면 외부 세계와 통신해야 해요. DOM을 조작하고 싶을 수도, Ajax 요청을 보내고 싶을 수도 있어요. 이 작업에는 FFI를 사용할 수 있어요. 대부분의 JavaScript API가 콜백을 요구하므로, 인자로 함수를 전달할 수 있도록 FFI를 확장해야 해요.

JavaScript FFI는 일반 FFI와 약간 다르게 작동해요. 그것은 위치 인자(positional arguments)를 사용해 우리의 인자를 JavaScript 코드 조각에 직접 삽입해요.

다음처럼 JavaScript의 원시 덧셈을 사용할 수 있어요:

module Main

primPlus : Int -> Int -> IO Int
primPlus a b = mkForeign (FFun "%0 + %1" [FInt, FInt] FInt) a b

main : IO ()
main = do
  a <- primPlus 1 1
  b <- primPlus 1 2
  print (a, b)

%n 표기법이 0부터 시작해 우리 외부 함수에 주어진 n번째 인자의 위치를 한정한다는 점을 유의하세요. 위치보다는 퍼센트 기호가 필요하면 단순히 %%를 사용해요.

함수를 외부 함수에 전달하는 것은 매우 비슷해요. JavaScript 세계에서 다음 함수를 호출하고 싶다고 가정해보세요:

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

분명히 여기서 함수 f를 전달해야 해요 (우리는 twice에서 f를 사용하는 방식에서 그것을 추론할 수 있어요. JavaScript에 타입이 있었다면 더 분명할 거예요).

JavaScript FFI는 FFunction 타입의 무언가를 주면 인자로서의 함수를 이해할 수 있어요. 다음 예제 코드는 twice를 JavaScript에서 호출하고 결과를 우리 Idris 프로그램에 반환해요:

module Main

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

main : IO ()
main = do
  a <- twice (+1) 1
  print a

프로그램은 우리가 기대한 대로 3을 출력해요.

외부 JavaScript 파일 포함하기 (Including external JavaScript files)

JavaScript로 작업할 때 외부 라이브러리나, FFI를 통해 호출하고 싶은 몇몇 함수들을 — 그것들이 외부 파일에 저장되어 있든 — 포함하고 싶을 수 있어요. JavaScript와 NodeJS 코드 생성기는 %include 지시어를 이해해요. JavaScript와 NodeJS가 다른 코드 생성기로 처리되므로, 어느 것을 타겟팅할지 명시해야 한다는 것을 유의하세요. 이것은 같은 Idris 소스 파일에서 JavaScript와 NodeJS에 다른 파일들을 포함할 수 있다는 뜻이에요.

외부 JavaScript 파일을 추가하고 싶을 때마다 다음과 같이 할 수 있어요:

NodeJS의 경우:

%include Node "path/to/external.js"

브라우저에서 사용하는 경우:

%include JavaScript "path/to/external.js"

주어진 파일들은 생성된 코드의 맨 위에 추가될 거예요.

라이브러리 패키지의 경우 ipkg objs 옵션을 사용해 설치에 js 파일을 포함하고 다음을 사용할 수도 있어요:

%include Node "package/external.js"

Idris의 JavaScript와 NodeJS 백엔드는 그 위치에서도 파일을 찾아볼 거예요.

NodeJS 모듈 포함하기 (Including NodeJS modules)

NodeJS 코드 생성기는 %lib 지시어로 모듈도 포함할 수 있어요.

%lib Node "fs"

이 지시어는 다음 JavaScript로 컴파일돼요:

var fs = require("fs");

생성된 JavaScript 줄이기 (Shrinking down generated JavaScript)

Idris는 매우 큰 JavaScript 코드 덩어리를 만들 수 있어요. 하지만 생성된 코드는 Google의 closure-compiler를 사용해 축소(minify)될 수 있어요. 다른 축소기도 적합하지만 closure-compiler는 공격적인 인라인과 코드 제거를 수행하는 고급 컴파일을 제공해요. Idris는 이 컴파일 모드를 완전히 활용할 수 있으며, Idris로 작성된 JavaScript 애플리케이션을 배포할 때 그것을 사용하는 것이 매우 권장돼요.

축적성 (Cumulativity)

값이 타입에 나타날 수 있고 그 반대도 가능하므로, 타입 자체가 타입을 갖는 것은 자연스러워요. 예를 들어:

*universe> :t Nat
Nat : Type
*universe> :t Vect
Vect : Nat -> Type -> Type

하지만 Type의 타입은 무엇일까요? Idris에 물어보면 보고해요:

*universe> :t Type
Type : Type 1

Type이 자신의 타입이라면, Girard의 역설(Girard's paradox) 때문에 불일치로 이어질 거예요. 그래서 내부적으로는 타입(또는 우주)의 계층이 있어요:

Type : Type 1 : Type 2 : Type 3 : ...

우주는 축적적(cumulative)이에요. 즉 x : Type n이면, n < m인 한 x : Type m도 가질 수 있어요. 타입 검사기는 이런 우주 제약을 생성하고 불일치가 발견되면 오류를 보고해요. 보통 프로그래머는 이것을 걱정할 필요가 없지만, 그것은 다음 같은 (인위적인) 프로그램을 막아요:

myid : (a : Type) -> a -> a
myid _ x = x

idid :  (a : Type) -> a -> a
idid = myid _ myid

myid를 자신에게 적용하면 우주 계층에 순환이 생겨요 — myid의 첫 인자는 Type인데, 자신에게 적용되면 요구되는 것보다 더 낮은 수준에 있을 수 없어요.

[1]

https://github.com/david-christiansen/idris-type-providers

더 알아보기 (Learn more)