Vecteur contenant GADT

Question

Je suis en train d'apprendre tout ce que je peux sur ExistingentialQuantification et GADTs et KindSignatures, etc Et pour ce faire, j'essaie de trouver de petits programmes qui m'aident à mieux comprendre tout.

Maintenant, j'ai ce petit extrait (qui compile en fait, vous pouvez l'essayer sur votre propre, nécessite vecteur et mtl paquets) et je voudrais savoir s'il est tout possible de faire ce que je suis en essayant d'accomplir ou me guider sur la façon de faire fonctionner

{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE ExistentialQuantification #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE GADTs #-} 
{-# LANGUAGE Rank2Types #-} 
import Control.Monad.State.Lazy 
import qualified Data.Vector as V 

data MenuItem = ListS | ActionS | SliderS 

data MenuItemReference (a :: MenuItem) (n :: *) where 
     MenuListSReference :: Int -> MenuItemReference ListS Int 
     MenuActionSReference :: Int -> MenuItemReference ActionS Int 
     MenuSliderSReference :: Int -> MenuItemReference SliderS Int 

data MyState = MyState { vec :: forall a. V.Vector (MenuItemReference a Int) } 

newMyState :: MyState 
newMyState = MyState { vec = V.empty } 

listRef :: MenuItemReference ListS Int 
listRef = MenuListSReference 5 

actionRef :: MenuItemReference ActionS Int 
actionRef = MenuActionSReference 3 

myComputation :: State MyState() 
myComputation = do 
    addItem listRef 
    addItem actionRef 
    return() 

addItem :: forall a. MenuItemReference a Int -> State MyState() 
addItem menuItemRef = do 
    s <- get 
    put (s { vec = (vec s) `V.snoc` menuItemRef }) 

main :: IO() 
main = do 
    print $ evalState myComputation newMyState 

Comme vous pouvez le voir, je suis en train d'obtenir un vecteur de MenuItemReferences dans ce ... Qu'est-ce que je fais mal parce qu'avec ce J'ai pour l'instant l'erreur:

Couldn't match type ‘a’ with ‘a1’ 
    ‘a’ is a rigid type variable bound by 
     the type signature for 
     addItem :: MenuItemReference a Int -> State MyState() 
     at Main.hs:34:19 
    ‘a1’ is a rigid type variable bound by 
     a type expected by the context: V.Vector (MenuItemReference a1 Int) 
     at Main.hs:37:10 
Expected type: MenuItemReference a1 Int 
    Actual type: MenuItemReference a Int 
Relevant bindings include 
    menuItemRef :: MenuItemReference a Int (bound at Main.hs:35:9) 
    addItem :: MenuItemReference a Int -> State MyState() 
    (bound at Main.hs:35:1) 
In the second argument of ‘V.snoc’, namely ‘menuItemRef’ 
In the ‘vec’ field of a record 

Est-ce que quelqu'un pourrait expliquer quelle est la raison de l'erreur et comment je pourrais approcher (si possible) la chose que j'essaie d'accomplir.

Answer 1

Pourquoi ne pas simplement

data MenuItemReference = 
    MenuListSReference Int | 
    MenuActionSReference Int | 
    MenuSliderSReference Int 

alors?

Le constructeur utilisé annote déjà la valeur. Vous n'avez pas besoin d'injecter le type fantôme, car l'information est déjà présente. De plus, cela impliquerait que GHC ({-# LANGUAGE ImpredicativeTypes #-}) prenne en charge impredicative polymorphism pour construire Vector [forall a. MenuItemReference a Int] et l'utilise de manière polymorphe. Bien que cela soit favorable, le soutien a été décrit comme «fragile au mieux et brisé au pire».

En guise de note, this nice blog post explique comment nous pouvons nous débarrasser des types imprédicatifs, en utilisant newtype s et RankNTypes à la place. Cela vous oblige à introduire une couche de newtype, cependant.