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 선언은 해당 예제가 라이브러리의 개념을 어떻게 보여주는지 설명하는 주석과 함께 사용하는 것이 가장 좋습니다.