암시 인자
암시 인자 (Implicit Arguments)
타입 체커가 스스로 알아낼 수 있는 항은 밑줄(_)로 대체해 생략할 수 있어요.
타입 체커가 _의 값을 추론하지 못하면 오류를 보고해요.
예를 들어 다형적 항등 함수에 대해
id : (A : Set) → A → A
첫 번째 인자는 두 번째 인자의 타입으로부터 추론될 수 있어서, 항등 함수를 zero에 적용한 것을 id _ zero로 쓸 수 있어요.
심지어 첫 번째 인자 없이 이 함수 적용을 쓸 수도 있어요. 그런 경우 암시적 함수 공간(implicit function space)을 선언해요:
id : {A : Set} → A → A
그러면 id zero 표기법을 사용할 수 있어요.
또 다른 예:
_==_ : {A : Set} → A → A → Set
subst : {A : Set} (C : A → Set) {x y : A} → x == y → C x → C y
_==_의 첫 번째 인자가 암시적으로 남겨진 방식에 주의하세요. 비슷하게 subst의 적용에서 암시 인자 A, x, y를 생략할 수 있어요.
암시 인자를 명시적으로 주려면 중괄호로 감싸면 돼요. 다음 두 표현식은 동등해요:
x1 = subst C eq cx
x2 = subst {_} C {_} {_} eq cx
암시 인자가 타입에서 요구된다면 적용의 끝에도 삽입된다는 점을 주목할 가치가 있어요.
예를 들어 다음에서 y1과 y2는 동등해요.
y1 : a == b → C a → C b
y1 = subst C
y2 : a == b → C a → C b
y2 = subst C {_} {_}
암시 인자는 왼쪽 변에서 적극적으로 삽입되므로 y3과 y4는 동등해요. 예외는 타입 시그니처가 주어지지 않을 때인데, 그 경우 암시 인자 삽입이 일어나지 않아요. 따라서 y5의 정의에서 유일한 암시는 subst의 A 인자예요.
y3 : {x y : A} → x == y → C x → C y
y3 = subst C
y4 : {x y : A} → x == y → C x → C y
y4 {x} {y} = subst C {_} {_}
y5 = subst C
암시 인자를 가진 람다 추상화를 쓰는 것도 가능해요. 예를 들어 id : (A : Set) → A → A가 주어지면, 암시 타입 인자를 가진 항등 함수를 다음과 같이 정의할 수 있어요:
id’ = λ {A} → id A
암시 인자는 이름으로 참조할 수도 있어서, x에 값을 주지 않고 y에 표현식 e를 명시적으로 주고 싶다면 다음과 같이 쓸 수 있어요:
subst C {y = e} eq cx
드문 상황에서는 인자를 이름으로 주는 데 사용하는 이름을 바인딩된 변수의 이름과 분리하는 것이 유용할 수 있어요. 예를 들어 원하는 이름이 기존 이름을 가리는 경우예요. 이를 하려면 다음과 같이 씁니다:
id₂ : {A = X : Set} → X → X -- name of bound variable is X
id₂ x = x
use-id₂ : (Y : Set) → Y → Y
use-id₂ Y = id₂ {A = Y} -- but the label is A
레이블이 붙은 바인딩은 입력 시 홀로 나타나야 하므로, 이 예에서는 타입 Set을 반복할 필요가 있어요:
const : {A = X : Set} {B = Y : Set} → A → B → A
const x y = x
암시적 함수 공간을 구성할 때 암시 인자는 생략될 수 있어서, 아래 두 표현식은 모두 타입 {A : Set} → A → A의 유효한 표현식이에요:
z1 = λ {A} x → x
z2 = λ x → x
함수 타입에 대한 ∀(또는 forall) 문법에도 암시 변형이 있어요:
① : (∀ {x : A} → B) is-the-same-as ({x : A} → B)
② : (∀ {x} → B) is-the-same-as ({x : _} → B)
③ : (∀ {x y} → B) is-the-same-as (∀ {x} → ∀ {y} → B)
매우 특별한 상황에서는 이름 없는 숨은 인자 {A} → B를 선언하는 것이 의미가 있어요. 다음 예에서 zero ≤ zero 타입의 scons의 숨은 인자는 이 타입이 ⊤로 축약되므로 η-확장으로 풀 수 있어요.
data ⊥ : Set where
_≤_ : Nat → Nat → Set
zero ≤ _ = ⊤
suc m ≤ zero = ⊥
suc m ≤ suc n = m ≤ n
data SList (bound : Nat) : Set where
[] : SList bound
scons : (head : Nat) → {head ≤ bound} → (tail : SList head) → SList bound
example : SList zero
example = scons zero []
함수 공간이 언제 암시적일 수 있는지에 대한 제한은 없어요. 내부적으로 명시적 함수 공간과 암시적 함수 공간은 같은 방식으로 취급돼요. 이는 암시 인자가 해결될 것이라는 보장이 없다는 뜻이에요. 해결되지 않은 암시 인자가 있으면 타입 체커는 어떤 적용이 해결되지 않은 인자를 포함하는지 나타내는 오류 메시지를 줄 거예요.
암시 인자에 대한 이 관대한 접근의 이유는, 암시 인자의 사용이 해결이 보장되는 경우로 제한하면 실제로 많은 유용한 경우가 배제되기 때문이에요.
전술 인자 (Tactic arguments)
@(tactic t) 속성으로 특정 암시 인자를 풀기 위해 사용할 전술을 선언할 수 있어요. 여기서 t : Term → TC ⊤예요. 예를 들어:
clever-search : Term → TC ⊤
clever-search hole = unify hole (lit (nat 17))
the-best-number : {@(tactic clever-search) n : Nat} → Nat
the-best-number {n} = n
check : the-best-number ≡ 17
check = refl
전술은 올바른 타입의 임의의 항일 수 있고 함수의 이전 인자에 의존할 수 있어요:
default : {A : Set} → A → Term → TC ⊤
default x hole = bindTC (quoteTC x) (unify hole)
search : (depth : Nat) → Term → TC ⊤
example : {@(tactic default 10) depth : Nat}
{@(tactic search depth) proof : Proof} →
Goal