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. 또는-패턴🔗

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"

or-패턴을 사용하면 Weekday.isWeekend에서처럼 일부 정의를 크게 단순화하고 명확성을 높일 수 있습니다. 혼란스러운 동작이 발생할 가능성이 있으므로, 특히 여러 타입의 변수나 서로소인 변수 집합이 관련될 때는 이를 사용할 때 주의를 기울이는 것이 좋습니다.