Tail-Funktion für "sichere Liste" mit GADTs

Question

Ich las durch a GADT walkthrough und blieb bei einer der Übungen stecken. Die gegebene Datenstruktur ist:

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

Die Übung ist eine safeTail Funktion zu implementieren. Ich mag es ähnlich wie die tail Funktion in Prelude handeln:

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

^{(ich eigentlich nicht == definieren, aber hoffentlich ist es klar, was ich meine)}

Kann dies geschehen? Ich bin mir nicht ganz sicher, was der Typ überhaupt wäre ... vielleicht safeTail :: MarkedList a Safe -> MarkedList a NotSafe?

Answer 1

Es ist möglich, safeTail zu implementieren, wenn Sie die Typ-Struktur ein wenig ändern:

{-# 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 

Das Problem mit den ursprünglichen safeTail :: MarkedList a Safe -> MarkedList a b ist, dass b jede Art sein kann - nicht unbedingt die gleiche Art, dass der Schwanz der Liste ist mit markiert. Dies wird hier behoben, indem die Listenstruktur auf der Typ-Ebene reflektiert wird, wodurch der Rückgabetyp safeTail entsprechend eingeschränkt werden kann.

Answer 2

Ja, es kann getan werden. Der Trick besteht darin, diese existenziell quantifizierte enthaltene Liste in eine Liste eines bekannten Typs zu verwandeln: nämlich eine!

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

Jetzt können wir den Schwanz sicher nehmen:

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

Zusätzlich dieses Muster Spiel abgeschlossen ist. Sie erhalten keine Warnung von -fwarn-incomplete-patterns, und wenn Sie versuchen, eine Nil Klausel hinzuzufügen, erhalten Sie einen Fehler. Lassen Sie uns auf StandaloneDeriving drehen, leiten eine Show Instanz und testen Sie Ihre Proben:

*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