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 타입의 생성자임을 명시합니다. 즉, [1, 2, 3]이 List String을 기대하는 문맥에서 타입 오류인 것과 마찬가지로, Vect String 3을 기대하는 문맥에서 Vect.nil을 사용하는 것도 타입 오류입니다:

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이 어떤 요소 타입이든 가질 수 있음을 나타내기 때문입니다.

인덱싱된 패밀리는 서로 다른 인덱스 값에 따라 서로 다른 생성자를 사용할 수 있게 만들기 때문에 타입의 family라고 불립니다. 어떤 의미에서 색인 패밀리는 타입이 아니라 서로 관련된 타입들의 모음이며, 색인 값을 선택하는 것은 곧 그 모음에서 타입을 선택하는 것이기도 합니다. 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은 결과의 길이로 나타납니다. 밑줄 자리 표시자(underscore placeholder)와 연관된 메시지는 현재의 작업을 설명합니다:

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

인덱싱된 패밀리를 다룰 때, 생성자는 Lean이 생성자의 인덱스가 기대 타입의 인덱스와 일치함을 알 수 있는 경우에만 적용될 수 있습니다. 하지만 두 생성자 모두 n과 일치하는 인덱스를 가지고 있지 않습니다—nil은 Nat.zero와 일치하고, cons는 Nat.succ와 일치합니다. 예시 타입 오류에서와 마찬가지로, 변수 n은 함수에 인자로 어떤 Nat이 제공되는지에 따라 둘 중 어느 쪽이든 될 수 있습니다. 해결 방법은 패턴 매칭을 사용하여 가능한 두 경우를 모두 고려하는 것입니다:

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⊢ α

두 번째 밑줄은 Vect α k여야 하며, 이는 replicate에 대한 재귀 호출로 만들어낼 수 있습니다:

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

이는 정보가 실수로 폐기되는 것을 방지하지만, 프로그램이 크래시되는 것도 그 나름의 어려움을 수반합니다. Option 또는 Except 모나드를 사용할 Lean에서의 대응물은 안전성만큼의 가치가 없을 수도 있는 부담을 초래할 것입니다.

하지만 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에 대한 유사한 정의에서 발생하는 것과 같은 "누락된 경우" 오류 없이 이 정의를 받아들입니다:

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. 연습문제🔗

의존 타입을 사용한 프로그래밍에 대한 감각을 얻으려면 경험이 필요하며, 이 절의 연습 문제는 매우 중요합니다. 각 연습 문제를 풀 때, 코드를 직접 실험해 보면서 타입 검사기가 어떤 실수를 잡아낼 수 있고 어떤 실수는 잡아낼 수 없는지 확인해 보십시오. 이는 오류 메시지에 대한 감각을 익히는 좋은 방법이기도 합니다.

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 타입을 가져야 합니다.
쌍(pair)들의 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.reverse 함수를 정의하여 Vect의 순서를 뒤집으십시오.
다음 타입을 갖는 함수 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를 정의하십시오. 예제에서 잘 작동하는지 확인하십시오.