Programmation de type niveau imbriquée

Question

J'essaie d'utiliser DataKinds pour effectuer une programmation au niveau du type, mais je rencontre des difficultés lorsque l'une de ces structures est imbriquée dans une autre.

{-# LANGUAGE DataKinds, TypeFamilies, GADTs, MultiParamTypeClasses, FlexibleInstances #-} 

module Temp where 

data Prop1 = D | E 

data Lower :: Prop1 -> * where 
    SubThing1 :: Lower D 
    SubThing2 :: Lower E 

class ClassLower a where 
    somefunc2 :: a -> String 

instance ClassLower (Lower D) where 
    somefunc2 a = "string3" 

instance ClassLower (Lower E) where 
    somefunc2 a = "string4" 

data Prop2 = A | B | C 

data Upper :: Prop2 -> * where 
    Thing1 :: Upper A 
    Thing2 :: Upper B 
    Thing3 :: Lower a -> Upper C 

class ClassUpper a where 
    somefunc :: a -> String 

instance ClassUpper (Upper A) where 
    somefunc a = "string1" 

instance ClassUpper (Upper B) where 
    somefunc a = "string2" 

instance ClassUpper (Upper C) where 
    somefunc (Thing3 x) = somefunc2 x 

Dès que j'ajoute que la dernière instance de ClassUpper, je me retrouve avec une erreur.

Temp.hs:37:25: error: 
    • Could not deduce (ClassLower (Lower a)) 
     arising from a use of ‘somefunc2’ 
     from the context: 'C ~ 'C 
     bound by a pattern with constructor: 
        Thing3 :: forall (a :: Prop1). Lower a -> Upper 'C, 
       in an equation for ‘somefunc’ 
     at /Users/jdouglas/jeff/emulator/src/Temp.hs:37:13-20 
    • In the expression: somefunc2 x 
     In an equation for ‘somefunc’: somefunc (Thing3 x) = somefunc2 x 
     In the instance declaration for ‘ClassUpper (Upper 'C)’ 

Je comprends que 'C ~ 'C indique le type d'égalité, mais je ne comprends pas ce que le problème sous-jacent est, beaucoup moins la solution ou solution de contournement. Qu'est-ce que je ne comprends pas, et quel est le meilleur moyen de résoudre ce problème?

Answer 1

Ou vous pouvez écrire votre distinguer les cas de la GADT ClassLower par exemple comme celui-ci, en utilisant la correspondance de motif (plutôt que la variable de type):

instance ClassLower (Lower a) where 
    somefunc2 SubThing1 = "string3" 
    somefunc2 SubThing2 = "string4" 

Answer 2

Le problème ici est un peu subtil. La raison pour laquelle on peut s'attendre à ce que GHC accepte ceci est que vous avez des instances pour tous les Lower a possibles puisque vous ne fournissez que des façons de faire Lower D et Lower E. Cependant, on pourrait construire une définition pathologique pour Lower comme

import GHC.Exts (Any) 

data Lower :: Prop1 -> * where 
    SubThing1 :: Lower D 
    SubThing2 :: Lower E 
    SubThing3 :: Lower Any 

Le point est que non seulement D et E ont Prop1 genre. Ce n'est pas seulement avec des choses comme Any que nous pouvons jouer de telles manigances - même le constructeur suivant est autorisé (donc aussi)!

SubThing4 :: Lower (F Int) 

type family F x :: Prop1 where {} 

Donc, en résumé, le problème sous-jacent est que GHC ne peut vraiment pas être sûr que la contrainte ClassLower (Lower a) (nécessaire en raison de l'utilisation de somefunc2) va être satisfait. Pour ce faire, il faudrait faire un peu de travail en vérifiant les constructeurs GADT et en s'assurant que chaque cas possible est couvert par une instance. Dans ce cas, vous pouvez résoudre votre problème en ajoutant la contrainte ClassLower (Lower a) au constructeur GADT (un FlexibleContexts).

data Upper :: Prop2 -> * where 
    Thing1 :: Upper A 
    Thing2 :: Upper B 
    Thing3 :: ClassLower (Lower a) => Lower a -> Upper C