7.4. Indices, Parameters, and Universe Levels
귀납 타입에서 인덱스와 매개변수의 구분은 생성자 사이에서 값이 달라지는지 여부를 설명하는 방식에 그치지 않는다. 귀납 타입의 인자가 매개변수인지 인덱스인지는 유니버스 단계 사이의 관계를 정할 때도 중요하다. 특히 귀납 타입은 매개변수와 같은 유니버스 단계에 있을 수 있지만 인덱스보다는 더 큰 유니버스에 있어야 한다. 이 제한이 있어야 Lean을 프로그래밍 언어이자 정리 증명기로 사용할 수 있으며, 없으면 Lean의 논리가 모순된다. 오류 메시지를 실험하면 이 규칙과 타입의 인자가 매개변수인지 인덱스인지 결정하는 정확한 규칙을 잘 이해할 수 있다.
일반적으로 귀납 타입의 정의에서는 콜론 앞에 매개변수를, 콜론 뒤에 인덱스를 둔다.
매개변수에는 함수 인자처럼 이름을 붙이지만 인덱스에는 타입만 기술한다.
이는 Vect의 정의에서 볼 수 있다:
inductive Vect (α : Type u) : Nat → Type u where
| nil : Vect α 0
| cons : α → Vect α n → Vect α (n + 1)
이 정의에서 α는 매개변수이고 Nat은 인덱스다.
매개변수는 정의 전체에서 참조할 수 있지만(예를 들어 Vect.cons는 첫 인자의 타입에 α를 사용한다) 항상 일관되게 사용해야 한다.
인덱스는 달라질 수 있으므로 데이터 타입 정의의 처음에 인자로 제공하는 대신 각 생성자에 개별 값을 지정한다.
매개변수를 가진 아주 간단한 데이터 타입은 WithParameter다:
inductive WithParameter (α : Type u) : Type u where
| test : α → WithParameter α
u 유니버스 단계를 매개변수와 귀납 타입 자체에 모두 사용할 수 있으므로 매개변수가 데이터 타입의 유니버스 단계를 높이지 않음을 알 수 있다.
마찬가지로 매개변수가 여러 개면 귀납 타입에는 더 큰 유니버스 단계가 사용된다:
inductive WithTwoParameters (α : Type u) (β : Type v) : Type (max u v) where
| test : α → β → WithTwoParameters α β매개변수는 데이터 타입의 유니버스 단계를 높이지 않으므로 다루기 편하다. Lean은 인덱스처럼 콜론 뒤에 기술되었지만 매개변수처럼 사용된 인자를 찾아 매개변수로 바꾸려 한다. 다음 두 귀납 데이터 타입은 매개변수를 콜론 뒤에 쓴 예다:
inductive WithParameterAfterColon : Type u → Type u where
| test : α → WithParameterAfterColon αinductive WithParameterAfterColon2 : Type u → Type u where
| test1 : α → WithParameterAfterColon2 α
| test2 : WithParameterAfterColon2 α초기 데이터 타입 선언에서 매개변수에 이름을 붙이지 않았다면 각 생성자에서 다른 이름을 사용할 수 있지만 일관되게 사용해야 한다. 다음 선언은 받아들여진다:
inductive WithParameterAfterColonDifferentNames : Type u → Type u where
| test1 : α → WithParameterAfterColonDifferentNames α
| test2 : β → WithParameterAfterColonDifferentNames β그러나 매개변수 이름을 명시적으로 선언한 데이터 타입에는 이 유연성이 적용되지 않는다:
inductive WithParameterBeforeColonDifferentNames (α : Type u) : Type u where
| test1 : α → WithParameterBeforeColonDifferentNames α
| test2 : β → WithParameterBeforeColonDifferentNames β마찬가지로 인덱스에 이름을 붙이려 하면 오류가 발생한다:
inductive WithNamedIndex (α : Type u) : Type (u + 1) where
| test1 : WithNamedIndex α
| test2 : WithNamedIndex α → WithNamedIndex α → WithNamedIndex (α × α)적절한 유니버스 단계를 사용하고 인덱스를 콜론 뒤에 두면 선언이 받아들여진다:
inductive WithIndex : Type u → Type (u + 1) where
| test1 : WithIndex α
| test2 : WithIndex α → WithIndex α → WithIndex (α × α)Lean은 귀납 타입 선언의 콜론 뒤 인자가 모든 생성자에서 일관되게 사용되면 매개변수라고 판단할 수 있지만, 모든 매개변수는 여전히 모든 인덱스보다 앞에 와야 한다. 인덱스 뒤에 매개변수를 두면 그 인자 자체가 인덱스로 취급되어 데이터 타입의 유니버스 단계가 높아져야 한다:
inductive ParamAfterIndex : Nat → Type u → Type u where
| test1 : ParamAfterIndex 0 γ
| test2 : ParamAfterIndex n γ → ParamAfterIndex k γ → ParamAfterIndex (n + k) γ
매개변수는 타입일 필요가 없다.
이 예에서는 Nat 같은 일반 데이터 타입도 매개변수로 사용할 수 있음을 보인다:
inductive NatParam (n : Nat) : Nat → Type u where
| five : NatParam 4 5
제안된 대로 n을 사용하면 선언이 받아들여진다:
inductive NatParam (n : Nat) : Nat → Type u where
| five : NatParam n 5이 실험에서 무엇을 결론 내릴 수 있는가? 매개변수와 인덱스의 규칙은 다음과 같다:
-
매개변수는 각 생성자의 타입에서 동일하게 사용해야 한다.
-
모든 매개변수는 모든 인덱스보다 앞에 와야 한다.
-
정의하는 데이터 타입의 유니버스 단계는 가장 큰 매개변수의 유니버스 단계 이상이어야 하며, 가장 큰 인덱스보다 엄밀히 커야 한다.
-
콜론 앞에 이름을 붙여 쓴 인자는 항상 매개변수이고, 콜론 뒤의 인자는 보통 인덱스다. 콜론 뒤의 인자가 모든 생성자에서 일관되게 사용되고 어떤 인덱스 뒤에도 오지 않으면 Lean은 그 사용 방식에 따라 해당 인자를 매개변수로 판단할 수 있다.
확실하지 않을 때는 Lean 명령 #print로 데이터 타입 인자 중 매개변수가 몇 개인지 확인할 수 있다.
예를 들어 Vect에서는 매개변수가 1개라고 알려 준다:
#print Vect데이터 타입 인자의 순서를 정할 때 어떤 인자를 매개변수로, 어떤 인자를 인덱스로 할지 생각할 가치가 있다. 가능한 많은 인자를 매개변수로 만들면 유니버스 단계를 제어하는 데 도움이 되어 복잡한 프로그램의 타입 검사가 쉬워진다. 이를 위한 한 방법은 인자 목록에서 모든 매개변수가 모든 인덱스보다 앞에 오게 하는 것이다.
또한 Lean이 콜론 뒤 인자의 사용 방식으로 매개변수임을 판단할 수 있더라도 매개변수에는 명시적인 이름을 쓰는 것이 좋다. 그러면 독자에게 의도가 분명해지고 생성자에서 인자를 실수로 일관되지 않게 사용했을 때 Lean이 오류를 보고한다.