Lean에서는 패턴 매칭을 사용하여 null 검사를 연쇄적으로 수행할 수 있습니다. 리스트의 첫 번째 항목을 가져오는 것은 선택적 인덱싱 표기법을 사용하기만 하면 됩니다:

def first (xs : List α) : Option α := xs[0]?

결과는 반드시 Option이어야 합니다. 빈 리스트에는 첫 번째 항목이 없기 때문입니다. 첫 번째와 세 번째 항목을 추출하려면 각각이 none이 아닌지 확인해야 합니다:

def firstThird (xs : List α) : Option (α × α) := match xs[0]? with | none => none | some first => match xs[2]? with | none => none | some third => some (first, third)

마찬가지로, 첫 번째, 세 번째, 다섯 번째 항목을 추출하려면 값이 none이 아닌지 더 많은 검사가 필요합니다:

def firstThirdFifth (xs : List α) : Option (α × α × α) := match xs[0]? with | none => none | some first => match xs[2]? with | none => none | some third => match xs[4]? with | none => none | some fifth => some (first, third, fifth)

그리고 이 수열에 일곱 번째 항목을 추가하는 것은 상당히 다루기 어려워지기 시작합니다:

def firstThirdFifthSeventh (xs : List α) : Option (α × α × α × α) := match xs[0]? with | none => none | some first => match xs[2]? with | none => none | some third => match xs[4]? with | none => none | some fifth => match xs[6]? with | none => none | some seventh => some (first, third, fifth, seventh)

이 코드의 근본적인 문제는 숫자를 추출하는 것과 모든 숫자가 존재하는지 확인하는 것, 이렇게 두 가지 관심사를 동시에 다룬다는 데 있습니다. 두 번째 우려는 none 경우를 처리하는 코드를 복사하여 붙여넣음으로써 해결됩니다. 반복되는 부분을 헬퍼 함수로 추출하는 것이 좋은 스타일인 경우가 많습니다:

def andThen (opt : Option α) (next : α → Option β) : Option β := match opt with | none => none | some x => next x

C#과 Kotlin의 ?.와 비슷하게 사용되는 이 헬퍼는 none 값의 전파를 처리합니다. 이 함수는 두 개의 인자를 받습니다: 선택적 값과, 그 값이 none이 아닐 때 적용할 함수입니다. 첫 번째 인자가 none인 경우, 이 헬퍼는 none을 반환합니다. 첫 번째 인자가 none이 아니라면, 함수는 some 생성자의 내용에 적용됩니다.

이제 firstThird는 패턴 매칭 대신 andThen을 사용하도록 다시 작성할 수 있습니다:

def firstThird (xs : List α) : Option (α × α) := andThen xs[0]? fun first => andThen xs[2]? fun third => some (first, third)

Lean에서는 함수를 인자로 전달할 때 괄호로 둘러쌀 필요가 없습니다. 다음은 괄호를 더 많이 사용하고 함수의 본문을 들여쓴 동등한 정의입니다:

def firstThird (xs : List α) : Option (α × α) := andThen xs[0]? (fun first => andThen xs[2]? (fun third => some (first, third)))

andThen 헬퍼는 값들이 흘러가는 일종의 "파이프라인"을 제공하며, 다소 특이한 들여쓰기를 사용한 버전이 이러한 사실을 더 잘 드러냅니다. andThen을 작성할 때 사용하는 구문을 개선하면 이러한 계산을 훨씬 더 쉽게 이해할 수 있습니다.

이는 일반적으로 오류 또는 결과일 수 있는 데이터 타입을 정의하고, 예외를 사용하는 함수를 이 데이터 타입을 반환하는 함수로 변환함으로써 이루어집니다:

inductive Except (ε : Type) (α : Type) where | error : ε → Except ε α | ok : α → Except ε α deriving BEq, Hashable, Repr

타입 변수 ε는 함수가 발생시킬 수 있는 오류의 타입을 나타냅니다. 호출자는 오류와 성공을 모두 처리해야 하며, 이로 인해 타입 변수 ε는 자바(Java)의 검사 예외(checked exception) 목록과 다소 비슷한 역할을 하게 됩니다.

Option과 마찬가지로, Except도 목록에서 항목을 찾지 못했음을 나타내는 데 사용할 수 있습니다. 이 경우 오류 타입은 String입니다:

def get (xs : List α) (i : Nat) : Except String α := match xs[i]? with | none => Except.error s!"Index {i} not found (maximum is {xs.length - 1})" | some x => Except.ok x

범위 내의 값을 조회하면 Except.ok가 반환됩니다:

def ediblePlants : List String := ["ramsons", "sea plantain", "sea buckthorn", "garden nasturtium"]Except.ok "sea buckthorn"#eval get ediblePlants 2

Except.ok "sea buckthorn"

범위를 벗어난 값을 조회하면 Except.error가 반환됩니다:

Except.error "Index 4 not found (maximum is 3)"#eval get ediblePlants 4

Except.error "Index 4 not found (maximum is 3)"

단일 리스트 조회는 값 또는 오류를 편리하게 반환할 수 있습니다:

def first (xs : List α) : Except String α := get xs 0

하지만 두 번의 리스트 조회를 수행하려면 발생할 수 있는 실패를 처리해야 합니다:

def firstThird (xs : List α) : Except String (α × α) := match get xs 0 with | Except.error msg => Except.error msg | Except.ok first => match get xs 2 with | Except.error msg => Except.error msg | Except.ok third => Except.ok (first, third)

함수에 목록 조회를 하나 더 추가하려면 훨씬 더 많은 오류 처리가 필요합니다:

def firstThirdFifth (xs : List α) : Except String (α × α × α) := match get xs 0 with | Except.error msg => Except.error msg | Except.ok first => match get xs 2 with | Except.error msg => Except.error msg | Except.ok third => match get xs 4 with | Except.error msg => Except.error msg | Except.ok fifth => Except.ok (first, third, fifth)

그리고 목록 조회가 하나 더 늘어나면 상당히 감당하기 어려워지기 시작합니다:

def firstThirdFifthSeventh (xs : List α) : Except String (α × α × α × α) := match get xs 0 with | Except.error msg => Except.error msg | Except.ok first => match get xs 2 with | Except.error msg => Except.error msg | Except.ok third => match get xs 4 with | Except.error msg => Except.error msg | Except.ok fifth => match get xs 6 with | Except.error msg => Except.error msg | Except.ok seventh => Except.ok (first, third, fifth, seventh)

이번에도 공통적인 패턴을 헬퍼로 추출할 수 있습니다. 함수를 거치는 각 단계는 오류가 있는지 확인하며, 결과가 성공한 경우에만 나머지 계산을 진행합니다. andThen의 새 버전을 Except에 대해 정의할 수 있습니다:

def andThen (attempt : Except e α) (next : α → Except e β) : Except e β := match attempt with | Except.error msg => Except.error msg | Except.ok x => next x

Option과 마찬가지로, andThen의 이 버전을 사용하면 firstThird'를 더 간결하게 정의할 수 있습니다:

def firstThird' (xs : List α) : Except String (α × α) := andThen (get xs 0) fun first => andThen (get xs 2) fun third => Except.ok (first, third)

Option과 Except 경우 모두에서 반복되는 패턴이 두 가지 있습니다. 하나는 각 단계에서 중간 결과를 검사하는 것으로, 이는 andThen으로 분리되었습니다. 다른 하나는 최종 성공 결과로, 이는 각각 some과 Except.ok입니다. 편의를 위해, 성공 처리는 ok라는 헬퍼로 분리할 수 있습니다:

def ok (x : α) : Except ε α := Except.ok x

마찬가지로, 실패도 fail이라는 헬퍼로 분리할 수 있습니다:

def fail (err : ε) : Except ε α := Except.error err

ok와 fail을 사용하면 get을 조금 더 읽기 쉽게 만들 수 있습니다:

def get (xs : List α) (i : Nat) : Except String α := match xs[i]? with | none => fail s!"Index {i} not found (maximum is {xs.length - 1})" | some x => ok x

andThen에 대한 중위 선언을 추가한 후에는, firstThird도 Option을 반환하는 버전만큼이나 간결하게 작성할 수 있습니다:

infixl:55 " ~~> " => andThendef firstThird (xs : List α) : Except String (α × α) := get xs 0 ~~> fun first => get xs 2 ~~> fun third => ok (first, third)

이 기법은 더 큰 함수에도 유사하게 확장됩니다:

def firstThirdFifthSeventh (xs : List α) : Except String (α × α × α × α) := get xs 0 ~~> fun first => get xs 2 ~~> fun third => get xs 4 ~~> fun fifth => get xs 6 ~~> fun seventh => ok (first, third, fifth, seventh)

어떤 수를 2로 나누었을 때 나머지가 없으면 그 수는 짝수입니다:

def isEven (i : Int) : Bool := i % 2 == 0

sumAndFindEvens 함수는 리스트의 합을 계산하면서 그 과정에서 마주친 짝수들을 기억합니다:

def sumAndFindEvens : List Int → List Int × Int | [] => ([], 0) | i :: is => let (moreEven, sum) := sumAndFindEvens is (if isEven i then i :: moreEven else moreEven, sum + i)

이 함수는 흔히 쓰이는 패턴의 단순화된 예시입니다. 많은 프로그램은 데이터 구조를 한 번 순회하면서 주된 결과를 계산하는 동시에 일종의 부차적인 추가 결과를 누적해야 합니다. 이에 대한 한 가지 예시는 로깅입니다. IO 액션인 프로그램은 언제나 디스크의 파일에 로그를 남길 수 있지만, 디스크는 Lean 함수의 수학적 세계 바깥에 있기 때문에 IO에 기반한 로그에 대해 무언가를 증명하는 일은 훨씬 더 어려워집니다. 또 다른 예시로 중위 순회를 통해 트리의 모든 노드의 합을 계산하는 동시에 방문한 각 노드를 기록하는 함수가 있습니다:

def inorderSum : BinTree Int → List Int × Int | BinTree.leaf => ([], 0) | BinTree.branch l x r => let (leftVisited, leftSum) := inorderSum l let (hereVisited, hereSum) := ([x], x) let (rightVisited, rightSum) := inorderSum r (leftVisited ++ hereVisited ++ rightVisited, leftSum + hereSum + rightSum)

BinTree.branch
  (BinTree.branch
    (BinTree.branch (BinTree.leaf) (0, "a") (BinTree.branch (BinTree.leaf) (1, "b") (BinTree.leaf)))
    (2, "c")
    (BinTree.leaf))
  (3, "d")
  (BinTree.branch (BinTree.leaf) (4, "e") (BinTree.leaf))

트리는 재귀 함수로 처리하는 것이 가장 자연스럽지만, 트리에 대한 일반적인 재귀 패턴으로는 중위 번호를 계산하기가 어렵습니다. 이는 왼쪽 서브트리 어딘가에 할당된 가장 큰 번호가 노드의 데이터 값에 대한 번호를 정하는 데 사용된 다음, 오른쪽 서브트리의 번호 매기기를 시작할 지점을 정하는 데 다시 사용되기 때문입니다. 명령형 언어에서는 다음에 할당될 번호를 담고 있는 가변 변수를 사용하여 이 문제를 우회할 수 있습니다. 다음 Python 프로그램은 가변 변수를 사용하여 중위 순회 번호를 계산합니다:

class Branch:
    def __init__(self, value, left=None, right=None):
        self.left = left
        self.value = value
        self.right = right
    def __repr__(self):
        return f'Branch({self.value!r}, left={self.left!r}, right={self.right!r})'

def number(tree):
    num = 0
    def helper(t):
        nonlocal num
        if t is None:
            return None
        else:
            new_left = helper(t.left)
            new_value = (num, t.value)
            num += 1
            new_right = helper(t.right)
            return Branch(left=new_left, value=new_value, right=new_right)

    return helper(tree)

aTree의 Python 동등물의 번호 매기기는 다음과 같습니다:

a_tree = Branch("d",
                left=Branch("c",
                            left=Branch("a", left=None, right=Branch("b")),
                            right=None),
                right=Branch("e"))

그리고 그 번호는 다음과 같습니다:

Branch((3, 'd'), left=Branch((2, 'c'), left=Branch((0, 'a'), left=None, right=Branch((1, 'b'), left=None, right=None)), right=None), right=Branch((4, 'e'), left=None, right=None))

Python 예제가 가변 변수를 설정하는 외부 함수와 그 변수를 변경하는 내부 헬퍼 함수를 사용하는 것과 마찬가지로, Lean 버전의 함수는 변수의 시작 값을 제공하고 함수의 결과를 명시적으로 반환하는 외부 함수와, 번호가 매겨진 트리를 계산하는 동안 변수의 값을 스레딩하는 내부 헬퍼 함수를 함께 사용합니다:

def number (t : BinTree α) : BinTree (Nat × α) := let rec helper (n : Nat) : BinTree α → (Nat × BinTree (Nat × α)) | BinTree.leaf => (n, BinTree.leaf) | BinTree.branch left x right => let (k, numberedLeft) := helper n left let (i, numberedRight) := helper (k + 1) right (i, BinTree.branch numberedLeft (k, x) numberedRight) (helper 0 t).snd

이 코드는 none을 전파하는 Option 코드, error를 전파하는 Except 코드, 그리고 로그를 누적하는 WithLog 코드와 마찬가지로, 카운터의 값을 전파하는 것과 실제로 트리를 순회하여 결과를 찾는 것이라는 두 가지 관심사를 뒤섞습니다. 앞선 경우들과 마찬가지로, 계산의 한 단계에서 다른 단계로 상태를 전파하기 위해 andThen 도우미를 정의할 수 있습니다. 첫 번째 단계는 입력 상태를 인자로 받아 값과 함께 출력 상태를 반환하는 패턴에 이름을 붙이는 것입니다:

def State (σ : Type) (α : Type) : Type := σ → (σ × α)

State의 경우, ok는 입력 상태를 그대로 반환하는 함수이며, 제공된 값도 함께 반환합니다:

def ok (x : α) : State σ α := fun s => (s, x)

가변 변수를 다룰 때는 값을 읽는 것과 새 값으로 교체하는 것, 두 가지 기본 연산이 있습니다. 현재 값을 읽는 것은 입력 상태를 변경 없이 출력 상태에 넣고, 동시에 값 필드에도 넣는 함수를 통해 이루어집니다:

def get : State σ σ := fun s => (s, s)

새 값을 쓰는 것은 입력 상태를 무시하고, 제공된 새 값을 출력 상태에 넣는 것으로 이루어집니다:

def set (s : σ) : State σ Unit := fun _ => (s, ())

마지막으로, 상태를 사용하는 두 계산은 첫 번째 함수의 출력 상태와 반환값을 모두 구한 다음, 이 둘을 다음 함수에 전달함으로써 순차적으로 실행할 수 있습니다:

def andThen (first : State σ α) (next : α → State σ β) : State σ β := fun s => let (s', x) := first s next x s' infixl:55 " ~~> " => andThen

State와 그 헬퍼들을 사용하면 지역 가변 상태를 시뮬레이션할 수 있습니다:

def number (t : BinTree α) : BinTree (Nat × α) := let rec helper : BinTree α → State Nat (BinTree (Nat × α)) | BinTree.leaf => ok BinTree.leaf | BinTree.branch left x right => helper left ~~> fun numberedLeft => get ~~> fun n => set (n + 1) ~~> fun () => helper right ~~> fun numberedRight => ok (BinTree.branch numberedLeft (n, x) numberedRight) (helper t 0).snd

State는 하나의 로컬 변수만 시뮬레이션하기 때문에, get과 set은 특정 변수 이름을 참조할 필요가 없습니다.