如何从具有函数依赖关系的类型类中获取和使用依赖类型？

Question

如何从具有函数依赖关系的类型类中获取和使用依赖类型？

为了澄清并举例说明我最近的尝试(从我正在编写的实际代码中最小化)：

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，因为它打印了这个错误：

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]

对于上下文，下面是一个较少的示例：

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类型添加到图中：

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

完整的上下文:我有一个实体的Graph，每个实体都有一个id，每个实体被分配给一个节点。您可以逐个实体地查找节点。我还有一个Graph'，它由节点(可以分配实体)组成，为了查找节点，您需要提供节点的id ( Int )。Graph在内部使用Graph'。我有一个IdMap，它将实体的ids映射到Graph'中的节点ids。这是我的Graph定义：

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

答案：使用类型家族，参见Daniel Wagner's answer。有关整个故事，请参见Reid Barton's answer。

Answer 1

确实有点奇怪的是，GHC抱怨你在最上面发布的最小的f。但这似乎适用于类型的家庭：

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

也许你可以把这个想法改编成更大的例子。

Answer 2

在GHC的实现中，函数依赖项可以约束类型变量的值，否则这些变量将是不明确的(在show . read意义上)。它们不能以相等约束的方式提供两种类型相等的证据。我的理解是，在GHC的中间核心语言中添加矫顽力之前，函数依赖项是必需的，一般来说，为了将您期望工作的程序类型转换为类型良好的核心程序，这些矫顽器是必需的。

(这种情况可以说是最好的，因为GHC并没有真正在全局上强制执行功能依赖条件，而且如果您的第一个程序被接受，就很容易破坏类型安全。另一方面，GHC还可以更好地执行实例的全局一致性。)

简短的版本是，类型检查器围绕函数依赖项的逻辑不像您可能预期的那么强，特别是结合新的类型系统特性(如GADT)。我建议在这种情况下使用类型的家庭，例如Daniel的回答。

https://ghc.haskell.org/trac/ghc/ticket/345是一个类似主题的老票，因此您可以看到，这是一个长期存在的函数依赖问题，而使用类型族则是官方推荐的解决方案。

如果您想保留Identifiable有两个类型参数的样式，也可以以以下形式设置程序

type family IdOf a
class (b ~ IdOf a) => Identifiable a b where
    idOf :: a -> b

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

f :: Identifiable Int b => Int -> [b]
f a = [5 :: Int]