Vector containing GADT

Question

I'm just learning everything I can about ExistentialQuantification and GADTs and KindSignatures, etc. And to do that I try to come up with some small programs which help me to understand everything better.

Now I have this small snippet (which actually compiles, so you can try it on your own, requires vector and mtl packages) and would like to know whether it is at all possible to do what I am trying to accomplish or guide me to how to make it work

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

As you can see I'm trying to get a Vector of MenuItemReferences in it... What is it that I'm doing wrong because with what I have at the moment I get the error:

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

Could someone explain what is the reason behind the error and how I could approach (if at all possible) the thing I am trying to accomplish.

Well the problem that I see is that you quantified the Vector, not the inside of it; consider forall a. [a] vs [forall a. a]. That being said, the obvious change produces Illegal polymorphic or qualified type: ... GHC doesn't yet support impredicative polymorphism which I have no idea how to tackle, tbh. But then again, your MenuItemReference type seems a bit weird - a looks like a phantom type but I've no idea what it's supposed to do. — Bartek Banachewicz
This is a stripped down example just to show the problem. The MenuItemReference should be used to grab the correct item from other collections in my state. So MenuItemReference ListS Int will grab something from menuListItems, MenuItemReferences ActionS Int will grab something from menuActionItems and so on (menuListItems and menuActionItems are in MyState and they are Vectors of different data types) — ksaveljev
Oh... my... god... Thank you Bartek! I actually didn't see that (I mean duplication). You are correct, this is a useless duplication and the constructors themselves give enough information for me. Thank you very much for pointing that out! — ksaveljev
Yeah this isn't very straighforward, I backed out of that comment because I thought you meant something else. — Bartek Banachewicz

Bartek Banachewicz Bartek Banachewicz · Accepted Answer · 2015-11-16T11:45:49

Why not just

data MenuItemReference = 
    MenuListSReference Int | 
    MenuActionSReference Int | 
    MenuSliderSReference Int

then?

The constructor used already annotates the value. You don't need to inject the phantom type, because the information is already there.

Besides, doing so would require enabling GHC ({-# LANGUAGE ImpredicativeTypes #-}) to actually support impredicative polymorphism to construct Vector [forall a. MenuItemReference a Int] and use it polymorphically. While it does support that, the support has been described as "fragile at best and broken at worst".

As a side note this nice blog post explains how we can get rid of impredicative types, using newtypes and RankNTypes instead. This does require you to introduce a layer of newtype, however.

Vector containing GADT

1 Answers