4.6. 추가 편의 기능🔗

4.6.1. 공유 인자 타입🔗

같은 타입의 인자를 여러 개 받는 함수를 정의할 때는 그 인자들을 하나의 콜론 앞에 함께 쓸 수 있습니다. 예를 들어,

def equal? [BEq α] (x : α) (y : α) : Option α :=
  if x == y then
    some x
  else
    none

다음과 같이 작성할 수 있습니다

def equal? [BEq α] (x y : α) : Option α :=
  if x == y then
    some x
  else
    none

이는 타입 시그니처가 클 때 특히 유용합니다.

4.6.2. 선행 점 표기법🔗

귀납적 타입의 생성자는 네임스페이스 안에 있습니다. 덕분에 서로 관련된 여러 귀납적 타입이 같은 생성자 이름을 쓸 수 있지만, 프로그램이 장황해질 수 있습니다. 해당 귀납적 타입이 무엇인지 알려진 문맥에서는 생성자 이름 앞에 점을 붙여 네임스페이스를 생략할 수 있으며, Lean은 기대 타입을 사용해 생성자 이름을 해석합니다. 예를 들어, 이진 트리를 좌우 반전하는 함수는 다음과 같이 작성할 수 있습니다.

def BinTree.mirror : BinTree α → BinTree α
  | BinTree.leaf => BinTree.leaf
  | BinTree.branch l x r => BinTree.branch (mirror r) x (mirror l)

네임스페이스를 생략하면 프로그램이 상당히 짧아지지만, 그 대신 Lean 컴파일러가 없는 코드 리뷰 도구 같은 환경에서는 프로그램을 읽기가 더 어려워집니다:

def BinTree.mirror : BinTree α → BinTree α
  | .leaf => .leaf
  | .branch l x r => .branch (mirror r) x (mirror l)

표현식의 기대 타입을 사용해 네임스페이스를 명확히 하는 방식은 생성자가 아닌 다른 이름에도 적용할 수 있습니다. BinTree.empty가 BinTree를 만드는 또 다른 방법으로 정의되어 있다면, 이것 역시 점 표기법과 함께 사용할 수 있습니다:

def BinTree.empty : BinTree α := .leafBinTree.empty : BinTree Nat#check (.empty : BinTree Nat)

BinTree.empty : BinTree Nat

4.6.3. Or-패턴🔗

match 표현식처럼 여러 패턴을 허용하는 문맥에서는 여러 패턴이 결과 표현식을 공유할 수 있습니다. 요일을 나타내는 데이터 타입 Weekday는 다음과 같습니다:

inductive Weekday where
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday
deriving Repr

패턴 매칭을 사용하여 어떤 요일이 주말인지 확인할 수 있습니다:

def Weekday.isWeekend (day : Weekday) : Bool :=
  match day with
  | Weekday.saturday => true
  | Weekday.sunday => true
  | _ => false

이는 생성자 점 표기법을 사용하면 벌써 간단하게 만들 수 있습니다:

def Weekday.isWeekend (day : Weekday) : Bool :=
  match day with
  | .saturday => true
  | .sunday => true
  | _ => false

두 주말 패턴의 결과 표현식(true)이 같으므로 이 둘을 하나로 합칠 수 있습니다:

def Weekday.isWeekend (day : Weekday) : Bool :=
  match day with
  | .saturday | .sunday => true
  | _ => false

이는 인자에 이름을 붙이지 않는 형태로 더 간단하게 줄일 수 있습니다:

def Weekday.isWeekend : Weekday → Bool
  | .saturday | .sunday => true
  | _ => false

내부적으로는 결과 표현식이 각 패턴마다 그대로 복제됩니다. 이는 패턴이 변수를 바인딩할 수 있다는 것을 의미합니다. 다음 예제는 두 생성자 모두 같은 타입의 값을 담고 있는 합 타입에서 inl 생성자와 inr 생성자를 제거합니다:

def condense : α ⊕ α → α
  | .inl x | .inr x => x

결과 표현식이 복제되기 때문에, 패턴이 바인딩하는 변수들이 같은 타입을 가질 필요는 없습니다. 여러 타입에 대해 동작하는 오버로드된 함수를 사용하면, 서로 다른 타입의 변수를 바인딩하는 패턴들에 모두 적용되는 하나의 결과 표현식을 작성할 수 있습니다:

def stringy : Nat ⊕ Weekday → String
  | .inl x | .inr x => s!"It is {repr x}"

실제로는 모든 패턴에서 공통으로 나타나는 변수만 결과 표현식에서 참조할 수 있습니다. 결과가 각 패턴에 대해 의미가 있어야 하기 때문입니다. getTheNat에서는 n에만 접근할 수 있으며, x나 y를 사용하려고 하면 오류가 발생합니다.

def getTheNat : (Nat × α) ⊕ (Nat × β) → Nat
  | .inl (n, x) | .inr (n, y) => n

비슷한 정의에서 x에 접근하려고 하면 두 번째 패턴에는 사용할 수 있는 x가 없으므로 오류가 발생합니다:

def getTheAlpha : (Nat × α) ⊕ (Nat × α) → α
  | .inl (n, x) | .inr (n, y) => Unknown identifier `x`x

Unknown identifier `x`

결과 표현식이 사실상 패턴 매칭의 각 분기에 그대로 복사되어 붙여넣어진다는 사실은 때때로 놀라운 동작으로 이어질 수 있습니다. 예를 들어, 다음 정의들은 허용되는데, 결과 표현식의 inr 버전이 str의 전역 정의를 참조하기 때문입니다:

def str := "Some string"

def getTheString : (Nat × String) ⊕ (Nat × β) → String
  | .inl (n, str) | .inr (n, y) => str

이 함수를 두 생성자에 대해 호출해 보면 혼란스러운 동작이 드러납니다. 첫 번째 경우에는 β가 어떤 타입이어야 하는지 Lean에 알려 주기 위해 타입 표기가 필요합니다:

"twenty"#eval getTheString (.inl (20, "twenty") : (Nat × String) ⊕ (Nat × String))

"twenty"

두 번째 경우에는 전역 정의가 사용됩니다:

"Some string"#eval getTheString (.inr (20, "twenty"))

"Some string"

Weekday.isWeekend에서처럼 or-패턴을 사용하면 일부 정의를 크게 단순화하고 더 명확하게 만들 수 있습니다. 다만 혼란스러운 동작이 나타날 수 있으므로 사용할 때 주의하는 것이 좋습니다. 특히 여러 타입의 변수가 관련되거나 서로 겹치지 않는 변수 집합이 관련된 경우에는 더욱 주의해야 합니다.