3.1.1. 클래스와 인스턴스🔗

타입 클래스는 이름, 몇 가지 매개변수, 그리고 메서드의 모음으로 구성됩니다. 매개변수는 오버로드 가능한 연산이 정의되는 대상 타입을 나타내고, 메서드는 오버로드 가능한 연산의 이름과 타입 시그니처입니다. 이번에도 객체 지향 언어와 용어가 충돌합니다. 객체 지향 프로그래밍에서 메서드는 본질적으로 메모리상의 특정 객체에 연결된 함수이며, 그 객체의 비공개 상태에 특별히 접근할 수 있습니다. 객체와의 상호작용은 해당 객체의 메서드를 통해 이루어집니다. Lean에서 “메서드”라는 용어는 오버로드 가능하다고 선언된 연산을 가리키며, 객체나 값 또는 비공개 필드와는 특별한 관련이 없습니다.

덧셈을 오버로드하는 한 가지 방법은 plus라는 덧셈 메서드를 가진 Plus라는 타입 클래스를 정의하는 것입니다. Nat에 대한 Plus 인스턴스를 정의하고 나면 Plus.plus를 사용하여 두 Nat 값을 더할 수 있습니다:

8

인스턴스를 더 추가하면 Plus.plus가 더 다양한 타입의 인자를 받을 수 있게 됩니다.

다음 타입 클래스 선언에서 Plus는 클래스의 이름이고, α : Type은 유일한 인자이며, plus : α → α → α는 유일한 메서드입니다:

이 선언은 타입 α에 대해 연산을 오버로드하는 타입 클래스 Plus가 있다는 것을 나타냅니다. 구체적으로는 α 두 개를 받아 α를 반환하는 plus라는 오버로드된 연산이 하나 있습니다.

타입이 일급인 것과 마찬가지로 타입 클래스도 일급입니다. 특히 타입 클래스는 또 다른 종류의 타입입니다. Plus의 타입은 Type → Type입니다. 타입 하나를 인자(α)로 받아, α에 대한 Plus 연산의 오버로딩을 기술하는 새로운 타입을 결과로 내놓기 때문입니다.

특정 타입에 대해 plus를 오버로드하려면 인스턴스를 작성하십시오:

instance 뒤의 콜론은 Plus Nat이 실제로 타입임을 나타냅니다. Plus 클래스의 각 메서드에는 :=를 사용해 값을 할당해야 합니다. 이 경우에는 메서드가 plus 하나뿐입니다.

기본적으로 타입 클래스 메서드는 해당 타입 클래스와 같은 이름의 네임스페이스 안에 정의됩니다. 사용자가 타입 클래스 이름을 먼저 입력하지 않아도 되도록 네임스페이스를 open하면 편리할 수 있습니다. open 명령에 괄호를 쓰면 네임스페이스에서 괄호 안에 지정한 이름만 접근할 수 있게 됩니다:

8

Pos에 대한 덧셈 함수와 Plus Pos 인스턴스를 정의하면 plus를 사용하여 Pos 값과 Nat 값을 모두 더할 수 있습니다:

아직 Plus Float 인스턴스가 없기 때문에, plus로 두 부동소수점 수를 더하려고 하면 익숙한 메시지와 함께 실패합니다:

failed to synthesize instance of type class
  Plus Float

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

이 오류들은 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 값에 일반적인 덧셈 문법을 사용할 수 있습니다.

3.1.3. 문자열로 변환하기🔗

또 다른 유용한 내장 클래스로 ToString이 있습니다. ToString의 인스턴스는 주어진 타입의 값을 문자열로 변환하는 표준 방법을 제공합니다. 예를 들어, 값이 보간 문자열 안에 나타나면 ToString 인스턴스가 사용되며, 이 인스턴스는 IO에 대한 설명의 시작 부분에서 사용한 IO.println 함수가 값을 어떻게 표시할지를 결정합니다.

예를 들어, Pos를 String으로 변환하는 한 가지 방법은 그 내부 구조를 드러내는 것입니다. posToString 함수는 Pos.succ의 사용을 괄호로 감쌀지 여부를 결정하는 Bool을 인자로 받습니다. 이 값은 함수를 처음 호출할 때는 true여야 하고, 모든 재귀 호출에서는 false여야 합니다.

이 함수를 사용하여 ToString 인스턴스를 정의하면 다음과 같습니다.

유익하지만 감당하기 어려울 만큼 많은 출력을 냅니다:

"There are Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ Pos.one)))))"

반면에, 모든 양수에는 그에 대응하는 Nat이 있습니다. 양수를 Nat으로 변환한 다음 ToString Nat 인스턴스(즉, Nat에 대한 ToString의 오버로딩)를 사용하면 훨씬 짧은 출력을 빠르게 생성할 수 있습니다:

"There are 7"

인스턴스가 둘 이상 정의되어 있으면 가장 최근에 정의된 인스턴스가 우선합니다. 또한 어떤 타입에 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에 일반적인 곱셈 문법을 사용할 수 있습니다:

이 인스턴스를 사용하면 곱셈이 예상대로 동작합니다:

[7, 49, 14]

3.1.5. 숫자 리터럴🔗

양수를 표현하기 위해 생성자를 일일이 나열해 작성하는 것은 상당히 불편합니다. 이 문제를 우회하는 한 가지 방법은 Nat을 Pos로 변환하는 함수를 제공하는 것입니다. 하지만 이 방식에는 단점이 있습니다. 우선, Pos는 0을 표현할 수 없으므로, 이렇게 만든 함수는 Nat을 더 큰 수로 변환하거나 Option Pos를 반환해야 합니다. 어느 쪽도 사용자에게 딱히 편리하지 않습니다. 둘째로, 함수를 명시적으로 호출해야 하므로 양수를 사용하는 프로그램은 Nat을 사용하는 프로그램보다 작성하기가 훨씬 불편해집니다. 정밀한 타입과 편리한 API 사이에서 하나를 포기해야 한다면 정밀한 타입의 유용성이 떨어지게 됩니다.

숫자 리터럴을 오버로드하는 데 쓰이는 타입 클래스는 Zero, One, OfNat의 세 가지입니다. 많은 타입에는 0으로 쓰는 것이 자연스러운 값이 있으므로, Zero 클래스를 사용하면 이러한 특정 값을 재정의할 수 있습니다. 정의는 다음과 같습니다:

0은 양수가 아니므로 Zero Pos 인스턴스는 존재해서는 안 됩니다.

마찬가지로, 많은 타입에는 1로 쓰는 것이 자연스러운 값이 있습니다. One 클래스를 사용하면 이러한 값을 재정의할 수 있습니다:

One Pos 인스턴스는 충분히 타당합니다:

이 인스턴스를 사용하면 Pos.one 대신 1을 쓸 수 있습니다:

1

Lean에서 자연수 리터럴은 OfNat이라는 타입 클래스를 사용하여 해석됩니다:

이 타입 클래스는 두 개의 인자를 받습니다. α는 자연수가 오버로드되는 타입이고, 이름 없는 Nat 인자는 프로그램에서 실제로 나타난 숫자 리터럴입니다. 그런 다음 ofNat 메서드가 숫자 리터럴의 값으로 사용됩니다. 클래스가 Nat 인자를 포함하므로, 그 숫자가 의미를 갖는 값에 대해서만 인스턴스를 정의할 수 있게 됩니다.

OfNat은 타입 클래스의 인자가 반드시 타입일 필요는 없다는 것을 보여 줍니다. Lean에서 타입은 함수에 인자로 전달될 수 있고 def와 abbrev로 정의를 부여받을 수 있는 언어의 일급 구성원이므로, 덜 유연한 언어라면 허용하지 않을 위치에 타입이 아닌 인자가 오는 것을 막는 장벽이 없습니다. 즉, 타입 클래스에 대한 타입 인자뿐 아니라 타입이 아닌 인자도 쓸 수 있습니다. 이러한 유연성 덕분에 오버로드된 연산을 특정 타입뿐만 아니라 특정 값에 대해서도 제공할 수 있습니다. 또한 이를 통해 Lean 표준 라이브러리는 OfNat α 0 인스턴스가 있을 때마다 Zero α 인스턴스가 존재하도록, 그리고 그 반대도 성립하도록 구성할 수 있습니다. 마찬가지로 OfNat α 1 인스턴스가 One α 인스턴스를 함의하는 것처럼, One α 인스턴스는 OfNat α 1 인스턴스를 함의합니다.

4보다 작은 자연수를 나타내는 합 타입은 다음과 같이 정의할 수 있습니다:

이 타입에 임의의 숫자 리터럴을 허용하는 것은 말이 되지 않지만, 4보다 작은 숫자는 분명히 의미가 있습니다:

이러한 인스턴스가 있으면 다음 예제가 동작합니다:

LT4.three

LT4.zero

반면, 범위를 벗어난 리터럴은 여전히 허용되지 않습니다:

failed to synthesize instance of type class
  OfNat LT4 4
numerals are polymorphic in Lean, but the numeral `4` cannot be used in a context where the expected type is
  LT4
due to the absence of the instance above

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

Pos의 경우, OfNat 인스턴스는 Nat.zero를 제외한 모든 Nat에 대해 동작해야 합니다. 이를 달리 표현하면, 모든 자연수 n에 대해 인스턴스가 n + 1에 대해 동작해야 한다고 말할 수 있습니다. α와 같은 이름이 자동으로 함수의 암시적 인자가 되어 Lean이 스스로 채워 넣는 것처럼, 인스턴스도 자동 암시적 인자를 받을 수 있습니다. 이 인스턴스에서 인자 n은 임의의 Nat을 나타내며, 인스턴스는 그보다 1 큰 Nat에 대해 정의됩니다:

n은 사용자가 작성한 값보다 1 작은 Nat을 나타내므로, 보조 함수 natPlusOne은 인자보다 1 큰 Pos를 반환합니다. 이렇게 하면 양수에는 자연수 리터럴을 사용할 수 있지만 0에는 사용할 수 없습니다:

failed to synthesize instance of type class
  OfNat Pos 0
numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
  Pos
due to the absence of the instance above

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

3.1.6. 연습 문제🔗