如何从具有函数依赖项的类型类中获取和使用依赖项类型? [英] How do you get and use the dependent type from a type class with functional dependencies?

问题描述

如何从具有功能依赖项的类型类中获取和使用依赖项类型?

How do you get and use the dependent type from a type class with functional dependencies?

澄清并举例说明我的最新尝试(与我编写的实际代码相比有所减少):

To clarify and give an example of my latest attempt (minimised from actual code I was writing):

class Identifiable a b | a -> b where  -- if you know a, you know b
    idOf :: a -> b

instance Identifiable Int Int where
    idOf a = a

f :: Identifiable Int b => Int -> [b]  -- Does ghc infer b from the functional dependency used in Identifiable, and the instance?
f a = [5 :: Int]

但是ghc似乎无法推断b，因为它会显示此错误:

But ghc does not infer b, it seems, as it prints this error:

Couldn't match expected type ‘b’ with actual type ‘Int’
  ‘b’ is a rigid type variable bound by
      the type signature for f :: Identifiable Int b => Int -> [b]
      at src/main.hs:57:6
Relevant bindings include
  f :: Int -> [b] (bound at src/main.hs:58:1)
In the expression: 5 :: Int
In the expression: [5 :: Int]
In an equation for ‘f’: f a = [5 :: Int]

对于上下文，这是一个最小化的示例:

For context, here's a less minimised example:

data Graph a where
    Graph :: (Identifiable a b) => GraphImpl b -> Graph a

getImpl :: Identifiable a b => Graph a -> GraphImpl b
getImpl (Graph impl) = impl

此处的解决方法是将b作为arg类型添加到Graph:

The workaround here would be to add b as type arg to Graph:

data Graph a b | a -> b where
    Graph :: (Identifiable a b) => GraphImpl b -> Graph a

完整上下文:我有一个Graph实体，每个实体都有一个ID，每个实体分配给1个节点.您可以按实体查找节点.我还有一个Graph'，它由节点组成(可以分配一个实体)，要查找节点，您需要提供节点的ID(即Int). Graph在内部使用Graph'.我有一个IdMap，它将实体的ID映射到Graph'中的节点的ID.这是我的Graph定义:

The full context: I have a Graph of entities that each have an id, each entity is assigned to 1 node. You can look up a node by entity. I also have a Graph'which consists of nodes (which can be assigned an entity), and to lookup a node you need to provide the node's id, which is an Int. Graph uses Graph' internally. I have an IdMap which maps ids of entities to ids of nodes in Graph'. This is my Graph definition:

data Graph a where
    Graph  :: (Identifiable a b) => {
    _idMap :: IdMap b,
    _nextVertexId :: Int,
    _graph :: Graph' a
} -> Graph a

---

答案:使用类型族，请参见 Daniel Wagner的答案. 有关完整的故事，请参见里德·巴顿的答案.

---

Answer: Use type families, see Daniel Wagner's answer. For the full story, see Reid Barton's answer.

推荐答案

GHC抱怨您在最顶部发布的最小f确实有点奇怪.但这对于类型家族似乎还可以:

It does indeed seem a bit odd that GHC complains about the minimal f you posted at the very top. But it seems to work okay with type families:

{-# LANGUAGE TypeFamilies #-}
class Identifiable a where
    type IdOf a
    idOf :: a -> IdOf a

instance Identifiable Int where
    type IdOf Int = Int
    idOf a = a

f :: a -> [IdOf Int]
f _ = [5 :: Int]

也许您可以将此想法改编为更大的示例.

Perhaps you can adapt this idea to your larger example.

这篇关于如何从具有函数依赖项的类型类中获取和使用依赖项类型?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！