3.1. 양의 정수
일부 응용에서는 양수만이 의미를 가집니다. 예를 들어, 컴파일러와 인터프리터는 일반적으로 소스 위치에 대해 1부터 시작하는 줄 번호와 열 번호를 사용하며, 비어 있지 않은 리스트만을 나타내는 데이터 타입은 결코 길이 0을 보고하지 않습니다. 자연수에 의존하면서 숫자가 0이 아니라는 단언(assertion)으로 코드를 어지럽히기보다는, 양수만을 나타내는 데이터 타입을 설계하는 것이 유용할 수 있습니다.
양의 정수를 표현하는 한 가지 방법은 Nat과 매우 유사하지만, 기저 사례로 zero 대신 one을 사용합니다:
inductive Pos : Type where
| one : Pos
| succ : Pos → Pos이 데이터 타입은 의도한 값의 집합을 정확히 표현하지만, 사용하기에는 그다지 편리하지 않습니다. 예를 들어, 숫자 리터럴은 거부됩니다:
def seven : Pos := 7대신, 생성자를 직접 사용해야 합니다:
def seven : Pos :=
Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ Pos.one)))))마찬가지로, 덧셈과 곱셈도 사용하기 쉽지 않습니다:
def fourteen : Pos := seven + sevendef fortyNine : Pos := seven * seven
이 오류 메시지들은 각각 failed to synthesize로 시작합니다. 이는 오류가 구현되지 않은 오버로드된 연산으로 인한 것임을 나타내며, 구현해야 하는 타입 클래스를 설명합니다.
3.1.1. 클래스와 인스턴스
타입 클래스는 이름, 몇 가지 매개변수, 그리고 메서드들의 모음으로 구성됩니다. 매개변수는 오버로딩 가능한 연산이 정의되는 대상 타입을 기술하며, 메서드는 오버로딩 가능한 연산의 이름과 타입 시그니처입니다. 다시 한번, 객체 지향 언어들과 용어가 충돌하는 부분이 있습니다. 객체 지향 프로그래밍에서 메서드란 본질적으로 메모리상의 특정 객체와 연결되어 있으면서, 해당 객체의 비공개 상태에 대한 특별한 접근 권한을 가진 함수입니다. 객체는 자신의 메서드를 통해 상호작용됩니다. Lean에서 "메서드"라는 용어는 객체나 값, 프라이빗 필드와 특별한 관련 없이 오버로드 가능하도록 선언된 연산을 가리킵니다.
덧셈을 오버로드하는 한 가지 방법은 Plus라는 이름의 타입 클래스를 정의하고, plus라는 이름의 덧셈 메서드를 정의하는 것입니다. Nat에 대한 Plus의 인스턴스가 정의되고 나면, Plus.plus를 사용하여 두 Nat를 더하는 것이 가능해집니다:
#eval Plus.plus 5 3
인스턴스를 더 추가하면 Plus.plus가 더 다양한 유형의 인자를 받을 수 있게 됩니다.
다음 타입 클래스 선언에서 Plus는 클래스의 이름이고, α : Type은 유일한 인자이며, plus : α → α → α는 유일한 메서드입니다:
class Plus (α : Type) where
plus : α → α → α
이 선언은 타입 α에 대한 연산을 오버로드하는 타입 클래스 Plus가 존재함을 나타냅니다. 특히, 두 개의 α를 받아 하나의 α를 반환하는 plus라는 이름의 오버로드된 연산이 하나 있습니다.
타입이 일급인 것과 마찬가지로, 타입 클래스도 일급입니다. 특히, 타입 클래스는 또 다른 종류의 타입입니다. Plus의 타입은 Type → Type인데, 이는 타입을 인자(α)로 받아서 α에 대한 Plus의 연산 오버로딩을 설명하는 새로운 타입을 결과로 내놓기 때문입니다.
특정 타입에 대해 plus를 오버로드하려면 인스턴스를 작성하십시오:
instance : Plus Nat where
plus := Nat.add
instance 뒤의 콜론은 Plus Nat이 실제로 타입임을 나타냅니다. Plus 클래스의 각 메서드는 :=를 사용하여 값을 할당해야 합니다. 이 경우에는 오직 하나의 메서드, 즉 plus만 있습니다.
기본적으로 타입 클래스 메서드는 해당 타입 클래스와 같은 이름을 가진 네임스페이스에 정의됩니다. 사용자가 클래스 이름을 먼저 입력할 필요가 없도록 네임스페이스를 open하면 편리할 수 있습니다. open 명령에서 괄호는 네임스페이스에서 지정된 이름만 접근 가능하게 만들어야 함을 나타냅니다:
open Plus (plus)#eval plus 5 3
Pos에 대한 덧셈 함수를 정의하고 Plus Pos의 인스턴스를 정의하면 plus를 사용하여 Pos와 Nat 값을 모두 더할 수 있습니다:
def Pos.plus : Pos → Pos → Pos
| Pos.one, k => Pos.succ k
| Pos.succ n, k => Pos.succ (n.plus k)
instance : Plus Pos where
plus := Pos.plus
def fourteen : Pos := plus seven seven
Plus Float의 인스턴스가 아직 존재하지 않기 때문에, plus로 두 부동소수점 수를 더하려고 시도하면 익숙한 메시지와 함께 실패합니다:
#eval plus 5.2 917.25861이 오류들은 Lean이 주어진 타입 클래스에 대한 인스턴스를 찾지 못했다는 것을 의미합니다.
3.1.2. 오버로드된 덧셈
Lean의 내장 덧셈 연산자는 HAdd라는 타입 클래스에 대한 구문 설탕이며, 덧셈의 인자가 서로 다른 타입을 가질 수 있도록 유연하게 허용합니다. HAdd는 이종 덧셈(heterogeneous addition)의 줄임말입니다. 예를 들어, Nat를 Float에 더하여 새로운 Float를 만들어낼 수 있도록 HAdd 인스턴스를 작성할 수 있습니다. 프로그래머가 x + y를 작성하면, 이는 HAdd.hAdd x y를 의미하는 것으로 해석됩니다.
HAdd의 완전한 일반성을 이해하는 것은 이 장의 다른 절에서 다루는 기능들에 의존하지만, 인자의 타입이 섞이는 것을 허용하지 않는 더 단순한 타입 클래스인 Add가 있습니다. Lean 라이브러리는 두 인자의 타입이 동일한 HAdd의 인스턴스를 검색할 때 Add의 인스턴스가 발견되도록 설정되어 있습니다.
Add Pos의 인스턴스를 정의하면 Pos 값이 일반적인 덧셈 구문을 사용할 수 있습니다.
instance : Add Pos where
add := Pos.plusdef fourteen : Pos := seven + seven3.1.3. 문자열로 변환하기
또 다른 유용한 내장 클래스로 ToString이 있습니다. ToString의 인스턴스는 주어진 타입의 값을 문자열로 변환하는 표준적인 방법을 제공합니다. 예를 들어, 값이 보간된 문자열에 나타나면 ToString 인스턴스가 사용되는데, 이 인스턴스가 IO에 대한 설명의 시작 부분에서 사용된 IO.println 함수가 값을 어떻게 표시할지를 결정합니다.
예를 들어, Pos를 String으로 변환하는 한 가지 방법은 내부 구조를 드러내는 것입니다. 함수 posToString은 Pos.succ의 사용을 괄호로 묶을지 여부를 결정하는 Bool을 받으며, 이는 함수의 최초 호출에서는 true여야 하고 모든 재귀 호출에서는 false여야 합니다.
def posToString (atTop : Bool) (p : Pos) : String :=
let paren s := if atTop then s else "(" ++ s ++ ")"
match p with
| Pos.one => "Pos.one"
| Pos.succ n => paren s!"Pos.succ {posToString false n}"
이 함수를 ToString 인스턴스에 사용하면 다음과 같습니다:
instance : ToString Pos where
toString := posToString true결과는 유익하지만 압도적인 출력을 낳습니다:
#eval s!"There are {seven}"
반면에, 모든 양수에는 이에 대응하는 Nat이 존재합니다. 이를 Nat으로 변환한 다음 ToString Nat 인스턴스(즉, Nat에 대한 ToString의 오버로딩)를 사용하면 훨씬 더 짧은 출력을 빠르게 생성할 수 있습니다:
def Pos.toNat : Pos → Nat
| Pos.one => 1
| Pos.succ n => n.toNat + 1instance : ToString Pos where
toString x := toString (x.toNat)#eval s!"There are {seven}"
인스턴스가 둘 이상 정의된 경우, 가장 최근에 정의된 것이 우선합니다. 또한, 어떤 타입이 ToString 인스턴스를 가지고 있다면 이를 사용해 #eval의 결과를 표시할 수 있으므로, #eval seven은 7을 출력합니다.
3.1.4. 오버로딩된 곱셈
곱셈의 경우, HAdd와 마찬가지로 인자 타입을 혼합할 수 있도록 허용하는 HMul이라는 타입 클래스가 있습니다. x + y가 HAdd.hAdd x y로 해석되는 것과 마찬가지로, x * y는 HMul.hMul x y로 해석됩니다. 동일한 타입을 가진 두 인자의 곱셈이라는 일반적인 경우에는 Mul 인스턴스로 충분합니다.
Mul의 인스턴스는 Pos에서도 일반적인 곱셈 구문을 사용할 수 있게 해 줍니다:
def Pos.mul : Pos → Pos → Pos
| Pos.one, k => k
| Pos.succ n, k => n.mul k + k
instance : Mul Pos where
mul := Pos.mul이 인스턴스를 사용하면 곱셈이 예상대로 작동합니다:
#eval [seven * Pos.one,
seven * seven,
Pos.succ Pos.one * seven]3.1.5. 리터럴 숫자
양의 정수를 나타내기 위해 생성자를 연속으로 나열해 작성하는 것은 상당히 불편합니다. 이 문제를 우회하는 한 가지 방법은 Nat을 Pos로 변환하는 함수를 제공하는 것입니다. 그러나 이 접근 방식에는 단점이 있습니다. 우선, Pos는 0을 표현할 수 없으므로, 결과 함수는 Nat을 더 큰 수로 변환하거나, Option Pos를 반환해야 할 것입니다. 둘 다 사용자에게 특별히 편리하지는 않습니다. 둘째, 함수를 명시적으로 호출해야 한다면 양수를 사용하는 프로그램은 Nat를 사용하는 프로그램보다 작성하기가 훨씬 불편해질 것입니다. 정밀한 타입과 편리한 API 사이의 트레이드오프가 존재한다는 것은 정밀한 타입의 유용성이 떨어진다는 것을 의미합니다.
숫자 리터럴을 오버로드하는 데 사용되는 타입 클래스는 Zero, One, OfNat 세 가지입니다. 많은 타입에는 0으로 자연스럽게 쓰이는 값들이 있기 때문에, Zero 클래스는 이러한 특정 값들을 재정의할 수 있도록 허용합니다. 이는 다음과 같이 정의됩니다:
class Zero (α : Type) where
zero : α
0은 양수가 아니므로, Zero Pos의 인스턴스가 존재해서는 안 됩니다.
마찬가지로, 많은 타입에는 1로 자연스럽게 표기되는 값들이 있습니다. One 클래스를 사용하면 이러한 항목들을 재정의할 수 있습니다:
class One (α : Type) where
one : α
One Pos의 인스턴스는 완벽하게 타당합니다:
instance : One Pos where
one := Pos.one
이 인스턴스가 있으면, 1을 Pos.one의 자리에 사용할 수 있습니다:
#eval (1 : Pos)
Lean에서 자연수 리터럴은 OfNat이라는 타입 클래스를 사용하여 해석됩니다:
class OfNat (α : Type) (_ : Nat) where
ofNat : α
이 타입 클래스는 두 개의 인자를 받습니다: α는 자연수가 오버로드되는 대상 타입이고, 이름 없는 Nat 인자는 프로그램에서 발견된 실제 리터럴 숫자입니다. 그다음 ofNat 메서드가 숫자 리터럴의 값으로 사용됩니다. 이 클래스는 Nat 인자를 포함하므로, 숫자가 의미를 갖는 값에 대해서만 인스턴스를 정의하는 것이 가능해집니다.
OfNat은 타입 클래스의 인자가 반드시 타입일 필요는 없다는 것을 보여줍니다. Lean의 타입은 함수의 인자로 전달될 수 있고 def와 abbrev로 정의될 수 있는, 언어 내의 일급 참여자이므로, 유연성이 떨어지는 언어라면 허용하지 못했을 위치에 타입이 아닌 인자가 오는 것을 막는 장벽이 존재하지 않습니다. 이러한 유연성 덕분에 특정 타입뿐 아니라 특정 값에 대해서도 오버로드된 연산을 제공할 수 있습니다. 또한 이를 통해 Lean 표준 라이브러리는 OfNat α 0 인스턴스가 있을 때마다 Zero α 인스턴스가 존재하도록, 그리고 그 반대의 경우도 성립하도록 정리할 수 있습니다. 마찬가지로, OfNat α 1의 인스턴스가 One α의 인스턴스를 함의하는 것처럼, One α의 인스턴스는 OfNat α 1의 인스턴스를 함의합니다.
4보다 작은 자연수를 나타내는 합 타입은 다음과 같이 정의할 수 있습니다:
inductive LT4 where
| zero
| one
| two
| three이 타입에 어떤 리터럴 숫자든 사용할 수 있도록 허용하는 것은 말이 되지 않겠지만, 4보다 작은 숫자는 명백히 말이 됩니다:
instance : OfNat LT4 0 where
ofNat := LT4.zero
instance : OfNat LT4 1 where
ofNat := LT4.one
instance : OfNat LT4 2 where
ofNat := LT4.two
instance : OfNat LT4 3 where
ofNat := LT4.three이 인스턴스들이 있으면 다음 예제가 동작합니다:
#eval (3 : LT4)#eval (0 : LT4)반면, 범위를 벗어난 리터럴은 여전히 허용되지 않습니다:
#eval (4 : LT4)
Pos의 경우, OfNat 인스턴스는 Nat.zero를 제외한 any Nat에 대해 작동해야 합니다. 이를 다르게 표현하면, 모든 자연수 n에 대해 이 인스턴스가 n + 1에서도 작동해야 한다고 말할 수 있습니다. α와 같은 이름이 Lean이 스스로 채워 넣는 함수의 암시적 인자로 자동으로 바뀌는 것처럼, 인스턴스도 자동 암시적 인자를 받을 수 있습니다. 이 인스턴스에서 인자 n은 임의의 Nat를 나타내며, 이 인스턴스는 그보다 1 큰 Nat에 대해 정의됩니다:
instance : OfNat Pos (n + 1) where
ofNat :=
let rec natPlusOne : Nat → Pos
| 0 => Pos.one
| k + 1 => Pos.succ (natPlusOne k)
natPlusOne n
n은 사용자가 작성한 것보다 1 작은 Nat을 나타내기 때문에, 도우미 함수 natPlusOne은 인자보다 1 큰 Pos를 반환합니다. 이를 통해 자연수 리터럴을 양수에는 사용할 수 있지만, 0에는 사용할 수 없습니다:
def eight : Pos := 8def zero : Pos := 03.1.6. 연습문제
3.1.6.1. 또 다른 표현
양의 정수를 표현하는 대안적인 방법은 어떤 Nat의 후행자로 표현하는 것입니다. Pos의 정의를 Nat를 포함하며 생성자 이름이 succ인 구조체로 교체하십시오:
structure Pos where
succ ::
pred : Nat
Add, Mul, ToString, OfNat의 인스턴스를 정의하여 이 버전의 Pos를 편리하게 사용할 수 있도록 하십시오.
3.1.6.2. 짝수
짝수만을 나타내는 데이터 타입을 정의하십시오. 이를 편리하게 사용할 수 있도록 Add, Mul, ToString의 인스턴스를 정의하십시오. OfNat은 다음 절에서 소개되는 기능을 필요로 합니다.
3.1.6.3. HTTP 요청
HTTP 요청은 GET이나 POST와 같은 HTTP 메서드의 식별자로 시작하며, 여기에 URI와 HTTP 버전이 함께 표시됩니다. HTTP 메서드 중 흥미로운 부분 집합을 나타내는 귀납적 타입과, HTTP 응답을 나타내는 구조체를 정의하십시오. 응답에는 디버깅을 가능하게 하는 ToString 인스턴스가 있어야 합니다. 타입 클래스를 사용하여 각 HTTP 메서드에 서로 다른 IO 액션을 연결하고, 각 메서드를 호출하여 결과를 출력하는 IO 액션으로 테스트 도구를 작성하십시오.