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의 검사된 예외 목록과 조금 비슷한 역할을 한다.

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