종 (유형 이론)

종(kind)는 수리논리학 및 컴퓨터 과학의 영역에서 형 이론(타입 이론)으로 구분되어 있다. 종(kind)이란 타입 생성자같은 타입 혹은, 약간 더 일반적이지는 못하지만, 고계(고차)연산자와 같은 타입이다. 원시 타입은 *로 표기하고 "타입"이라고 부른다. 이는 어떤 타입 파라메터도 필요로 하지 않는 모든 데이터 타입의 종류이다. 종 시스템은 원시 타입에 부여된 단순 타입의 람다 계산법에서 "one level up"이다.

종은 때때로 혼동되도록 "(데이터) 타입의 타입"으로 설명되곤 하지만, 실제로는 인자(arity) 지정자라고 보는게 더 맞다. 구문 상으로는, 다형성 타입을 타입 생성자라고 생각하는 것이 더 자연스러우며, 따라서 다형성이 없는 타입의 경우 인자가 없는(nullary) 타입 생성자라고 생각하는 게 맞다. 그러나 모든 인자가 없는 생성자, 즉 모든 단일형 타입은 동일하고, 가장 간단한 종, 이름하여 *을 가진다.

프로그래밍 언어에서 고계(higher-order) 타입 연산자가 일반적이지는 않으므로, 대부분의 프로그래밍 실전에서, 종(kind)은 데이터 타입과 파라메터 다형성을 구현하는데 사용되는 생성자 타입을 구분하는데 사용된다. 종(kind)은 하스켈과 스칼라와 같이, 타입 시스템이 프로그래밍의 접근 방식으로 파라메터 다형성을 설명하는 언어에서, 명시적 혹은 암시적으로 나타난다.

예제

• $*$ ("타입"이라고 발음)은 인자가 없는(nullary) 타입 생성자라고 보여지는 모든 데이터 타입의 종류이며, 이러한 맥락에서 더 나은 타입이라고 한다. 이것은 보통 함수형 프로그래밍 언어의 함수 타입을 포함한다.
• $*\rightarrow *$은 단일 인자 타입 생성자의 종으로, 예를 들어, 리스트 타입 생성자가 해당된다.
• $*\rightarrow *\rightarrow *$은 (커링을 통한) 이진 인자(인자가 두 개)인 형식의 생성자의 종으로, 함수 타입 생성자의 종이기도 하다(함수 타입의 적용 결과와 헷갈리면 안 된다. 그 자체가 함수 타입이므로 $*$다
• $(*\rightarrow *)\rightarrow *$는 단일 타입 생성자에서 적합한 타입으로의 고계(higher-order) 타입 연산자 종이다.

하스켈의 종

(참고: 하스켈 문서는 함수 타입과 종에 대해서 동일한 화살표를 사용한다)

하스켈의 종 시스템은 단순히 두 가지 규칙을 가지고 있다:

• $*$모든 데이터 유형의 종이다
• $k_{1}\rightarrow k_{2}$ 은 단일 타입 생성자의 종으로, $k1$ 종의 타입을 받고 $k2$ 종의 타입을 반환한다.

(하스켈에서 적절한 타입이 호출됨으로써) 존재하는 타입은 값을 가지는 타입이다. 예를 들어, 상황을 복잡하게 만드는 타입 클래스는 무시하면, 4는 Int 타입의 값인 반면,  [1,2,3] 은 [Int] 타입의 값(정수형의 리스트)이다. 따라서, Int와 [Int]는 $*$ 종을 갖지만, 예를 들어, Int->Bool 또는 Int->Int->Bool와 같은 모든 함수 타입이 될 수 있다.

타입 생성자는 한 개 이상의 타입 인자를 받으며, 충분한 인자가 제공될 경우 데이터 타입을 만들어 낸다. 즉, 커링으로 부분 적용을 지원한다. 이는 하스켈이 파라메터 타입을 달성하는 방법이다. 예를 들어, [](목록) 타입은 타입 생성자로, 단일 인자를 받아 리스트의 요소의 타입을 지정한다. 따라서, [Int] (정수형 목록), [Float] (부동소수점형의 목록), 심지어 [[Int]] (정수형 목록의 목록)은 [] 타입을 유효하게 적용한 것이다. 그러므로, []은 $*\rightarrow *$이다. Int이 $*$이기 때문에, 그것을 []에 적용하게 되면 [Int]를 결과로 하며 $*$ 종이 된다. 2-튜플 생성자 (,)는 $*\rightarrow *$ 종이고, 3-튜플 생성자 (,,)는 $*\rightarrow *\rightarrow *$ 종이 되는 식이다.

종(kind) 추론

표준 하스켈은 다형성 종을 허용하지 않는다. 이것은 하스켈에서 지원되는 타입에 대한 파라메터 다형성과는 대조적이다. 예를 들어, 다음 예제에서:

data Tree z  = Leaf | Fork (Tree z) (Tree z)

z 는 $*$ $*\rightarrow *$ 등 어떤 종(kind)이든 될 수 있다. 기본적으로 하스켈은 타입이 명시적으로 다른 것을 나타내지 않는 이상, $*$. 그러므로 타입 검사기는 Tree를 다음과 같이 사용되는 것을 거부한다:

type FunnyTree = Tree []     -- invalid

[] 종(kind)으로 인해, $*\rightarrow *$ 은 항상 $*$인 z에 대한 예상되는 종(kind)와 일치하지 않는다. 하지만, 고계(higher-order) 타입 연산자는 허용된다. 예를 들어:

data App unt z = Z (unt z)

은 $(*\rightarrow *)\rightarrow *\rightarrow *$unt는 단일 인자 데이터 생성자일 것으로 예상되며, 그것의 인자에 적용되며, 반드시 하나의 타입이 있어야 하고, 다른 타입을 반환해야 한다. GHC는 PolyKinds 확장으로, KindSignatures와 함께 다형 종을 허용한다. 예를 들어:

data Tree (z :: k) = Leaf | Fork (Tree z) (Tree z)
type FunnyTree = Tree []     -- OK

GHC 8.0.1에서, 타입과 종은 실험적인 컴파일러 옵션인 -XTypeInType을 사용해 합쳐질 수 있다.