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

로우(row)를 튜플로 편리하게 구조화하는 데는 대가가 따릅니다: 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)의 타입을 충분히 정제하지 못한다는 것입니다. 이는 Row의 정의에서 단일 패턴 [col]이 매칭되었는지 아니면 col1 :: col2 :: cols 패턴이 매칭되었는지를 Lean이 아직 판단할 수 없기 때문이며, 따라서 Row 호출은 쌍 타입으로 계산되지 않습니다. 해결 방법은 Row.bEq의 정의에서 Row의 구조를 그대로 반영하는 것입니다:

다른 맥락에서와 달리, 타입에 등장하는 함수는 입력/출력 동작만으로는 고려할 수 없습니다. 이러한 타입을 사용하는 프로그램은 그 구조가 타입의 패턴 매칭 및 재귀 동작과 일치하도록 타입 수준 함수에서 사용된 알고리즘을 그대로 반영해야만 하게 됩니다. 의존 타입으로 프로그래밍하는 능력의 상당 부분은 올바른 계산적 동작을 갖는 적절한 타입 수준 함수를 선택하는 데 있습니다.

7.3.2.2. 열 포인터🔗

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

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

인덱스 계열 HasCol은 명세를 Lean 코드로 옮긴 것입니다:

이 패밀리의 세 인자는 스키마, 열 이름, 그 타입입니다. 세 가지 모두 인덱스이지만, 스키마를 열 이름과 타입 뒤에 배치하도록 인자 순서를 재조정하면 이름과 타입을 매개변수로 만들 수 있습니다. 생성자 here는 스키마가 열 ⟨name, t⟩로 시작할 때 사용할 수 있습니다. 즉, 이는 스키마의 첫 번째 열을 가리키는 포인터이며, 첫 번째 열이 원하는 이름과 타입을 가질 때에만 사용할 수 있습니다. 생성자 there는 더 작은 스키마를 가리키는 포인터를, 열이 하나 더 있는 스키마를 가리키는 포인터로 변환합니다.

"elevation"은 peak에서 세 번째 열이므로, there로 처음 두 열을 지나쳐서 찾을 수 있으며, 그 뒤로는 첫 번째 열이 됩니다. 다시 말해, HasCol peak "elevation" .int 타입을 만족시키려면 표현식 .there (.there .here)를 사용합니다. HasCol을 생각하는 한 가지 방법은 이를 장식된 Nat의 일종으로 보는 것입니다—zero는 here에 대응하고, succ는 there에 대응합니다. 이 추가적인 타입 정보 덕분에 오프바이원(off-by-one) 오류가 발생할 수 없습니다.

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

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

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

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

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

첫 번째 역할인 증거로서의 역할은 명제가 사용되는 방식과 유사합니다. 색인화된 패밀리 HasCol의 정의는 주어진 열이 존재한다는 증거로 간주되는 것이 무엇인지에 대한 명세로 읽을 수 있습니다. 그러나 명제와 달리, HasCol의 어떤 생성자가 사용되었는지가 중요합니다. 두 번째 역할에서는 생성자가 컬렉션에서 데이터를 찾기 위해 Nat처럼 사용됩니다. 인덱스 패밀리로 프로그래밍하려면 두 관점 사이를 유창하게 전환할 수 있는 능력이 필요할 때가 많습니다.

7.3.2.3. 서브스키마🔗

관계대수학에서 중요한 연산 중 하나는 테이블이나 행을 더 작은 스키마로 사영하는 것입니다. 더 작은 스키마에 존재하지 않는 모든 열은 잊혀집니다. 사영이 성립하려면 더 작은 스키마가 더 큰 스키마의 서브스키마여야 하는데, 이는 더 작은 스키마의 모든 열이 더 큰 스키마에 존재해야 함을 의미합니다. HasCol이 실패할 수 없는 행에서의 단일 열 조회를 작성할 수 있게 해주는 것과 마찬가지로, 서브스키마 관계를 색인화된 패밀리로 표현하면 실패할 수 없는 투영 함수를 작성할 수 있습니다.

한 스키마가 다른 스키마의 서브스키마가 될 수 있는 방식들은 색인 계열(indexed family)로 정의할 수 있습니다. 기본적인 아이디어는 더 작은 스키마의 모든 열이 더 큰 스키마에 나타나는 경우, 그 더 작은 스키마가 더 큰 스키마의 서브스키마가 된다는 것입니다. 더 작은 스키마가 비어 있다면, 이는 생성자 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가 기대하는 두 개의 인자를 나타냅니다. constructor의 인스턴스를 하나 더 추가하면 peak의 첫 번째 열이 "location"이 아니기 때문에 첫 번째 목표(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 자체의 각 경우에 대응하는 세 가지 경우를 가집니다. 이는 Subschema 인자에 있는 각 HasCol과 함께 Row.get을 사용하여 프로젝션된 행을 구성합니다:

7.3.5.1. 데카르트 곱🔗

두 테이블의 데카르트 곱을 구하는 것은 첫 번째 테이블의 각 행을 두 번째 테이블의 각 행에 이어 붙이는 방식으로 수행됩니다. 첫째로, Row의 구조로 인해, 행에 단일 열을 추가하려면 결과가 순수한 값이 될지 튜플이 될지를 판단하기 위해 스키마에 대한 패턴 매칭이 필요합니다. 이는 흔한 연산이므로, 패턴 매칭을 헬퍼로 분리해 내는 것이 편리합니다:

두 행을 이어 붙이는 것은 첫 번째 스키마와 첫 번째 행의 구조 모두에 대해 재귀적인데, 이는 행의 구조가 스키마의 구조와 발맞추어 진행되기 때문입니다. 첫 번째 행이 비어 있으면, 이어붙이기는 두 번째 행을 반환합니다. 첫 번째 행이 단일 요소일 경우, 그 값은 두 번째 행에 추가됩니다. 첫 번째 행에 여러 열이 포함되어 있는 경우, 첫 번째 열의 값은 해당 행의 나머지 부분에 대한 재귀 결과에 더해집니다.

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

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

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

7.3.5.2. 차이점🔗

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

다음으로 평가됩니다

"Columbia"와 "Sandy"는 길이가 8 이하이기 때문입니다. 테이블의 항목을 제거하는 작업은 도우미 List.without를 사용하여 수행할 수 있습니다:

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

7.3.5.3. 열 이름 변경🔗

행(row)에서 열(column) 이름을 변경하는 작업은 문제의 열을 찾을 때까지 행을 순회하는 재귀 함수로 수행되며, 열을 찾으면 새 이름을 가진 열이 기존 이름을 가진 열과 동일한 값을 갖게 됩니다:

이 함수는 인자의 type을 바꾸지만, 실제 반환값은 원래 인자와 정확히 같은 데이터를 담고 있습니다. 실행 시점의 관점에서 보면, 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"이 강조됩니다: