7.4. 인덱스, 매개변수, 유니버스 레벨
귀납적 타입의 인덱스와 매개변수를 구분하는 것은 단순히 생성자마다 달라지거나 달라지지 않는 타입의 인자를 설명하는 방법에 그치지 않습니다. 귀납적 타입의 인자가 매개변수인지 인덱스인지는 이들의 유니버스 레벨 사이의 관계를 결정할 때에도 중요합니다. 특히 귀납적 타입은 매개변수와 같은 유니버스 레벨을 가질 수 있지만, 인덱스보다는 더 큰 유니버스에 있어야 합니다. 이 제약은 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이 오류를 보고하게 됩니다.