GADT를 사용하는 "안전한 목록"을위한 테일 기능

Question

나는 a GADT walkthrough을 통해 읽고 있었고 연습 중 하나에서 멈추었습니다. 주어진 자료 구조는 다음과 같습니다

{-# LANGUAGE GADTs, EmptyDataDecls, KindSignatures #-} 
data NotSafe 
data Safe 
data MarkedList :: * -> * -> * where 
    Nil :: MarkedList t NotSafe 
    Cons :: a -> MarkedList a b -> MarkedList a c 

운동은 safeTail 기능을 구현하는 것입니다.

safeTail (Cons 'c' (Cons 'a' (Cons 't' Nil))) == Cons 'a' (Cons 't' Nil) 
safeTail (Cons 'x' Nil)      == Nil 
safeTail Nil -- type error (not runtime!) 

^{가 (실제로 ==을 정의하지 않았다, 그러나 희망이 무슨 뜻인지 분명)}

이이

을 수행 할 수 있습니다 : 나는 서곡에 tail 기능과 비슷한 역할을하고 싶습니다? 나는 타입이 심지어 무엇이 될지 전혀 모른다. 아마 safeTail :: MarkedList a Safe -> MarkedList a NotSafe?

Answer 1

당신이 유형의 구조를 조금 변경하는 경우 safeTail을 구현할 수 :

{-# LANGUAGE GADTs, EmptyDataDecls, KindSignatures #-} 

data Safe a 
data NotSafe 

data MarkedList :: * -> * -> * where 
    Nil :: MarkedList t NotSafe 
    Cons :: a -> MarkedList a b -> MarkedList a (Safe b) 

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

safeTail :: MarkedList a (Safe b) -> MarkedList a b 
safeTail (Cons _ t) = t 

원래 safeTail :: MarkedList a Safe -> MarkedList a b의 문제는 b 어떤 유형이 될 수 있다는 것입니다 - 반드시 같은 종류 그의 꼬리 목록에으로 표시됩니다. 이것은 리턴 타입이 safeTail 인 것을 허용하는 타입 레벨에리스트 구조를 적절히 제한함으로써 여기에서 고쳐졌습니다.

Answer 2

예, 가능합니다. 그 트릭은 존재 적으로 정량화 된 포함 목록을 알려진 유형의 목록으로 바꾸는 것입니다. 구체적으로는 NotSafe입니다.

unsafe :: MarkedList a b -> MarkedList a NotSafe 
unsafe Nil = Nil 
unsafe (Cons a b) = Cons a b 

이제 우리는 안전하게 꼬리를 취할 수 있습니다

safeTail :: MarkedList a Safe -> MarkedList a NotSafe 
safeTail (Cons a b) = unsafe b 

또한이 패턴 일치가 완료됩니다. -fwarn-incomplete-patterns에서 경고를받지 못하며 Nil 절을 추가하려고하면 오류가 발생합니다. 의는 Show 인스턴스를 도출, StandaloneDeriving 켜고 귀하의 샘플을 테스트 해보자 5 분전까지 장에서 링크 된 솔루션은 분명히 잘못했다

가

*Main> safeTail (Cons 'c' (Cons 'a' (Cons 't' Nil))) 
Cons 'a' (Cons 't' Nil) 
*Main> safeTail (Cons 'x' Nil) 
Nil 
*Main> safeTail Nil 

<interactive>:10:10: 
    Couldn't match type `NotSafe' with `Safe' 
    Expected type: MarkedList a0 Safe 
     Actual type: MarkedList a0 NotSafe 
    In the first argument of `safeTail', namely `Nil' 
    In the expression: safeTail Nil 
    In an equation for `it': it = safeTail Nil