10. 타입 클래스
타입 클래스는 함수형 프로그래밍 언어에서 애드혹 다형성(ad-hoc polymorphism)을 가능하게 하는 원칙적인 방법으로 도입되었습니다. 먼저 살펴볼 점은, 만약 어떤 함수가 (덧셈과 같은) 애드혹 다형 함수를 구현할 때 덧셈의 타입별 구현을 단순히 인자로 받아 나머지 인자들에 대해 그 구현을 호출하기만 한다면 구현하기가 쉬우리라는 것입니다. 예를 들어, Lean에서 덧셈의 구현을 담는 구조체(structure)를 선언한다고 가정해 봅시다.
위 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으로 두 배가 될 수 있다는 점에 주목하십시오. 물론, 사용자가 이런 식으로 구현체를 수동으로 전달하는 것은 매우 번거로울 것입니다. 실제로 이는 애드혹 다형성이 지닌 잠재적 이점 대부분을 무력화할 것입니다.
타입 클래스의 핵심 아이디어는 Add α와 같은 인자를 암묵적으로 만들고, 사용자 정의 인스턴스의 데이터베이스를 이용해 타입 클래스 해결(typeclass resolution)이라 알려진 과정을 통해 원하는 인스턴스를 자동으로 합성하는 것입니다. Lean에서는 위 예제의 structure를 class로 바꾸면 Add.add의 타입은 다음과 같이 됩니다:
여기서 대괄호는 Add α 타입의 인자가 instance implicit임을, 즉 타입 클래스 해석(typeclass resolution)을 사용하여 합성되어야 함을 나타냅니다. 이 버전의 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와 유사한 탐색처럼, 필요할 때 백트래킹하면서 재귀적으로 인스턴스를 거쳐 연쇄됩니다.
예를 들어, 다음 정의는 두 타입 α와 β가 거주자를 가진다면 그 곱 역시 거주자를 가진다는 것을 보여줍니다:
이를 앞서 나온 인스턴스 선언들에 추가하면, 예를 들어 타입 클래스 인스턴스는 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
마찬가지로, 적절한 상수 함수를 사용하여 type function을 채울 수 있습니다.
연습 문제로, 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 자연수라고 합니다. 매크로 nat_lit 2를 사용하면 raw 자연수 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은 타입 클래스 합성기를 시작합니다. 다음 예제에서는 출력 매개변수를 사용하여 이종 다형 곱셈을 정의합니다.
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의 타입이 제공되지 않았기 때문에 HMul 인스턴스는 Lean에 의해 합성되지 않습니다. 하지만 이런 상황에서는 y의 타입과 x의 타입이 같아야 한다고 가정하는 것이 자연스럽습니다. 기본 인스턴스를 사용하면 바로 이를 달성할 수 있습니다.
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 α α는 구현하지 않은 경우에 특히 중요합니다. 이제 표기법 a * b가 Lean에서 어떻게 정의되는지 밝히겠습니다.
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
또한 현재 section 또는 namespace가 닫힐 때까지, 혹은 현재 파일이 끝날 때까지 attribute 명령을 사용하여 인스턴스를 일시적으로 비활성화할 수도 있습니다.
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의 구문론적 설탕(syntactic sugar)이며, ite는 다음과 같이 정의됩니다.
namespace Hidden
def ite {α : Sort u}
(c : Prop) [h : Decidable c]
(t e : α) : α :=
h.casesOn (motive := fun _ => α) (fun _ => e) (fun _ => t)
end Hidden
표준 라이브러리에는 의존 if-then-else 표현식인 dite라는 ite의 변형도 포함되어 있습니다. 이는 다음과 같이 정의됩니다:
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에 대해 인스턴스를 가지게 됩니다. 따라서 결정 가능성 가정에 의존하는 라이브러리 내 모든 정리는 고전적으로 추론하고자 할 때 자유롭게 사용할 수 있습니다. Axioms and Computation에서, 배중률을 사용하여 함수를 정의하면 그 함수가 계산적으로 사용되지 못하게 될 수 있음을 살펴볼 것입니다. 따라서 표준 라이브러리는 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는 위와 같은 타입들의 패밀리입니다. 이를 통해 t가 F a₁ ... aₙ 타입일 때마다 s : t라고 쓸 수 있습니다. 다시 말해, 이 강제 변환은 F a₁ ... aₙ의 원소들을 타입으로 볼 수 있게 해 줍니다. 이는 구조체의 한 구성 요소, 즉 그 구조체의 캐리어가 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
다시 말해, 반군은 타입 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)의 인스턴스를 정의한다는 점에 유의하십시오.
함수 타입의 부류란 파이 타입 (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ₙ의 원소들을 함수로 볼 수 있습니다. 위 예제를 계속 이어서, 반군(semigroup) S1과 S2 사이의 준동형사상(morphism)이라는 개념을 정의할 수 있습니다. 즉, S1의 캐리어에서 S2의 캐리어로 가는 함수(암묵적 강제 변환에 주목하십시오)로서 곱셈을 보존하는 함수입니다. 사영(projection) 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이라는 또 다른 클래스가 있습니다. 매개변수 γ는 우리가 강제 변환하려는 대상 함수 타입을 지정하는 데 사용됩니다. 이 타입은 우리가 강제 변환하는 원래 타입에 따라 달라질 수 있습니다.