7.3.2.1. Recursion and Universes, Revisited🔗

행을 튜플로 편리하게 구성하는 데에는 대가가 따른다. Row가 두 기본 경우를 별도로 처리하므로, Row를 타입에 사용하고 코드(즉 스키마)에 대해 재귀적으로 정의한 함수도 같은 구분을 해야 한다. 이 점이 중요한 한 예는 스키마를 따라 재귀하면서 행의 동등성을 검사하는 함수를 정의하는 동등성 검사다. 다음 예제는 Lean의 타입 검사를 통과하지 못한다.

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

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

다른 맥락과 달리 타입에 나타나는 함수는 입력과 출력의 동작만으로 생각할 수 없다. 이 타입을 사용하는 프로그램은 타입 수준 함수가 사용하는 알고리즘을 그대로 따라야 한다. 그래야 프로그램의 구조가 타입의 패턴 매칭 및 재귀 동작과 일치한다. 종속 타입으로 프로그래밍하는 능력의 큰 부분은 올바른 계산 동작을 가진 적절한 타입 수준 함수를 선택하는 것이다.

7.3.2.2. Column Pointers🔗

일부 질의는 스키마에 특정 열이 있을 때만 의미가 있다. 예를 들어 고도가 1000미터보다 높은 산을 반환하는 질의는 정수를 담는 "elevation" 열이 있는 스키마에서만 의미가 있다. 열이 스키마에 들어 있음을 나타내는 한 가지 방법은 그 열을 직접 가리키는 포인터를 제공하는 것이다. 이 포인터를 인덱스 패밀리로 정의하면 잘못된 포인터를 배제할 수 있다.

열이 스키마에 존재하는 방식은 두 가지다. 스키마의 맨 앞에 있거나, 스키마의 뒤쪽 어딘가에 있다. 스키마의 뒤쪽에 있는 열도 결국 스키마의 어떤 꼬리 부분에서는 맨 앞에 있게 된다.

인덱스 패밀리 HasCol은 이 명세를 Lean 코드로 옮긴 것이다.

이 패밀리의 세 인자는 스키마, 열 이름, 열의 타입이다. 세 인자 모두 인덱스이지만, 열 이름과 타입 뒤에 스키마가 오도록 인자의 순서를 바꾸면 이름과 타입을 매개변수로 둘 수 있다. 스키마가 ⟨name, t⟩ 열로 시작할 때 생성자 here를 사용할 수 있다. 따라서 이는 스키마의 첫 열을 가리키는 포인터이며, 첫 열이 원하는 이름과 타입을 가질 때만 사용할 수 있다. 생성자 there는 더 작은 스키마를 가리키는 포인터를 열이 하나 더 있는 스키마를 가리키는 포인터로 바꾼다.

"elevation"은 peak의 세 번째 열이므로, there로 처음 두 열을 지나가면 찾을 수 있고 그 뒤에는 첫 번째 열이 된다. 다시 말해 HasCol peak "elevation" .int 타입을 만족하려면 .there (.there .here) 표현식을 사용하라. HasCol을 장식된 Nat의 일종으로 생각할 수도 있다. zero는 here에 대응하고 succ는 there에 대응한다. 추가된 타입 정보 덕분에 하나 차이 나는 오류를 일으킬 수 없다.

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

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

HasCol은 두 가지 역할을 한다.

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

2. 행에서 그 열에 대응하는 값을 찾는 데 사용할 수 있는 데이터가 된다.

첫 번째 역할인 증거의 역할은 명제를 사용하는 방식과 비슷하다. 인덱스 패밀리 HasCol의 정의는 주어진 열이 존재한다는 증거로 인정되는 것이 무엇인지 명세한 것으로 읽을 수 있다. 하지만 명제와 달리 HasCol의 어떤 생성자를 사용했는지가 중요하다. 두 번째 역할에서는 생성자를 Nat처럼 사용해 컬렉션에서 데이터를 찾는다. 인덱스 패밀리로 프로그래밍하려면 이 두 관점 사이를 능숙하게 오갈 수 있어야 하는 경우가 많다.

7.3.2.3. Subschemas🔗

관계 대수의 중요한 연산 중 하나는 테이블이나 행을 더 작은 스키마로 프로젝션하는 것이다. 더 작은 스키마에 없는 모든 열은 버린다. 프로젝션이 의미 있으려면 더 작은 스키마가 더 큰 스키마의 서브스키마여야 한다. 즉 더 작은 스키마의 모든 열이 더 큰 스키마에 있어야 한다. 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의 전술 언어에서 목표는 전술이 내부에서 적절한 표현식을 구성해 충족해야 하는 타입이다. 이 경우 constructor가 Subschema.cons를 적용했고, 두 목표는 cons가 기대하는 두 인자를 나타낸다. constructor를 한 번 더 추가하면 첫 번째 목표(HasCol peak "location" DBType.string)는 HasCol.there로 처리된다. peak의 첫 열은 "location"이 아니기 때문이다.

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 전술을 사용해 진행이 되는 동안 constructor를 계속 시도하도록 Lean에게 요청할 수 있다.

이처럼 더 유연한 버전은 더 흥미로운 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. Projecting Rows🔗

s'가 s의 서브스키마라는 증거가 주어지면 s의 행을 s'의 행으로 프로젝션할 수 있다. 이는 s'가 s의 서브스키마라는 증거를 사용해 수행한다. 이 증거가 s'의 각 열이 s에서 어디에 있는지 알려 준다. 새 s' 행은 기존 행의 적절한 위치에서 값을 가져와 한 열씩 구성한다.

이 프로젝션을 수행하는 함수 Row.project에는 Row 자체의 각 경우에 대응하는 세 경우가 있다. Subschema 인자의 각 HasCol과 Row.get을 함께 사용해 프로젝션된 행을 구성한다.

7.3.5.1. Cartesian Product🔗

두 테이블의 데카르트 곱은 첫 번째 테이블의 각 행을 두 번째 테이블의 각 행에 덧붙여 구한다. 우선 Row의 구조 때문에 행에 열 하나를 추가하려면 결과가 단일 값인지 튜플인지 결정하도록 스키마에 패턴 매칭해야 한다. 이는 자주 쓰는 연산이므로 패턴 매칭을 도우미로 분리하면 편리하다.

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

표준 라이브러리에 있는 List.flatMap은 입력 리스트의 각 원소에 리스트를 반환하는 함수를 적용하고, 그 결과 리스트들을 순서대로 덧붙인 결과를 반환한다.

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

List.product와 마찬가지로 항등 모나드에서 변이를 사용하는 반복문을 대안 구현 기법으로 사용할 수도 있다.

7.3.5.2. Difference🔗

테이블에서 원하지 않는 행은 리스트와 Bool을 반환하는 함수를 받는 List.filter로 제거할 수 있다. 함수가 true를 반환하는 원소만 담은 새 리스트가 반환된다. 예를 들어

를 평가하면

"Columbia"와 "Sandy"의 길이가 8 이하이기 때문이다. 테이블의 원소는 도우미 List.without을 사용해 제거할 수 있다.

질의를 해석할 때 Row의 BEq 인스턴스와 함께 사용한다.

7.3.5.3. Renaming Columns🔗

행의 열 이름 바꾸기는 해당 열을 찾을 때까지 행을 순회하는 재귀 함수로 수행한다. 열을 찾으면 새 이름의 열에 이전 열과 같은 값을 넣는다.

이 함수는 인자의 타입을 바꾸지만 실제 반환값에는 원래 인자와 정확히 같은 데이터가 들어 있다. 실행 시간 관점에서 Row.rename은 느린 항등 함수에 불과하다. 인덱스 패밀리로 프로그래밍할 때의 한 가지 어려움은 성능이 중요하면 이런 연산이 방해가 될 수 있다는 점이다. 이런 “재인덱싱” 함수를 없애려면 매우 신중하고 흔히 취약한 설계가 필요하다.

7.3.5.4. Prefixing Column Names🔗

열 이름에 접두사를 붙이는 일은 열 이름을 바꾸는 일과 매우 비슷하다. 원하는 열까지 이동한 다음 반환하는 대신 prefixRow는 모든 열을 처리해야 한다.

이를 List.map과 함께 사용하면 테이블의 모든 행에 접두사를 붙일 수 있다. 다시 말해 이 함수는 값의 타입을 바꾸기 위해서만 존재한다.

7.3.5.5. Putting the Pieces Together🔗

이 도우미들을 모두 정의했으므로 질의를 실행하려면 짧은 재귀 함수 하나만 있으면 된다.

생성자의 일부 인자는 실행 중에 사용되지 않는다. 특히 project 생성자와 Row.project 함수는 더 작은 스키마를 명시적 인자로 받지만, 이 스키마가 더 큰 스키마의 서브스키마라는 증거의 타입에 충분한 정보가 들어 있어 Lean이 인자를 자동으로 채울 수 있다. 마찬가지로 product 생성자가 요구하는 두 테이블의 열 이름이 서로소라는 사실은 Table.cartesianProduct에 필요하지 않다. 일반적으로 종속 타입은 프로그래머를 대신해 Lean이 인자를 채우게 할 기회를 많이 제공한다.

질의 결과에는 점 표기법을 사용해 Table 및 List 네임스페이스에 정의된 List.map, List.filter, Table.cartesianProduct 같은 함수를 호출한다. 이는 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. Errors You May Meet🔗

Query의 정의는 발생 가능한 많은 오류를 배제한다. 예를 들어 "mountain.location"에서 추가한 수식어를 잊으면 컴파일 시간 오류가 발생하며 열 참조 c! "location"을 강조한다.