Comment traiter un GADT récursif avec kind :: '[SomeDataKind]

Question

Je pense que c'est le plus loin dans les extensions de système de type Haskell que j'ai déjà été et j'ai couru dans une erreur que je n'ai pas pu se rendre compte. Excuses d'avance pour la longueur, c'est l'exemple le plus court que je puisse créer qui illustre encore le problème que j'ai. J'ai un GADT récursive dont type est une liste promu, quelque chose comme ce qui suit:

GADT Définition

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

Problème

Ce que je suis en train de faire est de parcourir les données et effectuer certaines opérations, par exemple propager le premier JustChar trouvé au sommet.

caractéristiques Annoying manquantes - nécessaires pour la section suivante

maintenant, parce qu'il n'y a apparemment pas de soutien de la syntaxe des enregistrements pour vous GADTs (https://ghc.haskell.org/trac/ghc/ticket/2595) besoin de les écrire manuellement, donc ils sont ici:

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 

données de test

donc, la chose que je veux faire. Descendez la structure du haut jusqu'à ce que je trouve une valeur qui est Just. Ainsi, compte tenu des valeurs initiales suivantes:

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) 

Résultat attendu

Je voudrais avoir quelque chose comme ceci:

> 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)))) 

Tentatives

Je pris quelques coups de couteau à cela, d'abord avec une fonction régulière:

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 

Cela donne à l'erreur:

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. 

J'ai essayé aussi une classe de types et de tenter de faire correspondre à la structure:

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 

Il en résulte l'erreur:

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. 

J'ai également essayé des combinaisons de correspondance sur SomeData '[] et SomeData '[p] en vain. J'espère avoir manqué quelque chose de simple mais je n'ai pas trouvé de documentation sur la façon de traiter une structure comme celle-ci et je suis à la limite de ma compréhension si le système de type Haskell, pour l'instant de toute façon:).Une fois de plus, désolé pour le poste long et toute aide serait grandement appréciée :)

Answer 1

L'erreur que vous obtenez est un hareng rouge - GHC ne peut pas déduire les types de fonctions sur GADTs. Vous devez lui donner une signature de type pour voir l'erreur réelle:

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

Cela donne l'erreur:

* 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 

Si on ne sait pas, ce message d'erreur indique que nous prétendons que le type arguement à SomeData est juste une variable (c'est-à-dire, nous n'en savons rien, sauf son genre) mais l'utilisation de certaines fonctions à l'intérieur propogate exige qu'il soit de la forme p0 : parts0 pour certains types p0 : parts0.

Cependant, vous dites au début:

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

mais le compilateur ne sait pas! Vous devez le dire, et typiquement ceci est fait par la correspondance de modèle sur un constructeur de GADT qui apporte une égalité de type dans la portée. Votre seul problème ici est que vous devrez faire correspondre sur trois constructeurs, qui auraient tous le même code. La solution est de supprimer le double de votre type de données:

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 

paquets comme singletons va générer le type SDataKind et des fonctions connexes du type pour vous automatiquement.

Toutes vos fonctions « record » sont grandement simplifiées:

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 

Et maintenant, afin d'obtenir votre fonction Typecheck (car il est en effet correct sémantiquement), tout ce que vous devez faire est de correspondance de motif sur le constructeur:

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

Notez que le code est identique, sauf l'addition d'une signature de type et @Mk{} après le modèle de variable sd. Enfin, essayer d'utiliser des typeclasses ici ne vous donne rien - vous avez déjà un type indexé qui contient toutes les informations (de type) dont vous avez besoin - vous obtenez ces informations par la recherche de modèles sur les constructeurs de ce type.

---

Notez également que vous ne perdez pas de généralité SomeData - si vous voulez des indices particuliers d'avoir des informations supplémentaires, vous ajoutez simplement un autre champ indexé sur le part.Vous pouvez même logique intégré complexe à l'intérieur du champ supplémentaire, car le champ SDataKind vous permet de matcher motif sur l'indice à volonté:

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 

---

Enfin, si vous souhaitez frayer un chemin le long du parcours original, vous peut le faire, mais la source de la duplication de code doit être très apparente:

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

Cela peut sembler un peu passe-partout-ish, mais si vous écrivez juste les trois cas de propagate, alors il peut être simple (si un peu verbeux):

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