7.1. Indexed Families🔗

다형성 귀납 타입은 타입 인자를 받는다. 예를 들어 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임을 말한다. 따라서 Vect String 3을 예상하는 문맥에서 Vect.nil을 사용하면 타입 오류다. List String을 예상하는 문맥에서 [1, 2, 3]을 사용하는 것과 같다:

example : Vect String 3 := Type mismatch
  Vect.nil
has type
  Vect ?m.3 0
but is expected to have type
  Vect String 3Vect.nil

Type mismatch
  Vect.nil
has type
  Vect ?m.3 0
but is expected to have type
  Vect String 3

이 예에서 0과 3의 불일치는 0과 3이 타입 자체가 아니더라도 다른 타입 불일치와 정확히 같은 역할을 한다. 메시지의 메타변수는 무시해도 된다. 메타변수가 있다는 것은 Vect.nil이 어떤 원소 타입도 가질 수 있음을 나타낸다.

인덱스 값에 따라 사용할 수 있는 생성자가 달라지므로 인덱싱된 패밀리를 타입의 패밀리라고 한다. 어떤 의미에서 인덱싱된 패밀리는 타입 하나가 아니라 서로 관련된 타입의 모음이며, 인덱스 값을 고르는 일이 모음에서 타입을 고르는 일이다. Vect의 인덱스로 5를 고르면 cons만 사용할 수 있고, 0을 고르면 nil만 사용할 수 있다.

인덱스가 아직 알려지지 않았다면(예를 들어 변수라면) 인덱스가 알려질 때까지 어떤 생성자도 사용할 수 없다. 길이에 n을 사용하면 Vect.nil과 Vect.cons 어느 것도 쓸 수 없다. 변수 n이 0과 일치하는 Nat인지 n + 1과 일치하는지 알 방법이 없기 때문이다:

example : Vect String n := Type mismatch
  Vect.nil
has type
  Vect ?m.2 0
but is expected to have type
  Vect String nVect.nil

Type mismatch
  Vect.nil
has type
  Vect ?m.2 0
but is expected to have type
  Vect String n

example : Vect String n := Type mismatch
  Vect.cons "Hello" (Vect.cons "world" Vect.nil)
has type
  Vect String (0 + 1 + 1)
but is expected to have type
  Vect String nVect.cons "Hello" (Vect.cons "world" Vect.nil)

Type mismatch
  Vect.cons "Hello" (Vect.cons "world" Vect.nil)
has type
  Vect String (0 + 1 + 1)
but is expected to have type
  Vect String n

리스트 길이를 타입의 일부로 만들면 타입에 더 많은 정보가 들어간다. 예를 들어 Vect.replicate는 주어진 값을 여러 번 복사한 Vect를 만드는 함수다. 이를 정확히 나타내는 타입은 다음과 같다:

def Vect.replicate (n : Nat) (x : α) : Vect α n := don't know how to synthesize placeholder
context:
α:Type u_1n:Natx:α⊢ Vect α n_

인자 n은 결과의 길이로 나타난다. 밑줄 자리표시자와 관련된 메시지는 해야 할 일을 설명한다:

don't know how to synthesize placeholder
context:
α:Type u_1n:Natx:α⊢ Vect α n

인덱싱된 패밀리를 다룰 때 생성자의 인덱스가 예상 타입의 인덱스와 일치함을 Lean이 알 수 있을 때만 생성자를 적용할 수 있다. 그러나 어느 생성자도 n과 일치하는 인덱스를 갖지 않는다. nil은 Nat.zero와, cons는 Nat.succ와 일치한다. 앞의 타입 오류 예제와 마찬가지로 함수 인자로 어떤 Nat이 주어지는지에 따라 변수 n은 둘 중 하나를 나타낼 수 있다. 해결책은 패턴 매칭으로 가능한 두 경우를 모두 고려하는 것이다:

def Vect.replicate (n : Nat) (x : α) : Vect α n :=
  match n with
  | 0 => don't know how to synthesize placeholder
context:
α:Type u_1n:Natx:α⊢ Vect α 0_
  | k + 1 => don't know how to synthesize placeholder
context:
α:Type u_1n:Natx:αk:Nat⊢ Vect α (k + 1)_

예상 타입에 n이 들어 있으므로 n에 패턴 매칭을 적용하면 두 경우에서 예상 타입이 정제된다. 첫 번째 밑줄에서는 예상 타입이 Vect α 0이 되었다.

don't know how to synthesize placeholder
context:
α:Type u_1n:Natx:α⊢ Vect α 0

두 번째 밑줄에서는 예상 타입이 Vect α (k + 1)이 되었다.

don't know how to synthesize placeholder
context:
α:Type u_1n:Natx:αk:Nat⊢ Vect α (k + 1)

값의 구조를 알아내는 것에 더해 패턴 매칭이 프로그램의 타입을 정제하면 이를 종속 패턴 매칭이라고 한다.

정제된 타입 덕분에 생성자를 적용할 수 있다. 첫 번째 밑줄은 Vect.nil과, 두 번째 밑줄은 Vect.cons와 일치한다:

def Vect.replicate (n : Nat) (x : α) : Vect α n :=
  match n with
  | 0 => .nil
  | k + 1 => .cons don't know how to synthesize placeholder
context:
α:Type u_1n:Natx:αk:Nat⊢ α_ don't know how to synthesize placeholder
context:
α:Type u_1n:Natx:αk:Nat⊢ Vect α k_

.cons 아래의 첫 번째 밑줄은 α 타입이어야 한다. 사용할 수 있는 α는 x다:

don't know how to synthesize placeholder
context:
α:Type u_1n:Natx:αk:Nat⊢ α

두 번째 밑줄은 재귀 호출 replicate로 만들 수 있는 Vect α k여야 한다:

don't know how to synthesize placeholder
context:
α:Type u_1n:Natx:αk:Nat⊢ Vect α k

다음은 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 Application type mismatch: The argument
  cons x (replicate k x)
has type
  Vect α (k + 1)
but is expected to have type
  Vect α k
in the application
  cons x (cons x (replicate k x))(.cons x (replicate k x))

Application type mismatch: The argument
  cons x (replicate k x)
has type
  Vect α (k + 1)
but is expected to have type
  Vect α k
in the application
  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 (α × β)
  Missing cases:
[], (List.cons _ _)
(List.cons _ _), []| [], [] => []
  | x :: xs, y :: ys => (x, y) :: zip xs ys

Missing cases:
[], (List.cons _ _)
(List.cons _ _), []

첫 패턴에 사용한 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, Type mismatch
  Vect.cons y ys
has type
  Vect ?m.10 (?m.16 + 1)
but is expected to have type
  Vect β 0.cons y ys => .nil
  | .cons x xs, .cons y ys => .cons (x, y) (zip xs ys)

Type mismatch
  Vect.cons y ys
has type
  Vect ?m.10 (?m.16 + 1)
but is expected to have type
  Vect β 0

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. Exercises🔗

종속 타입 프로그래밍의 감각을 익히려면 경험이 필요하므로 이 절의 연습문제는 매우 중요하다. 각 연습문제에서 코드를 실험하며 타입 검사기가 어떤 실수를 잡고 어떤 실수를 잡지 못하는지 확인하라. 이는 오류 메시지에 익숙해지는 좋은 방법이기도 하다.

오리건의 가장 높은 산 세 개와 덴마크의 가장 높은 산 세 개를 결합할 때 Vect.zip이 올바른 답을 내는지 다시 확인하라. Vect에는 List의 문법적 편의 기능이 없으므로 먼저 oregonianPeaks : Vect String 3과 danishPeaks : Vect String 3을 정의하는 것이 좋다.
Vect.map 함수를 (α → β) → Vect α n → Vect β n 타입으로 정의하라.
Vect.zipWith 함수를 정의하여 Vect의 원소를 함수로 하나씩 결합하라. 타입은 (α → β → γ) → 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.take 함수를 (n : Nat) → Vect α (k + n) → Vect α n 타입으로 정의하여 Vect의 처음 n개 원소를 반환하라. 예제에서 올바르게 작동하는지 확인하라.