3.7. 추가 편의 기능🔗

3.7.1. 인스턴스를 위한 생성자 문법🔗

내부적으로 타입 클래스는 구조체 타입이며, 인스턴스는 이러한 타입의 값입니다. 유일한 차이점은 Lean이 어떤 매개변수가 출력 매개변수인지 등 타입 클래스에 관한 추가 정보를 저장한다는 점, 그리고 인스턴스가 검색 대상으로 등록된다는 점입니다. 구조체 타입을 갖는 값은 보통 ⟨...⟩ 문법이나 중괄호와 필드를 사용하여 정의하고, 인스턴스는 보통 where를 사용하여 정의하지만, 두 문법 모두 두 종류의 정의에 사용할 수 있습니다.

예를 들어, 임업 애플리케이션에서는 나무를 다음과 같이 표현할 수 있습니다:

structure Tree : Type where
  latinName : String
  commonNames : List String

def oak : Tree :=
  ⟨"Quercus robur", ["common oak", "European oak"]⟩

def birch : Tree :=
  { latinName := "Betula pendula",
    commonNames := ["silver birch", "warty birch"]
  }

def sloe : Tree where
  latinName := "Prunus spinosa"
  commonNames := ["sloe", "blackthorn"]

세 가지 문법은 모두 동등합니다.

마찬가지로, 타입 클래스 인스턴스도 세 가지 문법을 모두 사용하여 정의할 수 있습니다:

class Display (α : Type) where
  displayName : α → String

instance : Display Tree :=
  ⟨Tree.latinName⟩

instance : Display Tree :=
  { displayName := Tree.latinName }

instance : Display Tree where
  displayName t := t.latinName

where 문법은 일반적으로 인스턴스에 사용되며, 구조체에는 중괄호 문법이나 where 문법 중 하나를 사용합니다. ⟨...⟩ 문법은 구조체 타입이 필드에 마침 이름이 붙어 있을 뿐 그 이름이 당장은 중요하지 않은 튜플과 매우 비슷하다는 점을 강조할 때 유용합니다. 그러나 다른 대안을 사용하는 것이 합리적인 상황도 있습니다. 특히 라이브러리가 인스턴스 값을 생성하는 함수를 제공할 수 있습니다. 인스턴스 선언에서 := 뒤에 이 함수에 대한 호출을 두는 것이 그러한 함수를 사용하는 가장 쉬운 방법입니다.

3.7.2. 예제🔗

Lean 코드로 실험할 때는 #eval이나 #check 명령보다 정의를 사용하는 편이 더 편리할 수 있습니다. 우선, 정의는 아무런 출력도 만들어 내지 않으므로 독자가 가장 흥미로운 출력에 계속 집중하도록 도울 수 있습니다. 둘째로, 대부분의 Lean 프로그램은 타입 시그니처부터 작성하기 시작하는 것이 가장 쉬우며, 그렇게 하면 프로그램 자체를 작성하는 동안 Lean이 더 많은 도움과 더 나은 오류 메시지를 제공할 수 있습니다. 반면에 #eval과 #check는 Lean이 주어진 표현식으로부터 타입을 결정할 수 있는 상황에서 사용하기가 가장 쉽습니다. 셋째로, #eval은 함수처럼 타입에 ToString이나 Repr 인스턴스가 없는 표현식에는 사용할 수 없습니다. 마지막으로, 여러 단계로 이루어진 do 블록, let 표현식, 그리고 여러 줄에 걸치는 그 밖의 구문 형태는 #eval이나 #check에서 타입 표기와 함께 작성하기가 특히 어려운데, 이는 단지 필요한 괄호를 어떻게 쳐야 할지 예측하기 어려울 수 있기 때문입니다.

이러한 문제를 피하기 위해 Lean은 소스 파일 안에서 예제를 명시적으로 표시하는 기능을 지원합니다. 예제는 이름이 없는 정의와 같습니다. 예를 들어, 코펜하겐의 녹지에서 흔히 볼 수 있는 새들을 담은 비어 있지 않은 리스트는 다음과 같이 작성할 수 있습니다:

example : NonEmptyList String :=
  { head := "Sparrow",
    tail := ["Duck", "Swan", "Magpie", "Eurasian coot", "Crow"]
  }

예제에서는 인자를 받아 함수를 정의할 수도 있습니다.

example (n : Nat) (k : Nat) : Bool :=
  n + k == k + n

이렇게 하면 내부적으로 함수가 만들어지지만, 이 함수에는 이름이 없어서 호출할 수 없습니다. 그래도 이 기능은 주어진 타입의 임의의 값이나 알려지지 않은 값을 가지고 라이브러리를 어떻게 사용할 수 있는지 보여 주는 데 유용합니다. 소스 파일에서는 example 선언에 주석을 함께 다는 것이 가장 좋습니다. 그 주석에서 해당 예제가 라이브러리의 개념을 어떻게 보여 주는지 설명하십시오.