확장 PolyKinds (작성 중)

GHC 공식 가이드 - 6.4.12. Kind polymorphism

생각 스트레칭

타입이 들어갈 자리를 a로 두면, 필요에 따라 여러 타입으로 바뀔 수 있는 걸 폴리모픽 타입이라 했습니다.
여러 타입을 a로 추상화해서 표현했다 말할 수도 있습니다.

폴리모픽 카인드는 필요에 따라 카인드를 다른 것으로 볼 수 있다는 얘기입니다.

다형Polymorphic 카인드

data App f a = MkApp (f a)

App의 카인드를 보면
Type -> Type인 f를 받고, Type을 받아 Type을 돌려주는 걸로 읽을 수 있습니다.

(Type -> Type) -> Type -> Type

그런데, 더 일반적인 상황까지 고려하면 a를 Type으로 보지 않고, Type -> Type으로 볼 수도 있습니다. (a, 1,… 보다 일반화해서 표현하면, 어떤 생성자 안에 들어 있는 타입 Just 1, [1], … 등으로 볼 수도 있습니다.) 그럼, a에 (Type -> Type)을 넣으면,

((Type -> Type) -> Type)) -> (Type -> Type) -> Type

로 일반화할 수 있습니다. KindSignatures 확장을 켜지 않고, GHC가 이렇게 카인드를 추론하게 하려면, a에 더미 생성자를 추가해서 Type -> Type으로 추론하게 할 수 있긴 있습니다만, PolyKinds 확장을 켜면, 더 일반적인 카인드로 추론하게 할 수 있습니다.

PolyKinds확장을 켜면 App의 카인드를 이렇게 추론합니다.

forall k. (k -> Type) -> k -> Type

아래 같이 구체 카인드로 추론하는 걸 인스턴스를 만들었다, 인스턴스화 되었다, 인스턴스다라고 말합니다.

data App f a = MkApp (f a)

App Maybe Int -- App의 카인드안에 있는 k가 Type으로 인스턴스화 됐다고 말합니다. (is instantiated to)
data T a = mkT (a Int) -- `a`는 `(Type -> Type)`으로 추론하고,

App T Maybe -- `k`는 (Type -> Type) 으로 추론됩니다.

(작성중)