7.1. 인덱스 족
다형적 귀납적 타입은 타입 인자를 받습니다. 예를 들어, List는 리스트 항목의 타입을 결정하는 인자를 받고, Except는 예외나 값의 타입을 결정하는 인자들을 받습니다. 데이터 타입의 모든 생성자에서 동일한 이러한 타입 인자들을 매개변수라고 합니다.
하지만 귀납적 타입의 인자가 모든 생성자에서 같아야 하는 것은 아닙니다. 어떤 생성자를 선택하느냐에 따라 타입의 인자가 달라지는 귀납적 타입을 인덱스 패밀리라고 부르며, 이때 달라지는 인자를 인덱스라고 합니다. 인덱스 족의 “hello world”는 원소의 타입뿐만 아니라 리스트의 길이도 함께 담고 있는 리스트 타입으로, 관례적으로 “벡터”라고 부릅니다:
inductive Vect (α : Type u) : Nat → Type u where
| nil : Vect α 0
| cons : α → Vect α n → Vect α (n + 1)
String 세 개로 이루어진 벡터의 타입에는 그 벡터가 String을 세 개 담고 있다는 사실이 포함됩니다:
example : Vect String 3 :=
.cons "one" (.cons "two" (.cons "three" .nil))
함수 선언은 일부 인자를 콜론 앞에 받을 수 있는데, 이는 해당 인자들을 정의 전체에서 사용할 수 있다는 뜻입니다. 또 일부 인자를 콜론 뒤에 받을 수도 있는데, 이는 그 인자들에 대해 패턴 매칭을 하여 함수를 경우별로 정의하겠다는 뜻입니다. 귀납적 데이터 타입에도 비슷한 원칙이 있습니다. 인자 α는 데이터 타입 선언의 맨 위, 콜론 앞에서 이름이 붙습니다. 이는 이 인자가 정의 안에서 Vect가 등장하는 모든 곳에 첫 번째 인자로 제공되어야 하는 매개변수임을 나타냅니다. 반면 Nat 인자는 콜론 뒤에 나오며, 이는 이 인자가 달라질 수 있는 인덱스임을 나타냅니다. 실제로 nil과 cons 생성자 선언에 등장하는 세 번의 Vect는 모두 일관되게 α를 첫 번째 인자로 제공하지만, 두 번째 인자는 경우마다 다릅니다.
nil의 선언은 이것이 Vect α 0 타입의 생성자임을 명시합니다. 즉, List String을 기대하는 문맥에서 [1, 2, 3]이 타입 오류인 것과 마찬가지로, Vect String 3을 기대하는 문맥에서 Vect.nil을 사용하는 것도 타입 오류입니다:
example : Vect String 3 := Vect.nil
이 예제에서 0과 3 사이의 불일치는 다른 모든 타입 불일치와 정확히 같은 역할을 합니다. 0과 3 자체는 타입이 아닌데도 그렇습니다. 메시지에 나오는 메타변수는 무시해도 됩니다. 메타변수가 있다는 것은 Vect.nil의 원소 타입이 무엇이든 될 수 있다는 뜻이기 때문입니다.
인덱스 족은 서로 다른 인덱스 값에 따라 사용할 수 있는 생성자가 달라질 수 있으므로 타입의 족이라고 불립니다. 어떤 의미에서 인덱스 족은 타입이 아닙니다. 그보다는 서로 관련된 타입들의 모음이며, 인덱스 값을 선택하는 것은 곧 그 모음에서 타입 하나를 선택하는 것이기도 합니다. Vect에 인덱스 5를 고르면 생성자 cons만 사용할 수 있고, 인덱스 0을 고르면 nil만 사용할 수 있습니다.
인덱스를 아직 알 수 없다면(예를 들어 변수이기 때문에), 인덱스가 알려질 때까지 어떤 생성자도 사용할 수 없습니다. 길이에 n을 사용하면 Vect.nil과 Vect.cons 중 어느 것도 사용할 수 없습니다. 변수 n이 나타내야 하는 Nat이 0에 맞는지 n + 1에 맞는지 알 방법이 없기 때문입니다:
example : Vect String n := Vect.nilexample : Vect String n := Vect.cons "Hello" (Vect.cons "world" Vect.nil)
리스트의 길이를 타입의 일부로 가지면 타입이 더 많은 정보를 담게 됩니다. 예를 들어, Vect.replicate는 주어진 값을 지정된 개수만큼 복사하여 Vect를 만드는 함수입니다. 이를 정확하게 나타내는 타입은 다음과 같습니다.
def Vect.replicate (n : Nat) (x : α) : Vect α n := _
인자 n은 결과의 길이로 나타납니다. 밑줄 자리 표시자에 연결된 메시지는 지금 해결해야 할 작업을 설명합니다:
인덱스 족을 다룰 때는 생성자의 인덱스가 기대 타입의 인덱스와 일치한다는 것을 Lean이 확인할 수 있는 경우에만 생성자를 적용할 수 있습니다. 그러나 어느 생성자도 n과 일치하는 인덱스를 가지고 있지 않습니다—nil은 Nat.zero와 일치하고, cons는 Nat.succ와 일치합니다. 앞서 예로 든 타입 오류에서와 마찬가지로, 변수 n은 함수에 인자로 어떤 Nat이 주어지느냐에 따라 둘 중 어느 쪽이든 나타낼 수 있습니다. 해결책은 패턴 매칭을 사용하여 가능한 두 경우를 모두 고려하는 것입니다:
def Vect.replicate (n : Nat) (x : α) : Vect α n :=
match n with
| 0 => _
| k + 1 => _
n이 기대 타입에 나타나므로, n에 대한 패턴 매칭은 매치의 두 경우에서 기대 타입을 구체화합니다. 첫 번째 밑줄에서 기대 타입은 Vect α 0이 되었습니다:
두 번째 밑줄 자리에서는 Vect α (k + 1)로 바뀌었습니다:
패턴 매칭이 값의 구조를 알아내는 것에 더해 프로그램의 타입까지 정제하는 경우, 이를 의존 패턴 매칭이라고 합니다.
정제된 타입 덕분에 생성자를 적용할 수 있습니다. 첫 번째 밑줄은 Vect.nil과 일치하고, 두 번째 밑줄은 Vect.cons와 일치합니다:
def Vect.replicate (n : Nat) (x : α) : Vect α n :=
match n with
| 0 => .nil
| k + 1 => .cons _ _
.cons 아래의 첫 번째 밑줄은 α 타입이어야 합니다. 사용할 수 있는 α가 있는데, 바로 x입니다:
두 번째 밑줄 자리에는 Vect α k가 와야 하며, 이는 replicate를 재귀 호출하여 만들 수 있습니다:
다음은 replicate의 최종 정의입니다:
def Vect.replicate (n : Nat) (x : α) : Vect α n :=
match n with
| 0 => .nil
| k + 1 => .cons x (replicate k x)
함수를 작성하는 동안 도움을 줄 뿐만 아니라, Vect.replicate의 타입은 많은 정보를 담고 있어서 클라이언트 코드가 소스 코드를 읽지 않고도 여러 예상치 못한 함수의 가능성을 배제할 수 있게 해 줍니다. 리스트용 replicate는 길이가 잘못된 리스트를 만들어 낼 수도 있습니다:
def List.replicate (n : Nat) (x : α) : List α :=
match n with
| 0 => []
| k + 1 => x :: x :: replicate k x
하지만 Vect.replicate에서 이런 실수를 하면 타입 오류가 발생합니다:
def Vect.replicate (n : Nat) (x : α) : Vect α n :=
match n with
| 0 => .nil
| k + 1 => .cons x (.cons x (replicate k x))
List.zip 함수는 첫 번째 리스트의 첫 번째 항목을 두 번째 리스트의 첫 번째 항목과, 첫 번째 리스트의 두 번째 항목을 두 번째 리스트의 두 번째 항목과 짝짓는 식으로 두 리스트를 결합합니다. List.zip을 사용하면 미국 오리건주에서 가장 높은 세 봉우리와 덴마크에서 가장 높은 세 봉우리를 짝지을 수 있습니다:
["Mount Hood",
"Mount Jefferson",
"South Sister"].zip ["Møllehøj", "Yding Skovhøj", "Ejer Bavnehøj"]결과는 세 개의 쌍으로 이루어진 리스트입니다:
[("Mount Hood", "Møllehøj"),
("Mount Jefferson", "Yding Skovhøj"),
("South Sister", "Ejer Bavnehøj")]두 리스트의 길이가 서로 다를 때 어떻게 동작해야 하는지는 다소 분명하지 않습니다. 많은 언어와 마찬가지로 Lean은 한쪽 리스트에 남는 항목을 무시하는 방식을 택합니다. 예를 들어 오리건주에서 가장 높은 봉우리 다섯 개의 높이를 덴마크에서 가장 높은 봉우리 세 개의 높이와 결합하면 세 개의 쌍이 만들어집니다. 구체적으로는,
[3428.8, 3201, 3158.5, 3075, 3064].zip [170.86, 170.77, 170.35]다음으로 평가됩니다
[(3428.8, 170.86), (3201, 170.77), (3158.5, 170.35)]
이 방식은 항상 답을 반환한다는 점에서 편리하지만, 리스트의 길이가 의도치 않게 서로 다를 때 데이터를 버리게 될 위험이 있습니다. F#은 다른 방식을 택합니다. F#의 List.zip은 길이가 일치하지 않으면 예외를 던지며, 이는 다음 fsi 세션에서 확인할 수 있습니다:
> List.zip [3428.8; 3201.0; 3158.5; 3075.0; 3064.0] [170.86; 170.77; 170.35];;
System.ArgumentException: The lists had different lengths. list2 is 2 elements shorter than list1 (Parameter 'list2') at Microsoft.FSharp.Core.DetailedExceptions.invalidArgDifferentListLength[?](String arg1, String arg2, Int32 diff) in /builddir/build/BUILD/dotnet-v3.1.424-SDK/src/fsharp.3ef6f0b514198c0bfa6c2c09fefe41a740b024d5/src/fsharp/FSharp.Core/local.fs:line 24 at Microsoft.FSharp.Primitives.Basics.List.zipToFreshConsTail[a,b](FSharpList`1 cons, FSharpList`1 xs1, FSharpList`1 xs2) in /builddir/build/BUILD/dotnet-v3.1.424-SDK/src/fsharp.3ef6f0b514198c0bfa6c2c09fefe41a740b024d5/src/fsharp/FSharp.Core/local.fs:line 918 at Microsoft.FSharp.Primitives.Basics.List.zip[T1,T2](FSharpList`1 xs1, FSharpList`1 xs2) in /builddir/build/BUILD/dotnet-v3.1.424-SDK/src/fsharp.3ef6f0b514198c0bfa6c2c09fefe41a740b024d5/src/fsharp/FSharp.Core/local.fs:line 929 at Microsoft.FSharp.Collections.ListModule.Zip[T1,T2](FSharpList`1 list1, FSharpList`1 list2) in /builddir/build/BUILD/dotnet-v3.1.424-SDK/src/fsharp.3ef6f0b514198c0bfa6c2c09fefe41a740b024d5/src/fsharp/FSharp.Core/list.fs:line 466 at <StartupCode$FSI_0006>.$FSI_0006.main@() Stopped due to error
이렇게 하면 실수로 정보를 버리는 일은 막을 수 있지만, 프로그램을 크래시시키는 데에도 나름의 어려움이 따릅니다. Lean에서 이에 해당하는 방식은 Option이나 Except 모나드를 사용하는 것인데, 이는 그로써 얻는 안전성에 비해 감수할 만한 가치가 없을 수도 있는 부담을 안겨 줍니다.
하지만 Vect를 사용하면, 두 인자의 길이가 같아야 함을 타입으로 요구하는 zip을 작성할 수 있습니다:
def Vect.zip : Vect α n → Vect β n → Vect (α × β) n
| .nil, .nil => .nil
| .cons x xs, .cons y ys => .cons (x, y) (zip xs ys)
이 정의에는 두 인자가 모두 Vect.nil인 경우와 두 인자가 모두 Vect.cons인 경우에 대한 패턴만 있지만, Lean은 List에 대한 비슷한 정의에서 발생하는 것과 같은 “missing cases” 오류 없이 이 정의를 받아들입니다:
def List.zip : List α → List β → List (α × β)
| [], [] => []
| x :: xs, y :: ys => (x, y) :: zip xs ys
이는 첫 번째 패턴에서 사용된 생성자 nil 또는 cons가 길이 n에 대한 타입 검사기의 지식을 정제하기 때문입니다. 첫 번째 패턴이 nil이면 타입 검사기는 길이가 0이었다는 것을 추가로 알아낼 수 있으므로, 두 번째 패턴으로 가능한 유일한 선택지는 nil입니다. 마찬가지로 첫 번째 패턴이 cons이면 타입 검사기는 어떤 Nat k에 대해 길이가 k+1이었다는 것을 알아낼 수 있으므로, 두 번째 패턴으로 가능한 유일한 선택지는 cons입니다. 실제로 nil과 cons를 함께 사용하는 경우를 추가하면 길이가 일치하지 않으므로 타입 오류가 발생합니다:
def Vect.zip : Vect α n → Vect β n → Vect (α × β) n
| .nil, .nil => .nil
| .nil, .cons y ys => .nil
| .cons x xs, .cons y ys => .cons (x, y) (zip xs ys)
n을 명시적 인자로 만들면 길이가 정제되는 것을 관찰할 수 있습니다:
def Vect.zip : (n : Nat) → Vect α n → Vect β n → Vect (α × β) n
| 0, .nil, .nil => .nil
| k + 1, .cons x xs, .cons y ys => .cons (x, y) (zip k xs ys)7.1.1. 연습 문제
의존 타입을 사용한 프로그래밍에 감을 잡으려면 경험이 필요하므로, 이 절의 연습 문제는 매우 중요합니다. 각 연습 문제를 풀 때 코드를 직접 실험해 보면서 타입 검사기가 어떤 실수를 잡아낼 수 있고 어떤 실수는 잡아내지 못하는지 확인해 보십시오. 이는 오류 메시지에 대한 감을 익히는 좋은 방법이기도 합니다.
-
오리건주에서 가장 높은 봉우리 세 곳과 덴마크에서 가장 높은 봉우리 세 곳을 결합할 때
Vect.zip이 올바른 결과를 내는지 다시 한번 확인하십시오.Vect에는List에 있는 문법 설탕이 없으므로,oregonianPeaks : Vect String 3과danishPeaks : Vect String 3을 정의하는 것부터 시작하면 도움이 될 수 있습니다. -
(α → β) → Vect α n → Vect β n타입을 가지는 함수Vect.map을 정의하십시오. -
함수를 사용하여
Vect의 원소들을 하나씩 결합하는 함수Vect.zipWith를 정의하십시오. 이 함수의 타입은(α → β → γ) → Vect α n → Vect β n → Vect γ n이어야 합니다. -
쌍으로 이루어진
Vect를 두Vect의 쌍으로 분리하는 함수Vect.unzip을 정의하십시오. 이 함수의 타입은Vect (α × β) n → Vect α n × Vect β n이어야 합니다. -
Vect의 끝에 항목을 추가하는 함수Vect.push를 정의하십시오. 이 함수의 타입은Vect α n → α → Vect α (n + 1)이어야 하며,#eval Vect.push (.cons "snowy" .nil) "peaks"의 결과는Vect.cons "snowy" (Vect.cons "peaks" (Vect.nil))이어야 합니다. -
Vect의 순서를 뒤집는 함수Vect.reverse를 정의하십시오. -
다음 타입을 갖는 함수
Vect.drop을 정의하십시오:(n : Nat) → Vect α (k + n) → Vect α k.#eval danishPeaks.drop 2의 결과가Vect.cons "Ejer Bavnehøj" (Vect.nil)인지 확인하여 함수가 올바르게 작동하는지 검증하십시오. -
Vect의 처음n개 항목을 반환하는, 타입이(n : Nat) → Vect α (k + n) → Vect α n인 함수Vect.take를 정의하십시오. 예제를 통해 제대로 동작하는지 확인하십시오.