확장 DataKinds (작성 중)

Posted on January 5, 2023

GHC 공식 가이드 - 6.4.10. Datatype promotion

promote: 위치나 순위를 더 높거나 중요한 곳으로 끌어 올리는 것

적당한 데이터 타입들을 자동으로 카인드로 끌어올리는promote 확장입니다. 값 생성자는 타입 생성자가 됩니다.

data Nat = Zero | Succ Nat

타입 생성자 Nat과, 값 생성자 Zero, Succ는 자동으로 끌어 올려져promoted
Nat라는 카인드가 생기고, Zero, Succ라는 타입이 생깁니다.

data List a = Nil | Cons a (List a)

List 카인드가 생기고, Nil, Cons 타입이 생깁니다.

GHC 8에서 도입된 TypeInType확장으로 카인드도 Type이라는 타입으로 보게 되어, 조금 머리가 복잡해졌습니다. 타입의 분류를 나타내는 카인드도 타입으로 봅니다. 러셀의 역설마냥 지라르의 역설로 불린다고 합니다.

연관 확장
Type families
GADTs (Generalized Algebraic Data Types) TypeInType (deprecated 되었고, PolyKinds를 보시면 됩니다.)
PolyKinds

(작성 중)

Github 계정이 없는 분은 메일로 보내주세요. lionhairdino at gmail.com