기타
기타 (Miscellaneous)
아직 분류하지 못했거나, 자신만의 페이지를 가질 만큼 작지 않은 것들에 대한 문서예요.
출처: 문서
본문
통일기 로그 (The Unifier Log)
통일기(unifier)가 어떤 것을 받아들이지 않는 이유를 디버깅하는 데 어려움이 있다면 (흔히 컴파일러 자체를 디버깅할 때), 문제의 표현식에 특별한 연산자 %unifyLog를 적용해보세요. 그러면 타입 검사기가 온갖 유익한 메시지를 뱉게 해요.
이름공간과 타입 지향 모호성 해소 (Namespaces and type-directed disambiguation)
이름은 분리된 이름공간(namespaces)에서 정의될 수 있고, 타입에 의해 모호성을 해소될 수 있어요. NAME EXPR 형태의 표현식은 표현식 EXPR에서 이름공간 NAME을 특권(privilege)으로 둬요. 예를 들어:
Idris> with List [[1,2],[3,4],[5,6]]
[[1, 2], [3, 4], [5, 6]] : List (List Integer)
Idris> with Vect [[1,2],[3,4],[5,6]]
[[1, 2], [3, 4], [5, 6]] : Vect 3 (Vect 2 Integer)
Idris> [[1,2],[3,4],[5,6]]
Can't disambiguate name: Prelude.List.::, Prelude.Stream.::, Prelude.Vect.::
대안 (Alternatives)
(| option1, option2, option3, ... |) 문법은 옵션들 중 하나가 작동할 때까지 각각을 차례로 타입 체킹해요. 이것은 예를 들어 정수 리터럴을 번역할 때 사용돼요.
Idris> the Nat (| "foo", Z, (-3) |)
0 : Nat
이것은 간단한 자동 증명을 제공하는 데도 사용할 수 있어요. 예를 들어, 증명의 일부 생성자를 시도해보는 것처럼.
syntax Trivial = (| Oh, Refl |)
전체성 검사 단언 (Totality checking assertions)
모든 정의는 커버리지(즉 모든 well-typed 응용이 처리됨)와, 종료(즉 모든 well-typed 응용이 결국 답을 생성함) 또는, codata를 반환할 경우 생산성(productivity, 실제로는 모든 재귀 호출이 생성자로 보호됨)에 대해 검사돼요.
당연히 종료 검사는 판정 불가능해요. 실제로 종료 검사기는 크기 변화(size change)를 찾아요 — 재귀 호출의 모든 순환은 감소하는 인자, 예를 들어 엄격히 양의(strongly positive) 데이터 타입의 재귀 인자를 가져야 해요.
전체성 검사기에 힌트를 주는 데 사용할 수 있는 내장 함수 두 개가 있어요:
assert_total x— 전체성 검사기가 알 수 없더라도 표현식x가 종료하고 커버함을 단언해요. 이것은 예를 들어x가 모든 입력을 커버하지 않는 함수를 사용하지만, 호출자가 특정 입력이 커버된다는 것을 알 때 사용할 수 있어요.assert_smaller p x— 표현식x가 패턴p보다 구조적으로 더 작음을 단언해요.
예를 들어, 다음 함수는 total로 검사되지 않아요:
qsort : Ord a => List a -> List a
qsort [] = []
qsort (x :: xs) = qsort (filter (<= x) xs) ++ (x :: qsort (filter (>= x) xs)))
이것은 검사기가 filter가 항상 qsort로의 재귀 호출에 대해 패턴 x :: xs보다 작은 값을 생성할 것인지 알 수 없기 때문이에요. 우리는 이것이 항상 사실일 것이라고 다음과 같이 단언할 수 있어요:
total
qsort : Ord a => List a -> List a
qsort [] = []
qsort (x :: xs) = qsort (assert_smaller (x :: xs) (filter (<= x) xs)) ++
(x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs))))
선순서 추론 (Preorder reasoning)
이 문법은 base 패키지의 Syntax.PreorderReasoning 모듈에 정의돼 있어요. 그것은 step과 qed라고 불리는 오버로드 가능한 함수들을 사용해 반사-전이 관계(reflexive-transitive relations)의 증명을 합성하는 문법을 제공해요. 이 모듈은 또한 동등성을 보여주기 위해 그 문법이 사용될 수 있게 하는 step과 qed 함수들을 정의해요.
다음은 예시예요:
import Syntax.PreorderReasoning
multThree : (a, b, c : Nat) -> a * b * c = c * a * b
multThree a b c =
(a * b * c) ={ sym (multAssociative a b c) }=
(a * (b * c)) ={ cong (multCommutative b c) }=
(a * (c * b)) ={ multAssociative a c b }=
(a * c * b) ={ cong {f = (* b)} (multCommutative a c) }=
(c * a * b) QED
괄호가 필요하다는 점을 주의하세요 — ={ }= 또는 QED의 왼쪽에는 단순 표현식(simple expression)만 올 수 있어요. 또한, 동등성에 대해 무언가를 증명하기 위해 선순서 추론 문법을 사용할 때, 하위 표현식이 아니라 전체 표현식만 관여시킬 수 있다는 점을 기억하세요. 이것은 가끔 cong의 사용을 요구할 수 있어요.
마지막으로, 동등성이 선순서 추론의 가장 명백한 응용이지만, 그것은 어떤 반사-전이 관계에도 사용될 수 있어요. step1 ={ just1 }= step2 ={ just2 }= end QED 같은 것은 (step step1 just1 (step step2 just2 (qed end)))로 번역되며, 정상적인 모호성 해소 과정을 통해 step과 qed의 적절한 정의를 선택해요. 예를 들어 표준 라이브러리는 동형사상(isomorphisms)에 대한 선순서 추론의 구현도 포함해요.
묵시적 인자에 대한 패턴 매칭 (Pattern matching on Implicit Arguments)
패턴 매칭은 묵시적 인자가 이름으로 참조될 때만 그 인자에 대해 허용돼요. 예를 들어:
foo : {n : Nat} -> Nat
foo {n = Z} = Z
foo {n = S k} = k
또는
foo : {n : Nat} -> Nat
foo {n = n} = n
후자는 다음과 같이 줄일 수 있어요:
foo : {n : Nat} -> Nat
foo {n} = n
즉, {x}는 {x=x}처럼 작동해요.
구현의 존재 (Existence of an implementation)
어떤 타입에 대해 어떤 인터페이스의 구현이 정의되었음을 보여주기 위해 %implementation 키워드를 사용할 수 있어요:
foo : Num Nat
foo = %implementation
'match' 응용 ('match' application)
ty <== name은 함수 name을 함수의 타입에 대해 ty를 매칭함으로써 그것이 타입 ty를 갖도록 적용해요. 이것은 증명에서 사용할 수 있어요. 예를 들어:
plus_comm : (n : Nat) -> (m : Nat) -> (n + m = m + n)
-- Base case
(Z + m = m + Z) <== plus_comm =
rewrite ((m + Z = m) <== plusZeroRightNeutral) ==>
(Z + m = m) in Refl
-- Step case
(S k + m = m + S k) <== plus_comm =
rewrite ((k + m = m + k) <== plus_comm) in
rewrite ((S (m + k) = m + S k) <== plusSuccRightSucc) in
Refl
반영 (Reflection)
%reflection 함수와 quoteGoal x by fn in t를 포함해요. quoteGoal x by fn in t는 현재 표현식의 예상 타입에 fn을 적용하고, 그 결과를 t를 정교화하면서 스코프 안에 있는 x에 넣어요.
Bash 완성 (Bash Completion)
optparse-applicative를 사용하면 Idris가 Bash 완성을 지원하게 돼요. 다음 명령으로 Idris의 완성 스크립트를 얻을 수 있어요:
idris --bash-completion-script `which idris`
현재 세션의 수명 동안 완성을 활성화하려면 다음 명령을 실행해요:
source <(idris --bash-completion-script `which idris`)
완성을 영구적으로 활성화하려면 다음 중 하나를 해야 해요:
- bash init 스크립트를 위 명령으로 수정한다.
- 완성 스크립트를 머신의 적절한
bash_completion.d/폴더에 추가한다.