친절한 서명

Question

하스켈 위키 책을 통해 가고 있습니다. GADTS

https://en.wikibooks.org/wiki/Haskell/GADT 가이드.

Cons 생성자의 제한된 유형을 일반화하는 Kind 서명이 추가 될 때까지 나는 꽤 잘 추적하고있었습니다.

data Safe 
data NotSafe 

data MarkedList    :: * -> * -> * where 
    Nil      :: MarkedList t NotSafe 
    Cons      :: a -> MarkedList a b -> MarkedList a c 

safeHead     :: MarkedList a Safe -> a 
safeHead (Cons x _)   = x 


silly 0      = Nil 
silly 1      = Cons() Nil 
silly n      = Cons() $ silly (n-1) 

Kind Signature를 사용하여 안전 및 안전하지 않은 MarkedLists에 대해 일치 및 패턴 일치를 생성 할 수 있습니다. 무슨 일이 벌어지고 있는지 이해하는 동안 나는 불행히도 친절한 서명이 이것을 어떻게 허용하는지에 대한 직관을 구축하는 데 어려움을 겪고 있습니다. 왜 나는 친절한 서명이 필요한가요? Kind Signature는 무엇을하고 있습니까?

Answer 1

유형 서명이 값에 대해 작동하는 것과 같은 방식으로 유형 서명이 유형에 대해 작동합니다. 여기

f :: Int -> Int -> Bool 
f x y = x < y 

는 f 두 인수 값을 취한 후 결과 값을 생성한다. 타입 등가가 될 수있다 :이

data D a b = D a b 

유형 D 두 인수의 형태를 취하고 결과 유형 (이 * -> * -> * 임) 생산한다. 예를 들어, D Int String은 종류입니다 (종류는 *입니다). 부분 신청 D Int은 부분 신청 f 15의 유형이 Int -> Bool 인 것과 똑같은 종류 * -> *입니다.

그래서 우리는 다시 쓸 수 있기 때문에 위 :

data D :: * -> * -> * where 
    D :: a -> b -> D a b 

GHCi에서, 당신은 유형과 종류를 조회 할 수 있습니다

임은 여전히 ​​MarkedList AB '때문에 혼란