4.6. Additional Conveniences🔗

4.6.1. Shared Argument Types🔗

같은 타입을 갖는 여러 인수를 받는 함수를 정의할 때는 같은 콜론 앞에 인수를 함께 쓸 수 있다. 예를 들어 다음과 같다.

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. Leading Dot Notation🔗

귀납 타입의 생성자는 네임스페이스 안에 있다. 이 덕분에 서로 관련된 여러 귀납 타입이 같은 생성자 이름을 사용할 수 있지만, 프로그램이 장황해질 수 있다. 해당 귀납 타입을 알고 있는 문맥에서는 생성자 이름 앞에 점을 붙여 네임스페이스를 생략할 수 있으며, 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-Patterns🔗

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 패턴을 사용하면 일부 정의를 크게 간소화하고 명확하게 만들 수 있다. 혼란스러운 동작이 생길 가능성이 있으므로, 특히 여러 타입의 변수나 서로 겹치지 않는 변수 집합이 관련된 경우에는 주의해서 사용하는 것이 좋다.