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)

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

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은 특정 변수 이름을 가리킬 필요가 없습니다.