3.1. Positive Numbers
일부 응용에서는 양수만 의미가 있다. 예를 들어 컴파일러와 인터프리터는 보통 소스 위치에 1부터 시작하는 줄·열 번호를 사용하며, 비어 있지 않은 리스트만 표현하는 데이터 타입은 길이가 0이라고 보고하지 않는다. 자연수에 의존하고 수가 0이 아니라는 단언을 코드 곳곳에 넣는 대신, 양수만 표현하는 데이터 타입을 설계하면 유용하다.
양수를 표현하는 한 가지 방법은 zero 대신 one을 기본 경우로 둔다는 점을 제외하면 Nat과 매우 비슷하다.
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. Classes and Instances
타입 클래스는 이름과 매개변수, 메서드 모음으로 이루어진다. 매개변수는 오버로딩할 연산을 정의할 타입을 설명하고, 메서드는 오버로딩할 연산의 이름과 타입 시그니처다. 여기서도 객체 지향 언어와 용어가 충돌한다. 객체 지향 프로그래밍에서 메서드는 메모리의 특정 객체와 연결되어 객체의 private 상태에 특별히 접근하는 함수다. 객체와 상호작용할 때 메서드를 사용한다. Lean에서 “메서드”는 오버로딩 가능하다고 선언된 연산을 뜻할 뿐, 객체나 값, private 필드와 특별히 연결되지 않는다.
덧셈을 오버로딩하는 한 가지 방법은 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. Overloaded Addition
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. Conversion to Strings
또 다른 유용한 내장 클래스는 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으로 변환한 다음 Nat에 대한 ToString 오버로딩인 ToString Nat 인스턴스를 사용하면 훨씬 짧은 출력을 빠르게 만들 수 있다.
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. Overloaded Multiplication
곱셈에는 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. Literal Numbers
양수의 생성자를 줄줄이 쓰는 것은 매우 불편하다.
한 가지 해결책은 Nat을 Pos로 바꾸는 함수를 제공하는 것이다.
하지만 이 방법에는 단점이 있다.
첫째, Pos는 0을 표현할 수 없으므로 함수가 Nat을 더 큰 수로 바꾸거나 Option Pos를 반환해야 한다.
어느 쪽도 사용자에게 특별히 편리하지 않다.
둘째, 함수를 명시적으로 호출해야 하므로 양수를 사용하는 프로그램은 Nat을 사용하는 프로그램보다 작성하기 훨씬 불편해진다.
정확한 타입과 편리한 API 사이에서 절충하면 정확한 타입의 유용성이 떨어진다.
숫자 리터럴을 오버로딩하는 타입 클래스는 Zero, One, OfNat 세 가지다.
많은 타입에는 자연스럽게 0으로 쓰는 값이 있으므로 Zero 클래스는 각 타입이 숫자 0으로 나타낼 구체적인 값을 정할 수 있게 한다.
정의는 다음과 같다.
class Zero (α : Type) where
zero : α
0은 양수가 아니므로 Zero Pos 인스턴스는 없어야 한다.
마찬가지로 많은 타입에는 자연스럽게 1로 쓰는 값이 있다.
One 클래스는 각 타입이 숫자 1로 나타낼 구체적인 값을 정할 수 있게 한다.
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 α 인스턴스도, 그 반대도 성립하도록 구성할 수 있다.
마찬가지로 One α 인스턴스는 OfNat α 1 인스턴스를 뜻하고, OfNat α 1 인스턴스는 One α 인스턴스를 뜻한다.
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가 아닌 어떤 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. Exercises
3.1.6.1. Another Representation
양수를 표현하는 다른 방법은 어떤 Nat의 후속 수로 표현하는 것이다.
Pos 정의를 Nat을 포함하고 생성자 이름이 succ인 구조체로 바꾸어라.
structure Pos where
succ ::
pred : Nat
이 버전의 Pos를 편리하게 사용할 수 있도록 Add, Mul, ToString, OfNat 인스턴스를 정의하라.
3.1.6.2. Even Numbers
짝수만 표현하는 데이터 타입을 정의하라. 편리하게 사용할 수 있도록 Add, Mul, ToString 인스턴스를 정의하라.
OfNat에는 다음 절에서 소개하는 기능이 필요하다.
3.1.6.3. HTTP Requests
HTTP 요청은 GET이나 POST 같은 HTTP 메서드와 URI, HTTP 버전으로 시작한다.
HTTP 메서드의 흥미로운 부분집합을 표현하는 귀납 타입과 HTTP 응답을 표현하는 구조체를 정의하라.
응답에 디버깅할 수 있게 하는 ToString 인스턴스를 제공하라.
타입 클래스로 각 HTTP 메서드에 서로 다른 IO 동작을 연결하고, 각 메서드를 호출해 결과를 출력하는 테스트 하니스를 IO 동작으로 작성하라.