I'd like to constrain the key type to be ImageId and the value type to be Sprite while leaving the concrete type of the map unconstrained, by way of the At typeclass. Is this possible? I seem to get a kind mismatch and, based on the type signature, I don't see how to resolve it. My example:
data Game m e = Game {
initial :: e,
-- ...
sprites :: (At m) => IO (m ImageId Sprite)
}
My error:
* Expected kind `* -> * -> *', but `m' has kind `*'
* In the first argument of `IO', namely `(m ImageId Sprite)'
In the type `(At m) => IO (m ImageId Sprite)'
In the definition of data constructor `Game'
|
64 | sprites :: (At m) => IO (m ImageId Sprite)
| ^^^^^^^^^^^^^^^^
At m provides at :: Index m -> Lens' m (Maybe (IxValue m)). Notice that Lens' m _ means that m is a concrete type like Int or Map ImageId Sprite, not a type constructor like Map. If you want to say that m ImageId Sprite is "map-like", then you need these 3 constraints:
At (m ImageId Sprite): provides at for indexing and update.Index (m ImageId Sprite) ~ ImageId: the keys used to index m ImageId Sprites are ImageIds.IxValue (m ImageId Sprite) ~ Sprite: the values in a m ImageId Sprite are Sprites.You may try to put this constraint in Game (though it's still wrong):
data Game m e = Game {
initial :: e,
-- ...
sprites :: (At (m ImageId Sprite),
Index (m ImageId Sprite) ~ ImageId,
IxValue (m ImageId Sprite) ~ Sprite) =>
IO (m ImageId Sprite)
}
Note that I'm saying m ImageId Sprite a bazillion times, but I don't apply m to other (or fewer) parameters. That's a clue that you don't actually need to abstract over m :: * -> * -> * (the kind of things like Map). You only need to abstract over m :: *.
-- still wrong, though
type IsSpriteMap m = (At m, Index m ~ ImageId, IxValue m ~ Sprite)
data Game m e = Game {
initial :: e,
-- ...
sprites :: IsSpriteMap m => IO m
}
This is good: if you ever make a specialized map for this data structure, like
data SpriteMap
instance At SpriteMap
type instance Index SpriteMap = ImageId
type instance IxValue SpriteMap = IxValue
you would not be able to use it with the too-abstract Game, but it fits right into the less-abstract one as Game SpriteMap e.
This is still wrong, though, because the constraint is in the wrong place. What you've done here is say this: if you have a Game m e, you can get a m if you prove that m is mappish. If I want to create a Game m e, I have no obligation to prove that m is mappish at all. If you don't get why, imagine if you could replace the => with a -> above. The person who calls sprites is passing in a proof that m is like a map, but the Game doesn't contain a proof itself.
If you want to keep m as a parameter to Game, you should simply write:
data Game m e = Game {
initial :: e,
-- ...
sprites :: IO m
}
And write every function that needs to use m as a map like:
doSomething :: IsSpriteMap m => Game m e -> IO ()
Or, you can use existential quantification:
data Game e = forall m. IsSpriteMap m => Game {
initial :: e,
-- ...
sprites :: IO m
}
To construct a Game e, you can use anything of type IO m to fill sprites, as long as IsSpriteMap m. When you consume a Game e in a pattern match, the pattern match will bind a (unnamed) type variable (let's call it m), and then it'll give you a IO m and a proof for IsSpriteMap m.
doSomething :: Game e -> IO ()
doSomething Game{..} = do sprites' <- sprites
imageId <- _
let sprite = sprites'^.at imageId
_
You can also keep m as a parameter to Game but still keep the context in the Game constructor. However, I urge you to just go with the first option of putting a context on every function, unless you have a reason not to.
(All code in this answer produces errors about language extensions. Keep sticking them in a {-# LANGUAGE <exts> #-} pragma at the top of your file until GHC is placated.)