10. 타입 클래스
타입 클래스는 함수형 프로그래밍 언어에서 애드혹 다형성(ad-hoc polymorphism)을 체계적으로 구현하는 방법으로 도입되었습니다. 먼저, 애드혹 다형 함수(덧셈 등)가 덧셈의 타입별 구현을 단순히 인자로 받은 다음 나머지 인자들에 그 구현을 호출하기만 한다면, 그러한 함수를 구현하기는 쉬우리라는 점에 주목합시다. 예를 들어, Lean에서 덧셈의 구현을 담는 구조체를 선언한다고 가정해 봅시다.
위의 Lean 코드에서 필드 add는 Add.add : {α : Type} → Add α → α → α → α 타입을 가지며, 여기서 타입 α를 감싸는 중괄호는 그것이 암시적 인자임을 의미합니다. double은 다음과 같이 구현할 수 있습니다.
namespace Ex
structure Add (α : Type) where
add : α → α → α
def double (s : Add α) (x : α) : α :=
s.add x x
#eval double { add := Nat.add } 10
#eval double { add := Nat.mul } 10
#eval double { add := Int.add } 10end Ex
자연수 n은 double { add := Nat.add } n으로 두 배로 만들 수 있다는 점에 유의하십시오. 물론 사용자가 이런 식으로 구현을 일일이 직접 넘겨주어야 한다면 매우 번거로울 것입니다. 실제로 그렇게 하면 임시 다형성(ad-hoc polymorphism)이 가져다줄 수 있는 이점 대부분이 사라질 것입니다.
타입 클래스의 핵심 아이디어는 Add α와 같은 인자를 암시적으로 만들고, 사용자가 정의한 인스턴스의 데이터베이스를 활용하여 타입 클래스 해결이라는 과정을 통해 원하는 인스턴스를 자동으로 합성하는 것입니다. Lean에서 위 예제의 structure를 class로 바꾸면 Add.add의 타입은 다음과 같이 됩니다:
여기서 대괄호는 Add α 타입의 인자가 인스턴스 암시적이라는 것, 즉 타입 클래스 해결을 사용하여 합성되어야 한다는 것을 나타냅니다. 이 버전의 add는 Haskell 항 add :: Add a => a -> a -> a에 해당하는 Lean의 대응물입니다. 마찬가지로, 다음과 같이 인스턴스를 등록할 수 있습니다:
namespace Ex
class Add (α : Type) where
add : α → α → α
instance : Add Nat where
add := Nat.add
instance : Add Int where
add := Int.add
instance : Add Float where
add := Float.add
end Ex
그러면 n : Nat과 m : Nat에 대해 항 Add.add n m은 Add Nat을 목표로 하는 타입 클래스 해결을 일으키며, 타입 클래스 해결은 위에서 정의한 Nat의 인스턴스를 합성합니다. 이제 인스턴스 암시적 인자를 사용하여 다음과 같이 double을 다시 구현할 수 있습니다:
namespace Ex
class Add (α : Type) where
add : α → α → α
instance : Add Nat where
add := Nat.add
instance : Add Int where
add := Int.add
instance : Add Float where
add := Float.add
def double [Add α] (x : α) : α :=
Add.add x x
#check @double
#eval double 10
#eval double (10 : Int)
#eval double (7 : Float)
#eval double (239.0 + 2)
end Ex
일반적으로 인스턴스는 다른 인스턴스에 복잡한 방식으로 의존할 수 있습니다. 예를 들어, α에 덧셈이 있으면 Array α에도 덧셈이 있다는 인스턴스를 선언할 수 있습니다:
instance [Add α] : Add (Array α) where
add x y := Array.zipWith (· + ·) x y
#eval Add.add #[1, 2] #[3, 4]
#eval #[1, 2] + #[3, 4]
Lean에서 (· + ·)는 fun x y => x + y를 나타내는 표기법이라는 점에 유의하십시오.
위 예제는 타입 클래스를 사용하여 표기법을 오버로드하는 방법을 보여 줍니다. 이제 또 다른 적용을 살펴보겠습니다. 주어진 타입의 임의의 원소가 필요한 경우가 많습니다. Lean에서는 타입에 원소가 하나도 없을 수 있다는 점을 떠올려 보십시오. “예외적인 경우(corner case)”에 정의가 임의의 원소를 반환하기를 원하는 일이 자주 있습니다. 예를 들어, xs의 타입이 List α일 때 표현식 head xs의 타입이 α이기를 원할 수 있습니다. 마찬가지로, 많은 정리는 타입이 비어 있지 않다는 추가 가정하에서 성립합니다. 예를 들어, α가 타입이라면 ∃ x : α, x = x는 α가 비어 있지 않을 때에만 참입니다. 표준 라이브러리는 타입 클래스 추론이 원소를 가진 타입(inhabited type)의 “기본” 원소를 추론할 수 있도록 타입 클래스 Inhabited를 정의합니다. 위 프로그램의 첫 번째 단계인 적절한 클래스 선언부터 시작합시다:
Inhabited.default에는 명시적 인자가 하나도 없다는 점에 유의하십시오.
클래스 Inhabited α의 원소는 어떤 원소 x : α에 대해 Inhabited.mk x 형태의 표현식일 뿐입니다. 사영 Inhabited.default를 사용하면 Inhabited α의 원소로부터 그러한 α의 원소를 “추출”할 수 있습니다. 이제 이 클래스를 몇 가지 인스턴스로 채워 봅시다:
namespace Ex
class Inhabited (a : Type _) where
default : a
instance : Inhabited Bool where
default := true
instance : Inhabited Nat where
default := 0
instance : Inhabited Unit where
default := ()
instance : Inhabited Prop where
default := True
#eval (Inhabited.default : Nat)
#eval (Inhabited.default : Bool)end Ex
export 명령을 사용하면 Inhabited.default의 별칭 default를 만들 수 있습니다.
namespace Ex
class Inhabited (a : Type _) where
default : a
instance : Inhabited Bool where
default := true
instance : Inhabited Nat where
default := 0
instance : Inhabited Unit where
default := ()
instance : Inhabited Prop where
default := True
export Inhabited (default)
#eval (default : Nat)
#eval (default : Bool)end Ex
10.1. 인스턴스 연쇄
타입 클래스 추론이 그 정도에 그친다면 그다지 인상적이지 않을 것입니다. 그저 정교화기가 조회 테이블에서 찾을 수 있도록 인스턴스 목록을 저장해 두는 메커니즘에 불과할 것입니다. 타입 클래스 추론을 강력하게 만드는 것은 인스턴스를 연쇄할 수 있다는 점입니다. 즉, 인스턴스 선언이 다시 타입 클래스의 암시적 인스턴스에 의존할 수 있습니다. 이로 인해 클래스 추론은 Prolog와 유사한 탐색 방식으로, 필요할 때는 백트래킹하면서 인스턴스들을 재귀적으로 거쳐 연쇄해 나갑니다.
예를 들어, 다음 정의는 두 타입 α와 β가 거주(inhabited)되어 있으면 그 곱도 거주되어 있음을 보여 줍니다:
이를 앞서 나온 인스턴스 선언들에 추가하면, 타입 클래스 인스턴스는 예를 들어 Nat × Bool의 기본 원소를 추론할 수 있습니다:
namespace Ex
class Inhabited (α : Type u) where
default : α
instance : Inhabited Bool where
default := true
instance : Inhabited Nat where
default := 0
opaque default [Inhabited α] : α :=
Inhabited.default
instance [Inhabited α] [Inhabited β] : Inhabited (α × β) where
default := (default, default)
#eval (default : Nat × Bool)end Ex
마찬가지로, 적절한 상수 함수를 사용하여 타입 함수의 원소를 만들 수 있습니다:
연습 삼아 List나 Sum 타입 같은 다른 타입에 대한 기본 인스턴스를 정의해 보십시오.
Lean 표준 라이브러리에는 inferInstance라는 정의가 있습니다. 이 정의의 타입은 {α : Sort u} → [i : α] → α이며, 기대 타입이 인스턴스일 때 타입 클래스 해결 절차를 작동시키는 데 유용합니다.
#check (inferInstance : Inhabited Nat)
def foo : Inhabited (Nat × Nat) :=
inferInstance
theorem ex : foo.default = (default, default) :=
rfl
#print 명령을 사용하면 inferInstance가 얼마나 단순한지 확인할 수 있습니다.
#print inferInstance10.2. ToString
다형적 메서드 toString의 타입은 {α : Type u} → [ToString α] → α → String입니다. 직접 정의한 타입에 대해 이 인스턴스를 구현하고, 연쇄(chaining)를 사용하여 복잡한 값을 문자열로 변환합니다. Lean은 대부분의 내장 타입에 대한 ToString 인스턴스를 기본으로 제공합니다.
10.3. 숫자 리터럴
Lean에서 숫자 리터럴은 다형적입니다. 숫자 리터럴(예: 2)을 사용하여 타입 클래스 OfNat를 구현하는 모든 타입의 원소를 나타낼 수 있습니다.
structure Rational where
num : Int
den : Nat
inv : den ≠ 0
instance : OfNat Rational n where
ofNat := { num := n, den := 1, inv := n:Nat⊢ 1 ≠ 0 All goals completed! 🐙 }
instance : ToString Rational where
toString r := s!"{r.num}/{r.den}"
#eval (2 : Rational)
#check (2 : Rational)
#check (2 : Nat)
Lean은 (2 : Nat)과 (2 : Rational)이라는 항을 각각 @OfNat.ofNat Nat 2 (@instOfNatNat 2)와 @OfNat.ofNat Rational 2 (@instOfNatRational 2)로 정교화합니다. 정교화된 항에 나타나는 숫자 2를 원시(raw) 자연수라고 합니다. 원시 자연수 2는 매크로 nat_lit 2를 사용하여 입력할 수 있습니다.
원시 자연수는 다형적이지 않습니다.
OfNat 인스턴스는 숫자 리터럴에 대해 매개변수화되어 있습니다. 따라서 특정 숫자 리터럴에 대한 인스턴스를 정의할 수 있습니다. 두 번째 인수는 위 예제처럼 변수인 경우가 많으며, 원시(raw) 자연수인 경우도 많습니다.
10.4. 출력 매개변수
기본적으로 Lean은 항 T가 알려져 있고 누락된 부분을 포함하지 않을 때에만 인스턴스 Inhabited T의 합성을 시도합니다. 다음 명령은 타입에 누락된 부분(즉, _)이 있기 때문에 typeclass instance problem is stuck, it is often due to metavariables 오류를 발생시킵니다.
/--
error: typeclass instance problem is stuck, it is often due to metavariables
Inhabited (Nat × ?m.2)
-/
#guard_msgs (error) in
#eval (inferInstance : Inhabited (Nat × _))
타입 클래스 Inhabited의 매개변수는 타입 클래스 합성기에 대한 입력 값으로 볼 수 있습니다. 타입 클래스에 매개변수가 여러 개 있으면 그중 일부를 출력 매개변수로 지정할 수 있습니다. Lean은 이러한 매개변수에 빠진 부분이 있더라도 타입 클래스 합성기를 시작합니다. 다음 예제에서는 출력 매개변수를 사용하여 이종(heterogeneous) 다형적 곱셈을 정의합니다.
namespace Ex
class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
hMul : α → β → γ
export HMul (hMul)
instance : HMul Nat Nat Nat where
hMul := Nat.mul
instance : HMul Nat (Array Nat) (Array Nat) where
hMul a bs := bs.map (fun b => hMul a b)
#eval hMul 4 3
#eval hMul 4 #[2, 3, 4]end Ex
매개변수 α와 β는 입력 매개변수로, γ는 출력 매개변수로 간주됩니다. 적용 hMul a b가 주어지면 a와 b의 타입이 알려진 뒤에 타입 클래스 합성기가 호출되고, 결과 타입은 출력 매개변수 γ에서 얻어집니다. 위 예제에서는 두 개의 인스턴스를 정의했습니다. 첫 번째는 자연수에 대한 동종 곱셈입니다. 두 번째는 배열에 대한 스칼라 곱셈입니다. 인스턴스를 연쇄하고 두 번째 인스턴스를 일반화한다는 점에 유의하십시오.
namespace Ex
class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
hMul : α → β → γ
export HMul (hMul)
instance : HMul Nat Nat Nat where
hMul := Nat.mul
instance : HMul Int Int Int where
hMul := Int.mul
instance [HMul α β γ] : HMul α (Array β) (Array γ) where
hMul a bs := bs.map (fun b => hMul a b)
#eval hMul 4 3
#eval hMul 4 #[2, 3, 4]
#eval hMul (-2) #[3, -1, 4]
#eval hMul 2 #[#[2, 3], #[0, 4]]end Ex
HMul α β γ 인스턴스가 있으면 언제든지 새로 만든 스칼라 배열 곱셈 인스턴스를 사용하여 Array β 타입의 배열에 α 타입의 스칼라를 곱할 수 있습니다. 마지막 #eval에서는 배열의 배열에 이 인스턴스가 두 번 사용되었다는 점에 주목하십시오.
인스턴스 합성 중에는 출력 매개변수가 무시됩니다. 출력 매개변수의 값이 이미 결정된 맥락에서 인스턴스 합성이 일어나더라도 그 값은 무시됩니다. 입력 매개변수를 사용하여 인스턴스를 찾고 나면, Lean은 이미 알려진 출력 매개변수의 값이 찾아낸 값과 일치하는지 확인합니다.
Lean에는 입력 매개변수의 특징 일부와 출력 매개변수의 특징 일부를 함께 지니는 준출력 매개변수도 있습니다. 입력 매개변수와 마찬가지로, 준출력 매개변수도 인스턴스를 선택할 때 고려됩니다. 출력 매개변수와 마찬가지로, 준출력 매개변수는 알려지지 않은 값을 인스턴스화하는 데 사용될 수 있습니다. 하지만 준출력 매개변수는 그 값을 유일하게 결정하지는 않습니다. 준출력 매개변수를 사용한 인스턴스 합성은 인스턴스를 고려하는 순서에 따라 어떤 인스턴스가 선택될지 달라질 수 있으므로 예측하기가 더 어려울 수 있지만, 그만큼 더 유연하기도 합니다.
10.5. 기본 인스턴스
클래스 HMul에서 매개변수 α와 β는 입력값으로 취급됩니다. 따라서 타입 클래스 합성은 이 두 타입이 알려진 뒤에야 시작됩니다. 이는 너무 제한적인 경우가 많습니다.
namespace Ex
class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
hMul : α → β → γ
export HMul (hMul)
instance : HMul Int Int Int where
hMul := Int.mul
def xs : List Int := [1, 2, 3]
/--
error: typeclass instance problem is stuck
HMul Int ?m.2 (?m.11 y)
Note: Lean will not try to resolve this typeclass instance problem because the second type argument to `HMul` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.
Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
-/
#guard_msgs (error) in
#eval fun y => xs.map (fun x => hMul x y)
end Ex
y의 타입이 주어지지 않았기 때문에 Lean은 HMul 인스턴스를 합성하지 않습니다. 그러나 이러한 상황에서는 y와 x의 타입이 같아야 한다고 가정하는 것이 자연스럽습니다. 기본 인스턴스(default instances)를 사용하면 바로 그렇게 할 수 있습니다.
namespace Ex
class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
hMul : α → β → γ
export HMul (hMul)
@[default_instance]
instance : HMul Int Int Int where
hMul := Int.mul
def xs : List Int := [1, 2, 3]
#check fun y => xs.map (fun x => hMul x y)end Ex
위 인스턴스에 [default_instance] 속성을 붙이면, 보류 중인 타입 클래스 합성 문제에 이 인스턴스를 사용하도록 Lean에 지시하게 됩니다. 실제 Lean 구현은 산술 연산자에 대해 동종(homogeneous) 클래스와 이종(heterogeneous) 클래스를 정의합니다. 또한 a + b, a * b, a - b, a / b, a % b는 이종 버전에 대한 표기법입니다. 인스턴스 OfNat Nat n은 OfNat 클래스의 기본 인스턴스(우선순위 100)입니다. 이 때문에 기대 타입을 알 수 없을 때 숫자 2는 Nat 타입을 가집니다. 더 높은 우선순위를 가진 기본 인스턴스를 정의하여 내장 인스턴스를 재정의할 수 있습니다.
structure Rational where
num : Int
den : Nat
inv : den ≠ 0
@[default_instance 200]
instance : OfNat Rational n where
ofNat := { num := n, den := 1, inv := n:Nat⊢ 1 ≠ 0 All goals completed! 🐙 }
instance : ToString Rational where
toString r := s!"{r.num}/{r.den}"
#check 2
우선순위는 서로 다른 기본 인스턴스 간의 상호작용을 제어하는 데에도 유용합니다. 예를 들어, xs의 타입이 List α라고 가정합시다. xs.map (fun x => 2 * x)를 정교화할 때, 곱셈에 대한 동종(homogeneous) 인스턴스가 OfNat α 2에 대한 기본 인스턴스보다 더 높은 우선순위를 갖기를 원합니다. 이는 HMul α α α 인스턴스만 구현하고 HMul Nat α α는 구현하지 않은 경우에 특히 중요합니다. 이제 Lean에서 a * b 표기법이 어떻게 정의되는지 밝히겠습니다.
namespace Ex
class OfNat (α : Type u) (n : Nat) where
ofNat : α
@[default_instance]
instance (n : Nat) : OfNat Nat n where
ofNat := n
class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
hMul : α → β → γ
class Mul (α : Type u) where
mul : α → α → α
@[default_instance 10]
instance [Mul α] : HMul α α α where
hMul a b := Mul.mul a b
infixl:70 " * " => HMul.hMul
end Ex
Mul 클래스는 동종 곱셈만 구현하는 타입에 편리합니다.
10.6. 지역 인스턴스
Lean에서 타입 클래스는 속성(attribute)을 사용하여 구현됩니다. 따라서 local 수식어를 사용하여 현재 section이나 namespace가 닫힐 때까지, 또는 현재 파일이 끝날 때까지만 효력이 있음을 지정할 수 있습니다.
structure Point where
x : Nat
y : Nat
section
local instance : Add Point where
add a b := { x := a.x + b.x, y := a.y + b.y }
def double (p : Point) :=
p + p
end -- instance `Add Point` is not active anymore
/--
error: failed to synthesize instance of type class
HAdd Point Point ?m.5
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-/
#guard_msgs in
def triple (p : Point) :=
p + p + p
또한 attribute 명령을 사용하여 현재 section이나 namespace가 닫힐 때까지, 또는 현재 파일이 끝날 때까지 인스턴스를 일시적으로 비활성화할 수도 있습니다.
structure Point where
x : Nat
y : Nat
instance addPoint : Add Point where
add a b := { x := a.x + b.x, y := a.y + b.y }
def double (p : Point) :=
p + p
attribute [-instance] addPoint
/--
error: failed to synthesize instance of type class
HAdd Point Point ?m.5
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-/
#guard_msgs in
def triple (p : Point) :=
p + p + p -- Error: failed to synthesize instance
이 명령은 문제를 진단할 때만 사용하시기를 권장합니다.
10.7. 범위 지정 인스턴스
네임스페이스 안에서 범위 지정 인스턴스(scoped instance)를 선언할 수도 있습니다. 이러한 종류의 인스턴스는 해당 네임스페이스 안에 있거나 그 네임스페이스를 열었을 때에만 활성화됩니다.
structure Point where
x : Nat
y : Nat
namespace Point
scoped instance : Add Point where
add a b := { x := a.x + b.x, y := a.y + b.y }
def double (p : Point) :=
p + p
end Point
-- instance `Add Point` is not active anymore
/--
error: failed to synthesize instance of type class
HAdd Point Point ?m.3
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-/
#guard_msgs (error) in
#check fun (p : Point) => p + p + p
namespace Point
-- instance `Add Point` is active again
#check fun (p : Point) => p + p + p
end Point
open Point -- activates instance `Add Point`
#check fun (p : Point) => p + p + p
open scoped <namespace> 명령을 사용하면 범위가 지정된 속성을 활성화할 수 있지만, 해당 네임스페이스의 이름을 “열지는” 않습니다.
structure Point where
x : Nat
y : Nat
namespace Point
scoped instance : Add Point where
add a b := { x := a.x + b.x, y := a.y + b.y }
def double (p : Point) :=
p + p
end Point
open scoped Point -- activates instance `Add Point`
#check fun (p : Point) => p + p + p
/--
error: Unknown identifier `double`
-/
#guard_msgs (error) in
#check fun (p : Point) => double p10.8. 결정 가능한 명제
표준 라이브러리에 정의된 타입 클래스의 또 다른 예로 Decidable 명제의 타입 클래스를 살펴봅시다. 대략적으로 말하면, Prop의 원소는 그것이 참인지 거짓인지 판정할 수 있을 때 결정 가능하다고 합니다. 이 구분은 구성적 수학에서만 의미가 있습니다. 고전적으로는 모든 명제가 결정 가능합니다. 그러나 예를 들어 경우 나누기로 함수를 정의하는 데 고전적 원리를 사용하면, 그 함수는 계산 가능하지 않게 됩니다. 알고리즘 관점에서 말하면, Decidable 타입 클래스를 사용하여 명제가 참인지 아닌지를 실제로 판정하는 절차를 추론할 수 있습니다. 그 결과, 이 타입 클래스는 계산적 정의가 가능할 때는 이를 지원하는 동시에 고전적 정의와 고전적 추론을 사용하는 쪽으로도 매끄럽게 넘어갈 수 있게 해 줍니다.
표준 라이브러리에서 Decidable은 다음과 같이 형식적으로 정의되어 있습니다.
namespace Hidden
class inductive Decidable (p : Prop) where
| isFalse (h : ¬p) : Decidable p
| isTrue (h : p) : Decidable p
end Hidden
논리적으로 말하자면, 원소 t : Decidable p를 갖는 것은 원소 t' : p ∨ ¬p를 갖는 것보다 더 강합니다. 이를 통해 p의 진릿값에 따라 임의의 타입의 값을 정의할 수 있기 때문입니다. 예를 들어, 표현식 if p then a else b가 의미를 가지려면 p가 결정 가능하다는 것을 알아야 합니다. 이 표현식은 ite p a b의 문법적 설탕이며, 여기서 ite는 다음과 같이 정의됩니다:
namespace Hidden
def ite {α : Sort u}
(c : Prop) [h : Decidable c]
(t e : α) : α :=
h.casesOn (motive := fun _ => α) (fun _ => e) (fun _ => t)
end Hidden
표준 라이브러리에는 ite의 변형인 dite도 있으며, 이는 의존 if-then-else 표현식입니다. 이는 다음과 같이 정의됩니다:
namespace Hidden
def dite {α : Sort u}
(c : Prop) [h : Decidable c]
(t : c → α) (e : Not c → α) : α :=
Decidable.casesOn (motive := fun _ => α) h e t
end Hidden
즉, dite c t e에서는 “then” 분기에서 hc : c를, “else” 분기에서 hnc : ¬c를 가정할 수 있습니다. dite를 더 편리하게 사용할 수 있도록, Lean에서는 dite c (fun h : c => t h) (fun h : ¬c => e h) 대신 if h : c then t else e라고 쓸 수 있습니다.
고전 논리 없이는 모든 명제가 결정 가능하다는 것을 증명할 수 없습니다. 하지만 특정 명제들이 결정 가능하다는 것은 증명할 수 있습니다. 예를 들어, 자연수와 정수에 대한 상등 및 비교와 같은 기본 연산의 결정 가능성을 증명할 수 있습니다. 게다가 결정 가능성은 명제 연결사에 대해 보존됩니다:
따라서 자연수에 대한 결정 가능한 술어를 기준으로 경우를 나누어 정의할 수 있습니다:
def step (a b x : Nat) : Nat :=
if x < a ∨ x > b then 0 else 1
set_option pp.explicit true
#print step
암시적 인자 표시를 켜 보면, 정교화기가 적절한 인스턴스를 적용하는 것만으로 명제 x < a ∨ x > b의 결정 가능성을 추론했음을 알 수 있습니다.
고전 공리를 사용하면 모든 명제가 결정 가능하다는 것을 증명할 수 있습니다. 고전 공리를 가져오고 Classical 네임스페이스를 열면 결정 가능성의 일반 인스턴스를 사용할 수 있습니다.
open Classical
이후로 Decidable p는 모든 p에 대해 인스턴스를 가지게 됩니다. 따라서 고전적으로 추론하고자 할 때에는 결정 가능성 가정에 의존하는 라이브러리의 모든 정리를 자유롭게 사용할 수 있습니다. 공리와 계산에서는 배중률을 사용하여 함수를 정의하면 그 함수를 계산에 사용하지 못하게 될 수 있음을 보게 될 것입니다. 따라서 표준 라이브러리는 propDecidable 인스턴스에 낮은 우선순위를 부여합니다.
namespace Hidden
open Classical
noncomputable scoped
instance (priority := low) propDecidable (a : Prop) : Decidable a :=
choice <| match em a with
| Or.inl h => ⟨isTrue h⟩
| Or.inr h => ⟨isFalse h⟩
end Hidden
이를 통해 Lean은 다른 인스턴스를 우선적으로 사용하고, 결정 가능성을 추론하려는 다른 시도가 모두 실패한 뒤에야 propDecidable을 대신 사용하게 됩니다.
Decidable 타입 클래스는 정리 증명을 위한 소규모 자동화 기능도 어느 정도 제공합니다. 표준 라이브러리는 Decidable 인스턴스를 사용하여 간단한 목표를 해결하는 택틱 decide와 함께, Decidable 인스턴스를 사용하여 대응하는 Bool을 계산하는 함수 decide도 도입합니다.
example : 10 < 5 ∨ 1 > 0 := ⊢ 10 < 5 ∨ 1 > 0
All goals completed! 🐙
example : ¬(True ∧ False) := ⊢ ¬(True ∧ False)
All goals completed! 🐙
example : 10 * 20 = 200 := ⊢ 10 * 20 = 200
All goals completed! 🐙
theorem ex : True ∧ 2 = 1 + 1 := ⊢ True ∧ 2 = 1 + 1
All goals completed! 🐙
#print ex
#check @of_decide_eq_true
#check @decide
작동 방식은 다음과 같습니다. 표현식 decide p는 p에 대한 결정 절차를 추론하려고 시도하며, 추론에 성공하면 true 또는 false로 평가됩니다. 특히 p가 참인 닫힌 표현식이라면, decide p는 정의적으로 불리언 값 true로 환원됩니다. decide p = true가 성립한다는 가정 아래에서 of_decide_eq_true는 p의 증명을 만들어 냅니다. 택틱 decide는 이 모든 것을 종합하여 목표 p를 증명합니다. 앞에서 살펴본 바에 따르면, p에 대해 추론된 결정 절차가 정의적으로 isTrue 경우로 평가될 만큼 충분한 정보를 가지고 있을 때는 언제나 decide가 성공합니다.
10.9. 타입 클래스 추론 관리하기
타입 클래스 추론으로 Lean이 추론할 수 있는 표현식을 직접 제공해야 하는 상황이라면, inferInstance를 사용하여 Lean에게 추론을 수행하도록 요청할 수 있습니다:
def foo : Add Nat := inferInstance
def bar : Inhabited (Nat → Nat) := inferInstance
#check @inferInstance
사실 Lean의 (t : T) 표기법을 사용하면 찾고 있는 인스턴스의 클래스를 간결하게 지정할 수 있습니다.
때로는 클래스가 정의 아래에 가려져 있어서 Lean이 인스턴스를 찾지 못하는 경우가 있습니다. 예를 들어, Lean은 Inhabited (Set α)의 인스턴스를 찾지 못합니다. 이 경우 다음과 같이 인스턴스를 명시적으로 선언할 수 있습니다:
def Set (α : Type u) := α → Prop
/--
error: failed to synthesize instance of type class
Inhabited (Set α)
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-/
#guard_msgs in
example : Inhabited (Set α) :=
inferInstance
instance : Inhabited (Set α) :=
inferInstanceAs (Inhabited (α → Prop))
때때로 타입 클래스 추론이 예상한 인스턴스를 찾지 못하거나, 더 나쁜 경우에는 무한 루프에 빠져 시간 초과가 발생할 수 있습니다. 이러한 상황에서 디버깅을 돕기 위해, Lean에서는 탐색 과정의 추적을 요청할 수 있습니다:
set_option trace.Meta.synthInstance true
VS Code를 사용하는 경우, 해당 정리나 정의 위에 마우스를 올리거나 CtrlShiftEnter로 메시지 창을 열어 결과를 확인할 수 있습니다.
다음 옵션을 사용하여 검색 범위를 제한할 수도 있습니다.
synthInstance.maxHeartbeats 옵션은 타입 클래스 해결 문제 하나당 허용되는 최대 하트비트 수를 지정합니다. 하트비트는 (작은) 메모리 할당 횟수를 천 단위로 센 값이며, 0은 제한이 없음을 의미합니다. synthInstance.maxSize 옵션은 타입 클래스 인스턴스 합성 절차에서 해를 구성하는 데 사용되는 인스턴스의 최대 개수입니다.
또한 VS Code와 Emacs 편집기 모드 모두에서 set_option에 탭 자동 완성이 작동하므로, 이를 이용해 적절한 옵션을 찾을 수 있다는 점도 기억해 두십시오.
앞서 언급했듯이, 주어진 맥락에 있는 타입 클래스 인스턴스들은 Prolog와 유사한 프로그램을 나타내며, 이로부터 백트래킹 탐색이 일어납니다. 프로그램의 효율성과 찾게 되는 해는 모두 시스템이 인스턴스를 시도하는 순서에 따라 달라질 수 있습니다. 가장 나중에 선언된 인스턴스가 가장 먼저 시도됩니다. 또한 인스턴스가 다른 모듈에 선언된 경우, 인스턴스가 시도되는 순서는 네임스페이스가 열리는 순서에 따라 달라집니다. 나중에 열린 네임스페이스에 선언된 인스턴스일수록 먼저 시도됩니다.
타입 클래스 인스턴스에 우선순위를 지정하면 인스턴스를 시도하는 순서를 바꿀 수 있습니다. 인스턴스를 선언하면 기본 우선순위 값이 지정됩니다. 인스턴스를 정의할 때 다른 우선순위를 지정할 수 있습니다. 다음 예제는 그 방법을 보여 줍니다:
10.10. 타입 클래스를 이용한 강제 변환
가장 기본적인 형태의 강제 변환은 한 타입의 원소를 다른 타입의 원소로 대응시킵니다. 예를 들어, Nat에서 Int로의 강제 변환이 있으면 임의의 원소 n : Nat를 Int의 원소로 볼 수 있습니다. 하지만 어떤 강제 변환은 매개변수에 의존합니다. 예를 들어, 임의의 타입 α에 대해 임의의 원소 as : List α를 Set α의 원소, 즉 리스트에 나타나는 원소들의 집합으로 볼 수 있습니다. 이에 해당하는 강제 변환은 α로 매개변수화된 타입들의 “족(family)” List α 위에서 정의됩니다.
Lean에서는 세 가지 종류의 강제 변환을 선언할 수 있습니다:
-
한 타입 족에서 다른 타입 족으로
-
타입 족에서 소트의 클래스로
-
타입 족에서 함수 타입들의 클래스로
첫 번째 종류의 강제 변환은 원본 계열의 한 구성원에 속하는 임의의 원소를 대상 계열의 대응하는 구성원에 속하는 원소로 볼 수 있게 해 줍니다. 두 번째 종류의 강제 변환은 원본 계열의 한 구성원에 속하는 임의의 원소를 타입으로 볼 수 있게 해 줍니다. 세 번째 종류의 강제 변환은 원본 계열의 임의의 원소를 함수로 볼 수 있게 해 줍니다. 이들을 차례로 하나씩 살펴봅시다.
Lean에서 강제 변환은 타입 클래스 해결 프레임워크를 기반으로 구현됩니다. α에서 β로의 강제 변환은 Coe α β의 인스턴스를 선언하여 정의합니다. 예를 들어, Bool에서 Prop으로의 강제 변환은 다음과 같이 정의할 수 있습니다:
이를 통해 if-then-else 표현식에서 불리언 항을 사용할 수 있습니다:
다음과 같이 List α에서 Set α로의 강제 변환을 정의할 수 있습니다:
def Set (α : Type u) := α → Prop
def Set.empty {α : Type u} : Set α := fun _ => False
def Set.mem (a : α) (s : Set α) : Prop := s a
def Set.singleton (a : α) : Set α := fun x => x = a
def Set.union (a b : Set α) : Set α := fun x => a x ∨ b x
notation "{ " a " }" => Set.singleton a
infix:55 " ∪ " => Set.union
def List.toSet : List α → Set α
| [] => Set.empty
| a::as => {a} ∪ as.toSet
instance : Coe (List α) (Set α) where
coe a := a.toSet
def s : Set Nat := {1}
#check s ∪ [2, 3]
↑ 표기법을 사용하면 특정 위치에 강제 변환이 삽입되도록 강제할 수 있습니다. 이 표기법은 의도를 명확히 드러내고 강제 변환 해소 시스템의 한계를 우회하는 데에도 도움이 됩니다.
def Set (α : Type u) := α → Prop
def Set.empty {α : Type u} : Set α := fun _ => False
def Set.mem (a : α) (s : Set α) : Prop := s a
def Set.singleton (a : α) : Set α := fun x => x = a
def Set.union (a b : Set α) : Set α := fun x => a x ∨ b x
notation "{ " a " }" => Set.singleton a
infix:55 " ∪ " => Set.union
def List.toSet : List α → Set α
| [] => Set.empty
| a::as => {a} ∪ as.toSet
instance : Coe (List α) (Set α) where
coe a := a.toSet
def s : Set Nat := {1}
#check let x := ↑[2, 3]; s ∪ x
#check let x := [2, 3]; s ∪ x
Lean은 타입 클래스 CoeDep을 사용하는 의존 강제 변환도 지원합니다. 예를 들어, 임의의 명제를 Bool로 강제 변환할 수는 없으며, Decidable 타입 클래스를 구현하는 명제만 강제 변환할 수 있습니다.
Lean은 필요할 경우 (비의존적인) 강제 변환을 연쇄적으로 적용하기도 합니다. 실제로 타입 클래스 CoeT는 Coe의 추이적 폐포입니다.
이제 두 번째 종류의 강제 변환을 살펴봅시다. 소트의 클래스(class of sorts)란 유니버스 Type u들의 모음을 의미합니다. 두 번째 종류의 강제 변환은 다음과 같은 형태입니다:
c : (x1 : A1) → ... → (xn : An) → F x1 ... xn → Type u
여기서 F는 위와 같은 타입 족(family of types)입니다. 이를 통해 t의 타입이 F a₁ ... aₙ일 때마다 s : t라고 쓸 수 있습니다. 다시 말해, 이 강제 변환을 통해 F a₁ ... aₙ의 원소를 타입으로 볼 수 있습니다. 이는 한 구성 요소, 즉 구조의 캐리어(carrier)가 Type인 대수적 구조를 정의할 때 매우 유용합니다. 예를 들어, 반군(semigroup)은 다음과 같이 정의할 수 있습니다:
structure Semigroup where
carrier : Type u
mul : carrier → carrier → carrier
mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)
instance (S : Semigroup) : Mul S.carrier where
mul a b := S.mul a b
다시 말해, 반군(semigroup)은 타입 carrier와 곱셈 mul로 구성되며, 이 곱셈은 결합법칙을 만족한다는 성질을 가집니다. instance 명령을 사용하면 a b : S.carrier가 있을 때마다 Semigroup.mul S a b 대신 a * b라고 쓸 수 있습니다. Lean이 a와 b의 타입으로부터 인자 S를 추론할 수 있다는 점에 주목하십시오. 함수 Semigroup.carrier는 클래스 Semigroup을 소트 Type u로 사상합니다:
structure Semigroup where
carrier : Type u
mul : carrier → carrier → carrier
mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)
instance (S : Semigroup) : Mul S.carrier where
mul a b := S.mul a b
#check Semigroup.carrier
이 함수를 강제 변환으로 선언하면, 반군 S : Semigroup이 있을 때마다 a : S.carrier 대신 a : S라고 쓸 수 있습니다:
structure Semigroup where
carrier : Type u
mul : carrier → carrier → carrier
mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)
instance (S : Semigroup) : Mul S.carrier where
mul a b := S.mul a b
instance : CoeSort Semigroup (Type u) where
coe s := s.carrier
example (S : Semigroup) (a b c : S) : (a * b) * c = a * (b * c) :=
Semigroup.mul_assoc _ a b c
(a b c : S)라고 쓸 수 있는 것은 바로 이 강제 변환 덕분입니다. Coe Semigroup (Type u)가 아니라 CoeSort Semigroup (Type u)의 인스턴스를 정의한다는 점에 유의하십시오.
함수 타입의 클래스란 Pi 타입 (z : B) → C들의 모임을 의미합니다. 세 번째 종류의 강제 변환은 다음과 같은 형태를 가집니다:
c : (x₁ : A₁) → ... → (xₙ : Aₙ) → (y : F x₁ ... xₙ) → (z : B) → C
여기서 F는 다시 타입의 족(family)이며, B와 C는 x₁, ..., xₙ, y에 의존할 수 있습니다. 이로써 t가 F a₁ ... aₙ의 원소일 때마다 t s라고 쓸 수 있습니다. 다시 말해, 이 강제 변환을 통해 F a₁ ... aₙ의 원소를 함수로 볼 수 있습니다. 위의 예제에 이어서, 반군 S1과 S2 사이의 준동형사상(morphism)이라는 개념을 정의할 수 있습니다. 즉, 곱셈을 보존하면서 S1의 캐리어(carrier)에서 S2의 캐리어로 가는 함수입니다(암묵적 강제 변환에 주목하십시오). 사영 Morphism.mor는 준동형사상을 그 기저 함수로 보냅니다:
structure Semigroup where
carrier : Type u
mul : carrier → carrier → carrier
mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)
instance (S : Semigroup) : Mul S.carrier where
mul a b := S.mul a b
instance : CoeSort Semigroup (Type u) where
coe s := s.carrier
structure Morphism (S1 S2 : Semigroup) where
mor : S1 → S2
resp_mul : ∀ a b : S1, mor (a * b) = (mor a) * (mor b)
#check @Morphism.mor그 결과, 이는 세 번째 종류의 강제 변환을 적용하기에 매우 적합한 대상입니다.
structure Semigroup where
carrier : Type u
mul : carrier → carrier → carrier
mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)
instance (S : Semigroup) : Mul S.carrier where
mul a b := S.mul a b
instance : CoeSort Semigroup (Type u) where
coe s := s.carrier
structure Morphism (S1 S2 : Semigroup) where
mor : S1 → S2
resp_mul : ∀ a b : S1, mor (a * b) = (mor a) * (mor b)
instance (S1 S2 : Semigroup) :
CoeFun (Morphism S1 S2) (fun _ => S1 → S2) where
coe m := m.mor
theorem resp_mul {S1 S2 : Semigroup} (f : Morphism S1 S2) (a b : S1)
: f (a * b) = f a * f b :=
f.resp_mul a b
example (S1 S2 : Semigroup) (f : Morphism S1 S2) (a : S1) :
f (a * a * a) = f a * f a * f a :=
calc f (a * a * a)
_ = f (a * a) * f a := S1:SemigroupS2:Semigroupf:Morphism S1 S2a:S1.carrier⊢ f.mor (a * a * a) = f.mor (a * a) * f.mor a All goals completed! 🐙
_ = f a * f a * f a := S1:SemigroupS2:Semigroupf:Morphism S1 S2a:S1.carrier⊢ f.mor (a * a) * f.mor a = f.mor a * f.mor a * f.mor a All goals completed! 🐙
강제 변환을 정의해 두면 f.mor (a * a * a) 대신 f (a * a * a)라고 쓸 수 있습니다. Morphism인 f가 함수가 필요한 자리에 쓰이면 Lean이 강제 변환을 삽입합니다. CoeSort와 비슷하게, 이런 종류의 강제 변환을 위한 또 다른 클래스 CoeFun이 있습니다. 매개변수 γ는 강제 변환의 목표가 되는 함수 타입을 지정하는 데 쓰입니다. 이 타입은 강제 변환되는 원래 타입에 의존할 수 있습니다.