Haskell의 DataKinds 확장은 무엇입니까?

Haskell의 DataKinds 확장은 무엇입니까?

---

나는 Learn You a Haskell 을 읽었 기 때문에 나에게 의미가있는 DataKinds 확장에 대한 설명을 찾으려고합니다 . 내가 배운 것을 조금만 가지고도 이해할 수있는 표준 소스가 있습니까?

편집 : 예를 들어 문서 에는

-XDataKinds를 사용하면 GHC는 자동으로 적합한 모든 데이터 유형을 종류로, 해당 (값) 생성자를 유형 생성자로 승격합니다. 다음 유형

그리고 예를 제공합니다

data Nat = Ze | Su Nat

다음과 같은 종류 및 유형 생성자를 발생시킵니다.

Nat :: BOX
Ze :: Nat
Su :: Nat -> Nat

나는 요점을 이해하지 못한다. 나는 이해하지 않지만 BOX수단, 문을 Ze :: Nat및 Su :: Nat -> Nat당신이 ghci로 볼 기대로 '제 및 스와 일반 데이터 생성자가 정확히하는 경우 일반적으로 이미 어떤 상태로 보인다

Prelude> :t Su
Su :: Nat -> Nat

---

기본부터 시작하겠습니다.

종류

종류는 유형의 유형 *입니다. 예 :

Int :: *
Bool :: *
Maybe :: * -> *

공지 ->너무 친절 수준에서 평균 "기능"에 오버로드됩니다. *일반적인 Haskell 유형도 마찬가지 입니다.

우리는 GHCi에게 :k.

데이터 종류

우리는 우리 자신의 종류를 만들 방법이 없기 때문에 이것은별로 유용하지 않습니다! 와 함께 DataKinds쓸 때

 data Nat = S Nat | Z

GHC는이를 홍보하여 ​​상응하는 종류를 Nat만들고

 Prelude> :k S
 S :: Nat -> Nat
 Prelude> :k Z
 Z :: Nat

그래서 DataKinds는 종류 시스템을 확장 가능하게 만듭니다.

용도

GADT를 사용하여 프로토 타입 종류의 예를 살펴 보겠습니다.

 data Vec :: Nat -> * where
    Nil  :: Vec Z
    Cons :: Int -> Vec n -> Vec (S n)

이제 Vec유형이 길이별로 색인화되어 있음을 알 수 있습니다.

이것이 기본 10k 피트 개요입니다.

* 이것은 실제로 계속됩니다. Values : Types : Kinds : Sorts ...일부 언어 (Coq, Agda ..)는이 무한한 우주 스택을 지원하지만 Haskell은 모든 것을 한 종류로 묶습니다.

---

내 의견은 다음과 같습니다.

다음 유형의 길이 인덱스 벡터를 고려하십시오.

data Vec n a where
  Vnil  :: Vec Zero a
  Vcons :: a -> Vec n a -> Vec (Succ n) a

data Zero
data Succ a

여기에 종류가 Vec :: * -> * -> *있습니다. Int의 길이가 0 인 Vector를 다음과 같이 나타낼 수 있기 때문입니다.

Vect Zero Int

의미없는 유형을 다음과 같이 선언 할 수도 있습니다.

Vect Bool Int

이것은 우리가 유형 수준에서 유형화되지 않은 함수형 프로그래밍을 가질 수 있음을 의미합니다. 따라서 데이터 종류를 도입하여 이러한 모호성을 제거하고 다음과 같은 종류를 가질 수 있습니다.

Vec :: Nat -> * -> *

이제 우리 Vec는 다음 Nat과 같이 선언 할 수 있는 DataKind를 얻습니다 .

datakind Nat = Zero | Succ Nat

By introducing a new data kind, no one can declare a meaningless type since Vec now has a more constrained kind signature.

ReferenceURL : https://stackoverflow.com/questions/20558648/what-is-the-datakinds-extension-of-haskell