3.7. Additional Conveniences
3.7.1. Constructor Syntax for Instances
내부적으로 타입 클래스는 구조체 타입이고 인스턴스는 그 타입의 값이다.
차이는 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. Examples
Lean 코드를 실험할 때는 #eval이나 #check 명령보다 정의가 편리할 수 있다.
첫째, 정의는 출력을 만들지 않아 독자가 가장 흥미로운 출력에 집중하게 한다.
둘째, 타입 시그니처부터 시작하면 Lean이 프로그램 작성 중 더 많은 도움과 나은 오류 메시지를 제공하므로 대부분의 Lean 프로그램을 쉽게 작성할 수 있다.
반면 #eval과 #check는 제공된 표현식에서 Lean이 타입을 알아낼 수 있는 문맥에서 사용하기 쉽다.
셋째, 함수처럼 ToString이나 Repr 인스턴스가 없는 타입의 표현식에는 #eval을 사용할 수 없다.
마지막으로 여러 줄을 차지하는 다단계 do 블록, let 표현식 및 다른 문법 형식은 필요한 괄호를 예측하기 어려워 #eval이나 #check에서 타입 주석과 함께 작성하기 특히 어렵다.