Wie man eine rekursive GADT mit Art :: '[SomeDataKind] verarbeitet

Question

Ich denke, das ist die am weitesten in die Haskell-Typ Systemerweiterungen, die ich schon gewesen bin und ich habe einen Fehler, die ich nicht in der Lage war herausfinden. Ich entschuldige mich im Voraus für die Länge, es ist das kürzeste Beispiel, das ich erstellen konnte, das immer noch das Problem veranschaulicht, das ich habe. Ich habe eine rekursive GADT deren Art ist eine Liste gefördert, etwa wie folgt:

GADT Definition

{-# LANGUAGE StandaloneDeriving #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE FlexibleInstances #-} 
{-# LANGUAGE GADTs #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE TypeOperators #-} 

data DataKind = A | B | C 

-- 'parts' should always contain at least 1 element which is enforced by the GADT. 
-- Lets call the first piece of data 'val' and the second 'subdata'. 
-- All data constructors have these 2 fields, although some may have 
-- additional fields which I've omitted for simplicity. 
data SomeData (parts :: [DataKind]) where 
    MkA :: Maybe Char -> Maybe (SomeData subparts) -> SomeData ('A ': subparts) 
    MkB :: Maybe Char -> Maybe (SomeData subparts) -> SomeData ('B ': subparts) 
    MkC :: Maybe Char -> Maybe (SomeData subparts) -> SomeData ('C ': subparts) 
deriving instance Show (SomeData parts) 

Problem

Was ich versuche, die Daten zu tun durchlaufen ist und führe einige Operationen aus, zum Beispiel propagiere die erste JustChar, die bis oben gefunden wurde.

Annoying fehlende Features - erforderlich für den nächsten Abschnitt

Jetzt, da es für GADTs offenbar keine Aufzeichnung Syntax-Unterstützung ist (https://ghc.haskell.org/trac/ghc/ticket/2595) Sie müssen sie manuell schreiben, also hier sind sie:

getVal :: SomeData parts -> Maybe Char 
getVal (MkA val _) = val 
getVal (MkB val _) = val 
getVal (MkC val _) = val 

-- The lack of record syntax for GADTs is annoying. 
updateVal :: Maybe Char -> SomeData parts -> SomeData parts 
updateVal val (MkA _val sub) = MkA val sub 
updateVal val (MkB _val sub) = MkB val sub 
updateVal val (MkC _val sub) = MkC val sub 

-- really annoying... 
getSubData :: SomeData (p ': rest) -> Maybe (SomeData rest) 
getSubData (MkA _ sub) = sub 
getSubData (MkB _ sub) = sub 
getSubData (MkC _ sub) = sub 

Testdaten

Also, die Sache will ich tun. Gehe die Struktur von oben nach unten, bis ich einen Wert gefunden habe, der Just ist. So gegeben folgende Anfangswerte:

a :: SomeData '[ 'A ] 
a = MkA (Just 'A') Nothing 

b :: SomeData '[ 'B ] 
b = MkB (Just 'B') Nothing 

c :: SomeData '[ 'C ] 
c = MkC (Just 'C') Nothing 

bc :: SomeData '[ 'B, 'C ] 
bc = MkB Nothing (Just c) 

abc :: SomeData '[ 'A, 'B, 'C ] 
abc = MkA Nothing (Just bc) 

Erwartetes Ergebnis

Ich mag so etwas wie dieses haben würde:

> abc 
MkA Nothing (Just (MkB Nothing (Just (MkC (Just 'C') Nothing)))) 
> propogate abc 
MkA (Just 'C') (Just (MkB (Just 'C') (Just (MkC (Just 'C') Nothing)))) 

Frühere Versuche

nahm ich ein paar Stichen bei ihm zuerst mit einer regulären Funktion:

propogate sd = 
    case getVal sd of 
     Just _val -> 
      sd 
     Nothing -> 
      let 
       newSubData = fmap propogate (getSubData sd) 
       newVal = join . fmap getVal $ newSubData 
      in 
       updateVal newVal sd 

Dies gibt den Fehler:

Broken.hs:(70,1)-(81,35): error: … 
    • Occurs check: cannot construct the infinite type: rest ~ p : rest 
     Expected type: SomeData rest -> SomeData (p : rest) 
     Actual type: SomeData (p : rest) -> SomeData (p : rest) 
    • Relevant bindings include 
     propogate :: SomeData rest -> SomeData (p : rest) 
      (bound at Broken.hs:70:1) 
Compilation failed. 

Ich habe auch versucht ein typeclass und versucht, auf die Struktur anzupassen:

class Propogate sd where 
    propogateTypeClass :: sd -> sd 

-- Base case: We only have 1 element in the promoted type list. 
instance Propogate (SomeData parts) where 
    propogateTypeClass sd = sd  

-- Recursie case: More than 1 element in the promoted type list. 
instance Propogate (SomeData (p ': parts)) where 
    propogateTypeClass sd = 
     case getVal sd of 
      Just _val -> 
       sd 
      Nothing -> 
       let 
        -- newSubData :: Maybe subparts 
        -- Recurse on the subdata if it exists. 
        newSubData = fmap propogateTypeClass (getSubData sd) 
        newVal = join . fmap getVal $ newSubData 
       in 
        updateVal newVal sd 

Diese im Fehler führt:

Broken.hs:125:5-26: error: … 
    • Overlapping instances for Propogate (SomeData '['A, 'B, 'C]) 
     arising from a use of ‘propogateTypeClass’ 
     Matching instances: 
     instance Propogate (SomeData parts) 
      -- Defined at Broken.hs:91:10 
     instance Propogate (SomeData (p : parts)) 
      -- Defined at Broken.hs:95:10 
    • In the expression: propogateTypeClass abc 
     In an equation for ‘x’: x = propogateTypeClass abc 
Compilation failed. 

Ich habe auch Kombinationen von Matching aufversuchtund SomeData '[p] vergeblich.

Ich hoffe, ich vermisse etwas Einfaches, aber ich habe keine Dokumentation nirgendwo gefunden, wie man eine Struktur wie folgt verarbeitet und ich bin an der Grenze meines Verständnisses, wenn das Haskell-System, für jetzt sowieso:).Noch einmal, Entschuldigung für die lange Post und jede Hilfe würde sehr geschätzt werden :)

Answer 1

Der Fehler, den Sie bekommen, ist ein Ablenkungsmanöver - GHC kann nicht die Arten von Funktionen auf GADTs ableiten. Sie müssen sie eine Art Unterschrift geben den wirklichen Fehler zu sehen:

propogate :: SomeData x -> SomeData x 
.... 

Das den Fehler gibt:

* Couldn't match type `x' with `p0 : parts0' 
    `x' is a rigid type variable bound by 
    the type signature for: 
     propogate :: forall (x :: [DataKind]). SomeData x -> SomeData x 
    Expected type: SomeData (p0 : parts0) 
    Actual type: SomeData x 

Wenn es nicht klar ist, wird diese Fehlermeldung besagt, dass wir behaupten, dass der Typ arguement zu SomeData ist nur eine Variable (das heißt, wir wissen nichts darüber, außer seiner Art), aber die Verwendung einiger Funktionen innerhalb propogate erfordern es in der Form p0 : parts0 für einige Typen p0 : parts0 sein.

jedoch angeben, die Sie am Anfang:

'parts' should always contain at least 1 element which is enforced by the GADT.

aber der Compiler dies nicht wissen! Sie müssen es sagen, und in der Regel wird dies durch Mustererkennung in einem GADT-Konstruktor getan, der eine Gleichheit des Typs in den Geltungsbereich bringt. Ihr einziges Problem hier ist, dass Sie auf drei Konstruktoren, die alle den gleichen Code hätten, abgleichen müssten. Die Lösung ist das Duplikat aus dem Datentyp zu entfernen:

data SomeData (parts :: [DataKind]) where 
    Mk :: SDataKind s -> Maybe Char -> Maybe (SomeData subparts) -> SomeData (s ': subparts) 

data SDataKind (x :: DataKind) where 
    SA :: SDataKind A 
    SB :: SDataKind B 
    SC :: SDataKind C 

Pakete wie singletons werden für Dich automatisch die SDataKind Art und verwandte Funktionen von der Art erzeugen.

Alle Ihre ‚Record‘ Funktionen stark vereinfacht werden:

getVal :: SomeData parts -> Maybe Char 
getVal (Mk _ v _) = v 

updateVal :: Maybe Char -> SomeData parts -> SomeData parts 
updateVal val (Mk t _val sub) = Mk t val sub 

getSubData :: SomeData (p ': rest) -> Maybe (SomeData rest) 
getSubData (Mk _ _ sub) = sub 

Und jetzt, um Ihre Funktion zu erhalten, typecheck (da es in der Tat richtig semantisch ist), alles, was Sie tun müssen, ist auf Mustererkennung der Konstruktor:

propogate :: SomeData x -> SomeData x 
propogate sd@Mk{} = 
    .... -- unchanged 

anzumerken, dass der Code identisch ist, außer der Hinzufügung eines Typ Signatur und @Mk{} nach dem variablen Muster sd.

Schließlich geben Sie hier nichts, wenn Sie versuchen, typeclasses zu verwenden - Sie haben bereits einen indizierten Typ, der alle erforderlichen Informationen enthält. Sie erhalten diese Informationen durch Mustervergleich für die Konstruktoren dieses Typs.

---

Beachten Sie auch, Sie keine Allgemeinheit in SomeData verlieren - wenn Sie bestimmte Indizes wünschen zusätzliche Informationen haben, können Sie einfach ein anderes Feld hinzufügen, auf dem part indiziert.Sie können auch komplexe Logik innerhalb des zusätzlichen Feldes einbetten, wie das SDataKind Feld, das Sie Muster auf dem Index nach Belieben Spiel ermöglicht:

data SomeData (parts :: [DataKind]) where 
    Mk :: SDataKind s 
    -> DataPart s 
    -> Maybe Char 
    -> Maybe (SomeData subparts) 
    -> SomeData (s ': subparts) 

type family (==?) (a :: k) (b :: k) :: Bool where 
    a ==? a = 'True 
    a ==? b = 'False 

-- Example - an additional field for only one index, without duplicating 
-- the constructors for each index 
data DataPart x where 
    Nil :: ((x ==? 'A) ~ 'False) => DataPart x 
    A_Data :: Integer -> DataPart A 

---

Schließlich, wenn Sie auf dem ursprünglichen Kurs stapfen möchten, können Sie so tun, aber die Quelle der Code-Duplizierung sollte sehr deutlich werden:

partsUncons :: SomeData ps0 -> (forall p ps . (ps0 ~ (p : ps)) => r) -> r 
partsUncons MkA{} x = x 
partsUncons MkB{} x = x 
partsUncons MkC{} x = x 

propogate :: SomeData x -> SomeData x 
propogate sd = partsUncons sd $ 
    .... -- unchanged 

Answer 2

Dies könnte ein wenig vorformulierten-ish erscheinen, aber wenn man nur die drei Fälle von propagate schreiben, dann kann es einfach gemacht werden (wenn ein bisschen ausführlich):

import Control.Monad (mplus) 
import Control.Arrow (second) 

propagate' :: (Maybe Char -> Maybe (SomeData ps) -> SomeData ps') 
      -> Maybe Char -> Maybe (SomeData ps) -> (Maybe Char, SomeData ps') 
propagate' mk c ds = (c'', mk c'' ds') 
    where 
    (c', ds') = maybe (Nothing, Nothing) (second Just . propagate) ds 
    c'' = c `mplus` c' 

propagate :: SomeData ps -> (Maybe Char, SomeData ps) 
propagate (MkA c ds) = propagate' MkA c ds 
propagate (MkB c ds) = propagate' MkB c ds 
propagate (MkC c ds) = propagate' MkC c ds