대화형 편집

대화형 편집 (Interactive Editing)

이제까지 우리는 Idris의 의존 타입 시스템이 함수의 타입에 의도된 동작을 더 정밀하게 기술함으로써 함수의 정확성에 대한 추가 확신을 줄 수 있는 여러 예를 봤어요. 타입 시스템이 프로그래머로 하여금 객체 언어의 타입 시스템을 기술하게 함으로써 EDSL 개발을 돕는 예도 봤어요. 그러나 정밀한 타입은 프로그램 검증 그 이상을 줘요 — 우리는 타입을 활용해 구조적으로 정확한(construct) 프로그램을 작성하도록 도울 수도 있어요.

Idris REPL은 타입에 기반해 프로그램의 부분을 검사·수정하는 여러 명령을 제공해요. 예를 들어 패턴 변수에 대한 케이스 분할(case splitting), 홀(hole)의 타입 검사, 기본적인 증명 탐색(proof search) 메커니즘 같은 것들이에요. 이 절에서 이러한 기능들이 텍스트 에디터에서 어떻게 활용될 수 있는지, 특히 Vim에서 어떻게 하는지 설명할게요. Emacs용 대화형 모드도 사용할 수 있어요.

REPL에서 편집하기 (Editing at the REPL)

REPL은 현재 로드된 모듈에 기반해 새 프로그램 조각을 생성하는 여러 명령을 제공해요. 이들은 일반적인 형태를 취해요:

:command [line number] [name]

즉, 각 명령은 특정 소스 줄의 특정 이름에 대해 작동하고 새 프로그램 조각을 출력해요. 각 명령에는 소스 파일을 제자리에서 갱신하는 대체 형태가 있어요:

:command! [line number] [name]

REPL이 로드되면, idris --client를 사용해 REPL 명령을 받고 응답하는 백그라운드 프로세스도 시작해요. 예를 들어 다른 곳에서 REPL이 실행 중이라면 다음과 같은 명령을 실행할 수 있어요:

$ idris --client ':t plus'
Prelude.Nat.plus : Nat -> Nat -> Nat
$ idris --client '2+2'
4 : Integer

텍스트 에디터는 이것을 편집 명령들과 함께 활용해 대화형 편집 지원을 제공할 수 있어요.

편집 명령 (Editing Commands)

:addclause

:addclause n f 명령 (약어 :ac n f)은 줄 n에 선언된 함수 f에 대한 템플릿 정의를 만들어요. 예를 들어 94번 줄부터 시작하는 코드가 다음과 같다면:

vzipWith : (a -> b -> c) ->
           Vect n a -> Vect n b -> Vect n c

:ac 94 vzipWith은 다음을 줄 거예요:

vzipWith f xs ys = ?vzipWith_rhs

이름은 프로그래머가 줄 수 있는 힌트(hints)에 따라 선택되고, 필요하면 숫자를 붙여 기계가 유일하게 만들어요. 힌트는 다음과 같이 줄 수 있어요:

%name Vect xs, ys, zs, ws

이것은 Vect 계열 타입에 대해 생성된 모든 이름이 xs, ys, zs, ws 순서로 선택되어야 함을 선언해요.

:casesplit

:casesplit n x 명령 (약어 :cs n x)은 줄 n의 패턴 변수 x를 취할 수 있는 다양한 패턴 형태로 분할하고, 통일(unification) 오류 때문에 불가능한 경우를 제거해요. 예를 들어 94번 줄부터 시작하는 코드가 다음과 같다면:

vzipWith : (a -> b -> c) ->
           Vect n a -> Vect n b -> Vect n c
vzipWith f xs ys = ?vzipWith_rhs

:cs 96 xs는 다음을 줄 거예요:

vzipWith f [] ys = ?vzipWith_rhs_1
vzipWith f (x :: xs) ys = ?vzipWith_rhs_2

즉, 패턴 변수 xs가 가능한 두 경우 []와 x :: xs로 분할됐어요. 다시 말하지만 이름은 같은 휴리스틱에 따라 선택돼요. 파일을 갱신하고(:cs! 사용) 같은 줄의 ys를 케이스 분할하면 다음을 얻어요:

vzipWith f [] [] = ?vzipWith_rhs_3

즉, 패턴 변수 ys가 한 경우 []로 분할됐어요. Idris가 다른 가능한 경우 y :: ys는 통일 오류를 초래한다는 것을 알아챘기 때문이에요.

:addmissing

:addmissing n f 명령 (약어 :am n f)은 줄 n의 함수 f가 모든 입력을 덮도록 요구되는 절(clauses)을 추가해요. 예를 들어 94번 줄부터 시작하는 코드가 다음과 같다면:

vzipWith : (a -> b -> c) ->
           Vect n a -> Vect n b -> Vect n c
vzipWith f [] [] = ?vzipWith_rhs_1

:am 96 vzipWith은 다음을 줘요:

vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_2

즉, 비어 있지 않은 벡터에 대한 경우가 없음을 알아차리고, 필요한 절들을 생성하며, 통일 오류로 이어질 절들을 제거해요.

:proofsearch

:proofsearch n f 명령 (약어 :ps n f)은 증명 탐색을 통해 줄 n의 홀 f에 대한 값을 찾으려 시도해요 — 지역 변수, 재귀 호출, 요구된 계열의 생성자에 대한 값을 시도해요. 선택적으로 증명 탐색을 해결하기 위해 적용할 수 있는 함수들인 힌트 목록을 취할 수 있어요. 예를 들어 94번 줄부터 시작하는 코드가 다음과 같다면:

vzipWith : (a -> b -> c) ->
           Vect n a -> Vect n b -> Vect n c
vzipWith f [] [] = ?vzipWith_rhs_1
vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_2

:ps 96 vzipWith_rhs_1은 다음을 줄 거예요:

[]

왜냐하면 길이 0의 Vect를 찾고 있는데, 빈 벡터가 유일한 가능성이기 때문이에요. 비슷하게, 그리고 어쩌면 놀랍게도, :ps 97 vzipWith_rhs_2를 풀려고 하면 가능성이 하나뿐이에요:

f x y :: (vzipWith f xs ys)

왜냐하면 vzipWith은 충분히 정밀한 타입을 갖기 때문이에요: 결과 벡터는 비어 있지 않아야 하고(a ::), 첫 원소는 타입 c여야 하며 얻는 유일한 방법은 f를 x와 y에 적용하는 것이고, 마지막으로 벡터의 꼬리는 재귀적으로만 만들 수 있어요.

:makewith

:makewith n f 명령 (약어 :mw n f)은 패턴 절에 with를 추가해요. 예를 들어 parity를 떠올려보세요. 10번 줄이 다음과 같다면:

parity (S k) = ?parity_rhs

:mw 10 parity는 다음을 줄 거예요:

parity (S k) with (_)
  parity (S k) | with_pat = ?parity_rhs

그런 다음 자리표시자 _를 parity k로 채우고 :cs 11 with_pat로 with_pat을 케이스 분할하면 다음 패턴들을 얻어요:

parity (S (plus n n)) | even = ?parity_rhs_1
parity (S (S (plus n n))) | odd = ?parity_rhs_2

여기서 케이스 분할이 패턴을 정규화했다는 점(+가 아니라 plus를 주는)을 유의하세요. 어쨌든, 대화형 편집을 사용하면 유효한 패턴이 정확히 무엇인지 프로그래머에게 보여줘 의존 패턴 매칭의 구현을 크게 단순화한다는 것을 볼 수 있어요.

Vim에서의 대화형 편집 (Interactive Editing in Vim)

Vim용 에디터 모드는 위에서 설명한 명령들을 사용해 문법 형광, 들여쓰기, 대화형 편집 지원을 제공해요.

대화형 편집은 다음과 같은 에디터 명령으로 이루어지며, 각각 버퍼를 직접 갱신해요:

  • \d — 현재 줄에 선언된 이름에 대한 템플릿 정의를 추가함 (:addclause 사용).

  • \c — 커서의 변수를 케이스 분할함 (:casesplit 사용).

  • \m — 커서의 이름에 대한 누락된 경우들을 추가함 (:addmissing 사용).

  • \w — with 절을 추가함 (:makewith 사용).

  • \o — 커서 아래의 홀을 풀기 위해 증명 탐색을 호출함 (:proofsearch 사용).

  • \p — 추가 힌트를 사용해 커서 아래의 홀을 풀기 위해 증명 탐색을 호출함 (:proofsearch 사용).

타입 검사기와 평가기를 호출하는 명령도 있어요:

  • \t — 커서 아래 (전역적으로 보이는) 이름의 타입을 표시함. 홀의 경우 컨텍스트와 기대 타입을 표시함.

  • \e — 평가할 식을 물어봄.

  • \r — 버퍼를 다시 로드하고 타입 검사함.

대응하는 명령이 Emacs 모드에서도 제공돼요. 다른 에디터에 대한 지원은 idris –client를 사용해 비교적 간단한 방식으로 추가할 수 있어요.

출처: 문서