7.4. 인덱스, 매개변수, 유니버스 레벨
귀납적 타입의 인덱스와 매개변수 사이의 구분은 생성자들 사이에서 변하거나 변하지 않는 타입의 인자들을 설명하는 방법에 그치지 않습니다. 귀납적 타입에 대한 인자가 매개변수인지 인덱스인지는 이들 유니버스 레벨 간의 관계를 결정할 때에도 중요합니다. 특히, 귀납적 타입은 매개변수와 동일한 유니버스 레벨을 가질 수 있지만, 인덱스보다는 더 큰 유니버스에 있어야 합니다. 이 제약은 Lean이 프로그래밍 언어일 뿐만 아니라 정리 증명기로도 사용될 수 있도록 보장하기 위해 필요합니다—이 제약이 없다면 Lean의 논리 체계는 모순되고 말 것입니다. 오류 메시지를 가지고 실험해 보는 것은 이러한 규칙들, 그리고 타입에 대한 인자가 매개변수인지 인덱스인지를 결정하는 정확한 규칙들을 설명하는 좋은 방법입니다.
일반적으로 귀납적 타입의 정의는 매개변수를 콜론 앞에, 인덱스를 콜론 뒤에 둡니다. 매개변수(parameter)는 함수 인자처럼 이름이 주어지는 반면, 인덱스(index)는 타입만 기술됩니다. 이는 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이 오류를 보고하도록 만듭니다.