7.3.2.1. 재귀와 유니버스 다시 살펴보기🔗

행을 튜플로 구조화하면 편리하지만 그만한 대가가 따릅니다. Row가 두 기저 사례를 따로 처리한다는 것은, 타입에 Row를 사용하면서 코드(즉, 스키마)에 대해 재귀적으로 정의되는 함수도 같은 구분을 해야 한다는 뜻입니다. 이 점이 문제가 되는 예로, 스키마에 대한 재귀를 사용해 두 행이 같은지 검사하는 함수를 정의하는 동등성 검사가 있습니다. 이 예제는 Lean의 타입 검사기를 통과하지 못합니다:

Type mismatch
  (v1, r1')
has type
  ?m.10 × ?m.11
but is expected to have type
  Row (col :: cols)

문제는 col :: cols 패턴이 행의 타입을 충분히 구체화하지 못한다는 점입니다. 이는 Row의 정의에서 단일 원소 패턴 [col]과 col1 :: col2 :: cols 패턴 중 어느 쪽이 매칭되었는지 Lean이 아직 알 수 없기 때문이며, 그래서 Row 호출이 쌍 타입으로까지 계산되지 않습니다. 해결책은 Row.bEq의 정의에 Row의 구조를 그대로 반영하는 것입니다:

다른 맥락에서와 달리, 타입에 등장하는 함수는 입력/출력 동작만으로 판단할 수 없습니다. 이러한 타입을 사용하는 프로그램은 그 구조가 타입의 패턴 매칭 및 재귀 동작과 맞아떨어지도록, 타입 수준 함수에서 사용된 알고리즘을 그대로 따를 수밖에 없게 됩니다. 의존 타입으로 프로그래밍하는 기술의 상당 부분은 올바른 계산 동작을 갖춘 적절한 타입 수준 함수를 고르는 데 있습니다.

7.3.2.2. 열 포인터🔗

어떤 쿼리는 스키마에 특정 열이 포함되어 있을 때에만 의미가 있습니다. 예를 들어, 고도가 1000미터보다 높은 산을 반환하는 쿼리는 정수를 담는 "elevation" 열이 있는 스키마의 맥락에서만 의미가 있습니다. 스키마에 어떤 열이 포함되어 있음을 나타내는 한 가지 방법은 그 열을 직접 가리키는 포인터를 제공하는 것이며, 이 포인터를 인덱스 족(indexed family)으로 정의하면 유효하지 않은 포인터를 배제할 수 있습니다.

열이 스키마에 존재할 수 있는 방식은 두 가지입니다. 스키마의 맨 앞에 있거나, 스키마의 뒤쪽 어딘가에 있는 것입니다. 어떤 열이 스키마의 뒤쪽에 있다면, 결국 그 열은 스키마의 어떤 꼬리 부분의 맨 앞이 됩니다.

인덱스 족 HasCol은 이 명세를 Lean 코드로 옮긴 것입니다.

이 족(family)의 세 인자는 스키마, 열 이름, 그리고 그 열의 타입입니다. 세 인자 모두 인덱스이지만, 인자의 순서를 바꾸어 스키마를 열 이름과 타입 뒤에 두면 이름과 타입을 매개변수로 만들 수 있습니다. 생성자 here는 스키마가 열 ⟨name, t⟩로 시작할 때 사용할 수 있습니다. 따라서 이 생성자는 스키마의 첫 번째 열을 가리키는 포인터이며, 첫 번째 열이 원하는 이름과 타입을 가질 때에만 사용할 수 있습니다. 생성자 there는 더 작은 스키마를 가리키는 포인터를 열이 하나 더 있는 스키마를 가리키는 포인터로 변환합니다.

"elevation"은 peak의 세 번째 열이므로 there로 처음 두 열을 건너뛰면 찾을 수 있습니다. 두 열을 건너뛰고 나면 이 열이 첫 번째 열이 됩니다. 다시 말해, HasCol peak "elevation" .int 타입을 만족시키려면 .there (.there .here) 표현식을 사용하면 됩니다. HasCol은 일종의 장식된 Nat으로 생각할 수 있습니다. zero는 here에 대응하고, succ는 there에 대응합니다. 추가된 타입 정보 덕분에 하나 차이 오류(off-by-one error)가 생길 수 없습니다.

스키마의 특정 열을 가리키는 포인터를 사용하면 행에서 해당 열의 값을 추출할 수 있습니다:

첫 번째 단계는 스키마에 대해 패턴 매칭을 하는 것입니다. 스키마에 따라 행이 튜플인지 단일 값인지가 결정되기 때문입니다. 빈 스키마에 대한 경우는 필요하지 않습니다. HasCol이 주어져 있고, HasCol의 두 생성자 모두 비어 있지 않은 스키마를 지정하기 때문입니다. 스키마에 열이 하나뿐이라면 포인터는 반드시 그 열을 가리켜야 하므로, HasCol의 생성자 중 here만 매칭하면 됩니다. 스키마의 열이 두 개 이상이면 here에 대한 경우와 there에 대한 경우가 모두 있어야 합니다. 전자에서는 값이 행의 첫 번째 값이고, 후자에서는 재귀 호출을 사용합니다. HasCol 타입이 행에 해당 열이 존재함을 보장하므로, Row.get은 Option을 반환할 필요가 없습니다.

HasCol은 두 가지 역할을 합니다:

1. 이는 특정 이름과 타입을 가진 열이 스키마에 존재한다는 증거 역할을 합니다.

2. 이는 행에서 해당 열과 연관된 값을 찾는 데 사용할 수 있는 데이터의 역할을 합니다.

첫 번째 역할인 증거로서의 역할은 명제가 사용되는 방식과 비슷합니다. 인덱스 족 HasCol의 정의는 주어진 열이 존재한다는 증거로 무엇이 인정되는지에 대한 명세로 읽을 수 있습니다. 그러나 명제와 달리 HasCol의 어떤 생성자가 사용되었는지가 중요합니다. 두 번째 역할에서는 컬렉션에서 데이터를 찾기 위해 생성자를 Nat처럼 사용합니다. 인덱스 족을 사용하는 프로그래밍에서는 두 관점 사이를 능숙하게 오가는 능력이 필요한 경우가 많습니다.

7.3.2.3. 부분 스키마🔗

관계 대수에서 중요한 연산 중 하나는 테이블이나 행을 더 작은 스키마로 사영하는 것입니다. 더 작은 스키마에 없는 열은 모두 버려집니다. 사영이 의미를 가지려면 더 작은 스키마가 더 큰 스키마의 부분 스키마여야 합니다. 즉, 더 작은 스키마의 모든 열이 더 큰 스키마에도 있어야 합니다. HasCol을 사용하면 행에서 실패할 수 없는 단일 열 조회를 작성할 수 있는 것처럼, 부분 스키마 관계를 인덱스 족으로 표현하면 실패할 수 없는 투영 함수를 작성할 수 있습니다.

한 스키마가 다른 스키마의 부분 스키마가 될 수 있는 방식은 인덱스 족으로 정의할 수 있습니다. 기본 아이디어는 작은 스키마의 모든 열이 큰 스키마에 나타나면 작은 스키마가 큰 스키마의 부분 스키마라는 것입니다. 작은 스키마가 비어 있으면 당연히 큰 스키마의 부분 스키마이며, 이는 생성자 nil로 표현됩니다. 작은 스키마에 열이 있으면 그 열은 큰 스키마에 있어야 하고, 부분 스키마의 나머지 열들도 모두 큰 스키마의 부분 스키마여야 합니다. 이는 생성자 cons로 표현됩니다.

다시 말해, Subschema는 더 작은 스키마의 각 열에, 더 큰 스키마에서 그 열의 위치를 가리키는 HasCol을 할당합니다.

travelDiary 스키마는 peak와 waterfall 모두에 공통되는 필드를 나타냅니다:

다음 예시에서 볼 수 있듯이, 이것은 분명히 peak의 부분 스키마입니다.

하지만 이런 코드는 읽기도 어렵고 유지보수하기도 어렵습니다. 이를 개선하는 한 가지 방법은 Lean이 Subschema와 HasCol 생성자를 자동으로 작성하도록 지시하는 것입니다. 이는 명제와 증명에 관한 막간에서 소개한 택틱 기능을 사용하여 할 수 있습니다. 그 막간에서는 by decide와 by simp를 사용하여 여러 명제의 증거를 제공합니다.

이 맥락에서는 두 가지 택틱이 유용합니다.

• constructor 택틱은 데이터 타입의 생성자를 사용하여 문제를 해결하도록 Lean에 지시합니다.

• repeat 택틱은 어떤 택틱이 실패하거나 증명이 끝날 때까지 그 택틱을 계속 반복하도록 Lean에 지시합니다.

다음 예제에서 by constructor는 그냥 .nil이라고 작성한 것과 같은 효과를 냅니다:

하지만 조금 더 복잡한 타입에 같은 택틱을 시도하면 실패합니다:

unsolved goals
a⊢ HasCol peak "location" DBType.string

a⊢ Subschema [] peak

unsolved goals로 시작하는 오류는 택틱이 구성해야 할 표현식을 완전히 구성하지 못했음을 나타냅니다. Lean의 택틱 언어에서 목표(goal)란 택틱이 내부적으로 적절한 표현식을 구성하여 충족시켜야 하는 타입입니다. 이 경우 constructor에 의해 Subschema.cons가 적용되었으며, 두 목표는 cons가 요구하는 두 인자를 나타냅니다. peak의 첫 번째 열은 "location"이 아니므로, constructor를 하나 더 추가하면 첫 번째 목표(HasCol peak "location" DBType.string)는 HasCol.there로 처리됩니다:

unsolved goals
a⊢ HasCol
  [{ name := "location", contains := DBType.string }, { name := "elevation", contains := DBType.int },
    { name := "lastVisited", contains := DBType.int }]
  "location" DBType.string

a⊢ Subschema [] peak

하지만 세 번째 constructor를 추가하면 HasCol.here를 적용할 수 있으므로 첫 번째 목표가 해결됩니다:

unsolved goals
a⊢ Subschema [] peak

constructor를 네 번째로 사용하면 Subschema peak [] 목표가 해결됩니다:

실제로 택틱을 사용하지 않고 작성한 버전에는 생성자가 네 개 있습니다:

constructor를 몇 번 써야 하는지 시행착오를 거쳐 알아내는 대신, repeat 택틱을 사용하면 진전이 있는 한 Lean이 constructor를 계속 시도하도록 할 수 있습니다:

이 더 유연한 버전은 더 흥미로운 Subschema 문제에도 적용됩니다:

무언가 동작할 때까지 생성자를 무작정 시도해 보는 접근 방식은 Nat이나 List Bool 같은 타입에는 그다지 유용하지 않습니다. 결국 어떤 표현식이 Nat 타입을 가진다고 해서 그것이 올바른 Nat이라는 뜻은 아니기 때문입니다. 하지만 HasCol이나 Subschema 같은 타입은 인덱스에 의해 충분히 제약되어 있어서 적용 가능한 생성자가 언제나 하나뿐입니다. 이는 프로그램 자체의 내용이 덜 흥미로우며, 컴퓨터가 올바른 생성자를 고를 수 있다는 뜻입니다.

한 스키마가 다른 스키마의 부분 스키마라면, 더 큰 스키마에 열을 하나 더 추가한 스키마의 부분 스키마이기도 합니다. 이 사실은 함수 정의로 나타낼 수 있습니다. Subschema.addColumn은 smaller가 bigger의 부분 스키마라는 증거를 받아서, smaller가 c :: bigger, 즉 열이 하나 더 추가된 bigger의 부분 스키마라는 증거를 반환합니다:

부분 스키마는 작은 스키마의 각 열을 큰 스키마의 어디에서 찾을 수 있는지 기술합니다. Subschema.addColumn은 이 기술을 원래의 큰 스키마 기준에서 확장된 큰 스키마 기준으로 옮겨야 합니다. nil의 경우 작은 스키마는 []이며, nil은 []이 c :: bigger의 부분 스키마라는 증거이기도 합니다. cons인 경우는 smaller의 열 하나를 bigger의 어디에 둘지를 기술하는데, 새 열 c를 반영하도록 there로 그 열의 위치를 조정해야 하며, 나머지 열은 재귀 호출이 조정합니다.

Subschema를 바라보는 또 다른 방식은 이것이 두 스키마 사이의 관계를 정의한다고 보는 것입니다. 즉, Subschema smaller bigger 타입을 갖는 표현식이 존재한다는 것은 (smaller, bigger)가 그 관계에 속한다는 뜻입니다. 이 관계는 반사적입니다. 즉, 모든 스키마는 자기 자신의 부분 스키마입니다:

7.3.2.4. 행 투영하기🔗

s'가 s의 부분 스키마라는 증거가 주어지면, s의 행을 s'의 행으로 사영할 수 있습니다. 이 작업은 s'가 s의 부분 스키마라는 증거를 사용하여 수행되며, 이 증거는 s'의 각 열이 s의 어디에 있는지를 알려 줍니다. s'의 새 행은 기존 행의 적절한 위치에서 값을 가져와 한 번에 한 열씩 만들어집니다.

이 사영을 수행하는 함수인 Row.project에는 Row 자체의 각 경우에 하나씩 대응하는 세 가지 경우가 있습니다. 이 함수는 Row.get과 Subschema 인자에 들어 있는 각 HasCol을 함께 사용하여 사영된 행을 구성합니다:

7.3.5.1. 데카르트 곱🔗

두 테이블의 데카르트 곱은 첫 번째 테이블의 각 행을 두 번째 테이블의 각 행에 이어 붙여서 구합니다. 먼저, Row의 구조 때문에 행에 열 하나를 추가하려면 결과가 단일 값이 될지 튜플이 될지 판단하기 위해 스키마에 대해 패턴 매칭을 해야 합니다. 이는 자주 쓰이는 연산이므로 패턴 매칭 부분을 헬퍼로 분리해 두면 편리합니다:

두 행을 이어 붙이는 연산은 첫 번째 스키마와 첫 번째 행 모두의 구조에 대해 재귀적입니다. 행의 구조가 스키마의 구조와 보조를 맞추어 진행되기 때문입니다. 첫 번째 행이 비어 있으면 이어 붙이기는 두 번째 행을 반환합니다. 첫 번째 행이 단일 원소이면 그 값이 두 번째 행에 추가됩니다. 첫 번째 행에 열이 여러 개 있으면 첫 번째 열의 값이 행의 나머지 부분에 대한 재귀 결과에 추가됩니다.

표준 라이브러리에 있는 List.flatMap은 그 자체로 리스트를 반환하는 함수를 입력 리스트의 모든 항목에 적용하고, 그 결과로 나온 리스트들을 순서대로 이어 붙인 결과를 반환합니다:

타입 시그니처를 보면 List.flatMap으로 Monad List 인스턴스를 구현할 수 있을 것 같습니다. 실제로 List.flatMap은 pure x := [x]와 함께 모나드를 구현합니다. 하지만 이는 그다지 유용한 Monad 인스턴스가 아닙니다. List 모나드는 기본적으로 Many의 한 변형으로, 사용자가 원하는 개수의 값을 요청할 기회를 갖기도 전에 탐색 공간을 지나는 모든 가능한 경로를 미리 탐색합니다. 이러한 성능상의 함정 때문에 List에 대해 Monad 인스턴스를 정의하는 것은 대개 좋은 생각이 아닙니다. 하지만 여기서는 질의 언어에 반환할 결과의 개수를 제한하는 연산자가 없으므로, 모든 가능성을 결합하는 것이 바로 원하는 동작입니다.

List.product와 마찬가지로, 항등 모나드 안에서 변경을 수행하는 루프를 대안적인 구현 기법으로 사용할 수 있습니다:

7.3.5.2. 차이🔗

테이블에서 원하지 않는 행은 List.filter를 사용하여 제거할 수 있습니다. 이 함수는 리스트와 Bool을 반환하는 함수를 인자로 받습니다. 그러면 함수가 true를 반환하는 항목만 담긴 새 리스트가 반환됩니다. 예를 들어,

다음으로 평가됩니다

"Columbia"와 "Sandy"의 길이가 8 이하이기 때문입니다. 테이블의 항목을 제거하려면 보조 함수 List.without을 사용하면 됩니다:

이는 쿼리를 해석할 때 Row에 대한 BEq 인스턴스와 함께 사용됩니다.

7.3.5.3. 열 이름 바꾸기🔗

행에서 열 이름을 바꾸는 작업은 재귀 함수로 수행합니다. 이 함수는 대상 열을 찾을 때까지 행을 순회하며, 그 열을 찾으면 새 이름을 가진 열에 기존 이름을 가진 열과 같은 값을 부여합니다:

이 함수는 인자의 타입을 바꾸지만, 실제 반환값에는 원래 인자와 정확히 같은 데이터가 들어 있습니다. 런타임 관점에서 보면 Row.rename은 느린 항등 함수에 지나지 않습니다. 인덱스 족으로 프로그래밍할 때의 어려움 중 하나는 성능이 중요한 상황에서 이런 종류의 연산이 방해가 될 수 있다는 점입니다. 이런 종류의 “재인덱싱” 함수를 없애려면 매우 신중하게 설계해야 하며, 그런 설계는 깨지기 쉬운 경우가 많습니다.

7.3.5.4. 열 이름에 접두사 붙이기🔗

열 이름에 접두사를 붙이는 작업은 열 이름을 바꾸는 작업과 매우 비슷합니다. prefixRow는 원하는 열까지 나아갔다가 되돌아오는 대신 모든 열을 처리해야 합니다:

이 함수를 List.map과 함께 사용하면 표의 모든 행에 접두사를 붙일 수 있습니다. 이번에도 이 함수는 값의 타입을 바꾸기 위해서만 존재합니다.

7.3.5.5. 모든 조각을 하나로 합치기🔗

이러한 보조 함수들을 모두 정의하고 나면, 쿼리를 실행하는 데는 짧은 재귀 함수 하나만 있으면 됩니다:

생성자의 인자 중 일부는 실행 중에 사용되지 않습니다. 특히 생성자 project와 함수 Row.project는 모두 더 작은 스키마를 명시적 인자로 받지만, 이 스키마가 더 큰 스키마의 부분 스키마라는 증거의 타입에는 Lean이 이 인자를 자동으로 채울 수 있을 만큼 충분한 정보가 담겨 있습니다. 마찬가지로 product 생성자가 요구하는, 두 테이블의 열 이름이 서로 겹치지 않는다는 사실은 Table.cartesianProduct에서는 필요하지 않습니다. 일반적으로 의존 타입은 Lean이 프로그래머를 대신하여 인자를 채워 넣을 수 있는 기회를 많이 제공합니다.

점 표기법은 쿼리 결과에 사용되어 List.map, List.filter, Table.cartesianProduct처럼 Table 네임스페이스와 List 네임스페이스 양쪽에 정의된 함수를 호출합니다. 이것이 가능한 이유는 Table이 abbrev를 사용하여 정의되었기 때문입니다. 타입 클래스 탐색과 마찬가지로, 점 표기법도 abbrev로 만든 정의를 꿰뚫어 볼 수 있습니다.

select의 구현 역시 상당히 간결합니다. 쿼리 q를 실행한 후 List.filter를 사용하여 표현식을 만족하지 않는 행을 제거합니다. List.filter는 Row s에서 Bool로 가는 함수를 기대하지만, DBExpr.evaluate의 타입은 Row s → DBExpr s t → t.asType입니다. select 생성자의 타입은 표현식이 DBExpr s .bool 타입을 가질 것을 요구하므로, 이 맥락에서 t.asType은 실제로 Bool입니다.

해발 고도가 500미터를 넘는 모든 산봉우리의 높이를 구하는 쿼리는 다음과 같이 작성할 수 있습니다:

이를 실행하면 예상한 대로 정수 리스트가 반환됩니다:

[3637, 1519, 2549]

관광 일정을 세울 때는 같은 위치에 있는 산과 폭포를 모두 짝지어 보는 것이 유용할 수 있습니다. 이는 두 테이블의 데카르트 곱을 구한 다음, 위치가 같은 행만 선택하고, 이름을 사영하여 수행할 수 있습니다:

예제 데이터에는 미국의 폭포만 포함되어 있으므로, 이 쿼리를 실행하면 미국에 있는 산과 폭포의 쌍이 반환됩니다:

[("Mount Nebo", "Multnomah Falls"), ("Mount Nebo", "Shoshone Falls"), ("Moscow Mountain", "Multnomah Falls"),
  ("Moscow Mountain", "Shoshone Falls"), ("Mount St. Helens", "Multnomah Falls"),
  ("Mount St. Helens", "Shoshone Falls")]

7.3.5.6. 마주칠 수 있는 오류🔗

Query의 정의 덕분에 발생할 수 있는 많은 오류가 사전에 배제됩니다. 예를 들어, "mountain.location"에 추가한 한정자를 빠뜨리면 열 참조 c! "location"을 강조하는 컴파일 타임 오류가 발생합니다: