包含GADT的向量

我只是在学习关于存在性量化，GADT和KindSignatures等的所有事情。为此，我尝试想出一些小程序，这些程序可以帮助我更好地理解所有内容。包含GADT的向量

现在我有了这个小片段（这实际上编译，所以你可以尝试一下你自己，需要矢量和MTL包），并想知道它是否是在所有可能做的我是什么试图完成或指导我如何使它工作

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

正如你可以看到我想要得到它MenuItemReferences的矢量...它是什么，我因为做错了什么我现在有错误：

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

有人能解释一下这个错误背后的原因，以及我如何能够接近（如果可能的话）我试图完成的事情。

来源

2015-11-16 ksaveljev

那么我看到的问题是你量化矢量，而不是它的内部;考虑一下。 [a]'vs'[forall a。一]'。话虽如此，显而易见的变化产生了“非法多态或合格类型：...... GHC尚不支持impandicative多态性，我不知道如何解决，tbh。但是再一次，你的'MenuItemReference'类型似乎有点奇怪 - 'a'看起来像一个幻象类型，但我不知道它应该做什么。 –

这是一个精简的例子，只是为了显示问题。 'MenuItemReference'应该用来从我的状态中的其他集合中获取正确的项目。因此'MenuItemReference ListS Int'会从'menuListItems'中获取某些东西，'MenuItemReferences ActionS Int'会从'menuActionItems'等等获取某物（'menuListItems'和'menuActionItems'在'MyState'中，它们是* Vectors *不同的数据类型） – ksaveljev

哦......我的......上帝......谢谢你Bartek！我其实并没有看到（我的意思是重复）。你是对的，这是无用的重复，而构造者自己给我提供了足够的信息。非常感谢您指出这一点！ – ksaveljev

为什么不

data MenuItemReference = 
    MenuListSReference Int | 
    MenuActionSReference Int | 
    MenuSliderSReference Int

呢？

使用的构造函数已经注释了该值。您不需要注入幻像类型，因为信息已经存在。

此外，这样做需要启用GHC（{-# LANGUAGE ImpredicativeTypes #-}）实际支持impredicative polymorphism构造Vector [forall a. MenuItemReference a Int]并以多形方式使用它。虽然它确实支持这一点，但支持被形容为“最多是脆弱的，最坏的情况是坏的”。

作为附注this nice blog post解释了我们如何摆脱impandicative类型，使用newtype s和RankNTypes来代替。但是，这确实需要您引入一层newtype。

来源

2015-11-16 11:45:49

包含GADT的向量

回答

相关问题