Idris REPL

Idris에는 REPL이 함께 제공돼요.

출처: 문서

본문

평가 (Evaluation)

완전한 의존 타입 언어이기 때문에, Idris에는 사물을 평가하는 두 가지 단계가 있어요: 컴파일-타임과 런-타임. 컴파일-타임에는 타입 체킹을 판정 가능하게(decidable) 유지하기 위해 그것이 전체(total, 즉 종료하고 모든 가능한 입력을 커버하는)임을 아는 것만 평가해요. 컴파일-타임 평가기는 Idris 커널의 일부이며, 값의 HOAS(고차 추상 문법, higher order abstract syntax) 스타일 표현을 사용해 Haskell로 구현돼 있어요. 여기서 모든 것이 정규형(normal form)을 갖는 것으로 알려져 있으므로, 평가 전략은 실제로 중요하지 않아요. 어느 쪽이든 같은 답을 얻기 때문이에요. 실제로는 Haskell 런타임 시스템이 선택하는 대로 할 거예요.

REPL은 편의를 위해 컴파일-타임 평가 개념을 사용해요. (평가기를 사용할 수 있으므로) 구현하기 더 쉬울 뿐 아니라, 용어가 타입 검사기에서 어떻게 평가되는지 보여주는 데 매우 유용할 수 있어요. 그래서 다음의 차이를 볼 수 있어요:

Idris> \n, m => (S n) + m
\n => \m => S (plus n m) : Nat -> Nat -> Nat

Idris> \n, m => n + (S m)
\n => \m => plus n (S m) : Nat -> Nat -> Nat

사용자 지정 (Customisation)

Idris는 초기화 스크립트(initialisation scripts)를 지원해요.

초기화 스크립트 (Initialisation scripts)

Idris REPL이 시작하면, Idris의 애플리케이션 데이터 디렉터리에서 repl/init 파일을 열려고 시도해요. 애플리케이션 데이터 디렉터리는 Haskell 함수 호출 getAppUserDataDirectory "idris"의 결과인데, 대부분의 Unix 계열 시스템에서는 $HOME/.idris을 반환하고, 다양한 Windows 버전에서는 C:/Documents And Settings/user/Application Data/appName 같은 경로를 반환해요.

repl/init 파일은 개행으로 구분된 REPL 명령 목록이에요. 모든 명령이 초기화 스크립트에서 지원되는 것은 아니에요 — REPL의 정상 동작을 방해하지 않을 하위 집합만 지원돼요. 특히, 색상 설정, 묵시적 표시 같은 표시 옵션, 로그 수준이 지원돼요.

초기화 스크립트 예시 (Example initialisation script)

:colour prompt white italic bold
:colour implicit magenta italic

REPL 명령들 (The REPL Commands)

현재 지원되는 명령들의 집합은 다음과 같아요:

명령	인자	용도
`<expr>`		표현식을 평가
`:t :type`	`<expr>`	표현식의 타입을 검사
`:core`	`<expr>`	용어의 코어 언어 표현을 봄
`:miss :missing`	`<name>`	누락된 절들을 보여줌
`:doc`	`<name>`	내부 문서를 보여줌
`:mkdoc`	`<namespace>`	namespace(들)와 의존성에 대한 IdrisDoc 생성
`:apropos`	`[<package list>] <name>`	이름, 타입, 문서를 검색
`:s :search`	`[<package list>] <expr>`	타입으로 값을 검색
`:wc :whocalls`	`<name>`	어떤 이름의 호출자들을 나열
`:cw :callswho`	`<name>`	어떤 이름의 피호출자들을 나열
`:browse`	`<namespace>`	어떤 namespace의 내용을 나열
`:total`	`<name>`	이름의 전체성을 검사
`:r :reload`		현재 파일을 다시 로드
`:l :load`	`<filename>`	새 파일을 로드
`:cd`	`<filename>`	작업 디렉터리 변경
`:module`	`<module>`	추가 모듈을 임포트
`:e :edit`		`$EDITOR` 또는 `$VISUAL`을 사용해 현재 파일을 편집
`:m :metavars`		남은 증명 의무(holes)를 보여줌
`:p :prove`	`<hole>`	hole을 증명
`:a :addproof`	`<name>`	소스 파일에 증명을 추가
`:rmproof`	`<name>`	증명 스택에서 증명을 제거
`:showproof`	`<name>`	증명을 보여줌
`:proofs`		사용 가능한 증명들을 보여줌
`:x`	`<expr>`	인터프리터로 표현식에서 나오는 IO 액션들을 실행
`:c :compile`	`<filename>`	실행 파일로 컴파일 `[codegen] <filename>`
`:exec :execute`	`[<expr>]`	실행 파일로 컴파일하고 실행
`:dynamic`	`<filename>`	C 라이브러리를 동적으로 로드 (`%dynamic`과 유사)
`:dynamic`		동적으로 로드된 C 라이브러리들을 나열
`:? :h :help`		이 도움말 텍스트를 표시
`:set`	`<option>`	옵션 설정 (errorcontext, showimplicits, originalerrors, autosolve, nobanner, warnreach, evaltypes, desugarnats)
`:unset`	`<option>`	옵션 해제
`:color :colour`	`<option>`	REPL 색상을 켜거나 끔; 특정 색상을 설정
`:consolewidth`	`auto\|infinite\|<number>`	콘솔의 폭을 설정
`:printerdepth`	`<number-or-blank>`	최대 pretty-printing 깊이를 설정 (아무것도 지정하지 않으면 infinite)
`:q :quit`		Idris 시스템 종료
`:w :warranty`		보증 정보를 표시
`:let`	`(<top-level-declaration>)…`	함수 정의, 인스턴스 구현, fixity 선언 같은 선언을 평가
`:unlet :undefine`	`(<name>)…`	나열된 repl 정의들을 제거 (이름이 없으면 모든 repl 정의 제거)
`:printdef`	`<name>`	함수의 정의를 보여줌
`:pp :pprint`	`<option> <number> <name>`	Idris 함수를 LaTeX 또는 HTML로, 지정된 폭으로 pretty print

REPL 사용하기 (Using the REPL)

도움말 얻기 (Getting help)

:help 명령(또는 :h 또는 :?)은 사용 가능한 명령들의 짧은 요약을 출력해요.

Idris 종료 (Quitting Idris)

Idris에서 나가고 싶으면 간단히 :q 또는 :quit를 사용해요.

표현식 평가 (Evaluating expressions)

표현식을 평가하려면 그냥 입력하면 돼요. Idris가 타입을 추론할 수 없다면, Idris의 문법은 직접적인 타입 주석을 허용하지 않으므로, the 연산자를 사용해 수동으로 타입을 제공하는 것이 도움이 될 수 있어요. the의 예시는:

Idris> the Nat 4
4 : Nat
Idris> the Int 4
4 : Int
Idris> the (List Nat) [1,2]
[1,2] : List Nat
Idris> the (Vect _ Nat) [1,2]
[1,2] : Vect 2 Nat

이것은 표현식이 여전히 모호한 이름을 포함하는 경우에는 작동하지 않을 수 있어요. 이름은 with 키워드를 사용해 모호성을 해소할 수 있어요:

Idris> sum [1,2,3]
When elaborating an application of function Prelude.Foldable.sum:
        Can't disambiguate name: Prelude.List.::,
                                 Prelude.Stream.::,
                                 Prelude.Vect.::
Idris> with List sum [1,2,3]
6 : Integer

let 바인딩 추가 (Adding let bindings)

REPL에 let 바인딩을 추가하려면 :let을 사용해요. 아마 타입 주석도 제공해야 할 거예요. :let은 data 같은 다른 선언에서도 작동해요.

Idris> :let x : String; x = "hello"
Idris> x
"hello" : String
Idris> :let y = 10
Idris> y
10 : Integer
Idris> :let data Foo : Type where Bar : Foo
Idris> Bar
Bar : Foo

타입 정보 얻기 (Getting type information)

어떤 표현식의 타입을 Idris에 묻으려면 :t 명령을 사용해요. 또한 오버로드된 이름과 함께 사용하면, Idris는 모든 오버로딩과 그 타입을 제공해요. 중위 연산자의 타입을 묻으려면 그것을 괄호로 감싸요.

Idris> :t "foo"
"foo" : String
Idris> :t plus
Prelude.Nat.plus : Nat -> Nat -> Nat
Idris> :t (++)
Builtins.++ : String -> String -> String
Prelude.List.++ : (List a) -> (List a) -> List a
Prelude.Vect.++ : (Vect m a) -> (Vect n a) -> Vect (m + n) a
Idris> :t plus 4
plus (Builtins.fromInteger 4) : Nat -> Nat

:doc로 인터페이스에 대한 기본 정보를 요청할 수도 있어요:

Idris> :doc Monad
Interface Monad

Parameters:
    m

Methods:
    (>>=) : Monad m => m a -> (a -> m b) -> m b

        infixl 5

Instances:
    Monad id
    Monad PrimIO
    Monad IO
    Monad Maybe

...

다른 문서도 :doc에서 사용할 수 있어요:

Idris> :doc (+)
Prelude.Interfaces.(+) : Num ty => ty -> ty -> ty

infixl 8

The function is Total

Idris> :doc Vect
Data type Prelude.Vect.Vect : Nat -> Type -> Type

Arguments:
        Nat
        Type

Constructors:

Prelude.Vect.Nil : (a : Type) -> Vect 0 a


Prelude.Vect.:: : (a : Type) -> (n : Nat) -> a -> (Vect n a) -> Vect (S n) a

infixr 7

Arguments:
        a
        Vect n a

Idris> :doc Monad
Interface Monad

Parameters:
    m

Methods:
    (>>=) : Monad m => m a -> (a -> m b) -> m b
        Also called bind.
        infixl 5

        The function is Total
    join : Monad m => m (m a) -> m a
        Also called flatten or mu

        The function is Total
Implementations:
    Monad (IO' ffi)
    Monad Stream
    Monad Provider
    Monad Elab
    Monad PrimIO
    Monad Maybe
    Monad (Either e)
    Monad List

사물 찾기 (Finding things)

:apropos 명령은 어떤 문자열에 대해 이름, 타입, 문서를 검색하고 결과를 출력해요. 예를 들어:

Idris> :apropos eq
eqPtr : Ptr -> Ptr -> IO Bool


eqSucc : (left : Nat) -> (right : Nat) -> (left = right) -> S left = S right
S preserves equality

lemma_both_neq : ((x = x') -> _|_) -> ((y = y') -> _|_) -> ((x, y) = (x', y')) -> _|_


lemma_fst_neq_snd_eq : ((x = x') -> _|_) -> (y = y') -> ((x, y) = (x', y)) -> _|_


lemma_snd_neq : (x = x) -> ((y = y') -> _|_) -> ((x, y) = (x, y')) -> _|_


lemma_x_eq_xs_neq : (x = y) -> ((xs = ys) -> _|_) -> (x :: xs = y :: ys) -> _|_


lemma_x_neq_xs_eq : ((x = y) -> _|_) -> (xs = ys) -> (x :: xs = y :: ys) -> _|_


lemma_x_neq_xs_neq : ((x = y) -> _|_) -> ((xs = ys) -> _|_) -> (x :: xs = y :: ys) -> _|_


prim__eqB16 : Bits16 -> Bits16 -> Int

prim__eqB16x8 : Bits16x8 -> Bits16x8 -> Bits16x8

prim__eqB32 : Bits32 -> Bits32 -> Int

prim__eqB32x4 : Bits32x4 -> Bits32x4 -> Bits32x4

prim__eqB64 : Bits64 -> Bits64 -> Int

prim__eqB64x2 : Bits64x2 -> Bits64x2 -> Bits64x2

prim__eqB8 : Bits8 -> Bits8 -> Int

prim__eqB8x16 : Bits8x16 -> Bits8x16 -> Bits8x16

prim__eqBigInt : Integer -> Integer -> Int

prim__eqChar : Char -> Char -> Int

prim__eqFloat : Double -> Double -> Int

prim__eqInt : Int -> Int -> Int

prim__eqString : String -> String -> Int

prim__syntactic_eq : (a : Type) -> (b : Type) -> (x : a) -> (y : b) -> Maybe (x = y)

sequence : Traversable t => Applicative f => (t (f a)) -> f (t a)


sequence_ : Foldable t => Applicative f => (t (f a)) -> f ()


Eq : Type -> Type
The Eq interface defines inequality and equality.

GTE : Nat -> Nat -> Type
Greater than or equal to

LTE : Nat -> Nat -> Type
Proofs that n is less than or equal to m

gte : Nat -> Nat -> Bool
Boolean test than one Nat is greater than or equal to another

lte : Nat -> Nat -> Bool
Boolean test than one Nat is less than or equal to another

ord : Char -> Int
Convert the number to its ASCII equivalent.

replace : (x = y) -> (P x) -> P y
Perform substitution in a term according to some equality.

sym : (l = r) -> r = l
Symmetry of propositional equality

trans : (a = b) -> (b = c) -> a = c
Transitivity of propositional equality

:search는 Hoogle의 정신에 입각한 타입 기반 검색을 해요. 자세한 내용은 타입 지향 검색(:search)에서 볼 수 있어요. 다음은 예시예요:

Idris> :search a -> b -> a
= Prelude.Basics.const : a -> b -> a
Constant function. Ignores its second argument.

= assert_smaller : a -> b -> b
Assert to the totality checker than y is always structurally
smaller than x (which is typically a pattern argument)

> malloc : Int -> a -> a


> Prelude.pow : Num a => a -> Nat -> a


> Prelude.Interfaces.(*) : Num a => a -> a -> a


> Prelude.Interfaces.(+) : Num a => a -> a -> a
... (More results)

:search는 의존 타입도 찾을 수 있어요:

Idris> :search plus (S n) n = plus n (S n)
< Prelude.Nat.plusSuccRightSucc : (left : Nat) ->
                                  (right : Nat) ->
                                  S (left + right) = left + S right

Idris 코드 로드와 재로드 (Loading and reloading Idris code)

:l File.idr 명령은 현재 실행 중인 REPL에 File.idr을 로드하고, :r은 마지막으로 로드된 파일을 다시 로드해요.

전체성 (Totality)

모든 Idris 정의는 전체성에 대해 검사돼요. :total <NAME> 명령은 그 검사의 결과를 표시해요. 정의가 total이 아니면, 그것은 불완전한 패턴 매칭 때문일 수 있어요. 그렇다면 :missing 또는 :miss가 누락된 case들을 표시해요.

파일 편집 (Editing files)

:e 명령은 현재 모듈에서 기본 편집기를 실행해요. 제어가 Idris로 돌아온 후 파일이 다시 로드돼요.

컴파일러 호출 (Invoking the compiler)

현재 모듈은 :c <FILENAME> 또는 :compile <FILENAME> 명령을 사용해 실행 파일로 컴파일될 수 있어요. 이 명령은 codegen을 지정할 수 있게 해주므로, 예를 들어 :c javascript <FILENAME>으로 JavaScript를 생성할 수 있어요. :exec 명령은 프로그램을 임시 파일로 컴파일하고 결과 실행 파일을 실행해요.

IO 액션 (IO actions)

GHCI와 달리, Idris REPL은 묵시적 IO 모나드 안에 있지 않아요. 즉, IO 액션을 실행하려면 특별한 명령을 사용해야 해요. :x tm은 Idris 인터프리터에서 IO 액션 tm을 실행해요.

C 라이브러리 동적 로드 (Dynamically loading C libraries)

때때로 Idris 프로그램은 C로 작성된 외부 라이브러리에 의존할 수 있어요. Idris 인터프리터에서 이 라이브러리들을 사용하려면 먼저 동적으로 로드되어야 해요. 이것은 Idris 소스 파일의 %dynamic <LIB> 지시어나 REPL의 :dynamic <LIB> 명령을 통해 달성돼요. 현재 동적으로 로드된 라이브러리들의 집합은 인자 없이 :dynamic을 실행해서 볼 수 있어요. 이 라이브러리들은 타입 프로바이더와 :exec에서 Idris FFI를 통해 사용할 수 있어요.

색상 (Colours)

Idris 용어는 놀라운 색상으로 제공돼요! 기본적으로 Idris REPL은 색상을 사용해 데이터 생성자, 타입 또는 타입 생성자, 연산자, 묶인 변수(bound variables), 묵시적 인자를 구분해요. 이 기능은 모든 POSIX 계열 시스템에서 사용할 수 있으며, Windows에서도 작동하게 하려는 계획이 있어요.

기본 색상이 마음에 들지 않으면 다음과 같은 명령으로 끌 수 있어요.

:colour off

그리고, 지루함이 찾아오면 다음 명령으로 다시 켤 수 있어요.

:colour on

색상을 수정하려면 다음 명령을 사용해요.

:colour <CATEGORY> <OPTIONS>

여기서 <CATEGORY>는 keyword, boundvar, implicit, function, type, data, 또는 prompt 중 하나이고, <OPTIONS>는 색상들과 글꼴 옵션들에서 빼낸 공백-구분 목록이에요. 사용 가능한 색상은 default, black, yellow, cyan, red, blue, white, green, magenta이에요. 두 개 이상의 색상이 지정되면, 마지막 것이 우선해요. 사용 가능한 옵션은 dull과 vivid, bold와 nobold, italic과 noitalic, underline과 nounderline으로, 반대말 쌍을 이뤄요. 색상 default는 터미널의 기본 색상을 말해요.

시작 시 사용되는 색상은 REPL 초기화 스크립트로 변경할 수 있어요.

색상은 --nocolour 커맨드라인 옵션으로 시작 시 비활성화할 수 있어요.

더 알아보기 (Learn more)

Idris 참조 문서 목차