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

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

为了澄清并给出我最近的尝试的一个例子（从我正在编写的实际代码中最小化）：

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 添加到 Graph 中：

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

完整的上下文：我有一个Graph每个实体都有一个 id，每个实体分配给 1 个节点。您可以按实体查找节点。我也有一个Graph'它由节点（可以分配一个实体）组成，要查找节点，您需要提供节点的 id，它是一个 Int。Graph uses Graph'内部。我有一个IdMap它将实体的 id 映射到节点的 idGraph'。这是我的Graph定义：

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

Answer：使用类型系列，请参见丹尼尔·瓦格纳的回答 https://stackoverflow.com/a/30536116/1031434。 完整故事请参见里德·巴顿的回答 https://stackoverflow.com/a/30537079/1031434.

在 GHC 的实现中，函数依赖可以约束类型变量的值，否则这些变量将是不明确的（在show . read感觉）。它们不能像等式约束那样用来提供两种类型相等的证据。我的理解是，函数依赖早于向 GHC 的中间 Core 语言添加强制转换，并且通常需要这些强制转换，以便将您期望使用的程序类型转换为类型良好的 Core 程序。

（这种情况可以说是最好的，因为 GHC 并没有真正在全局范围内强制执行函数依赖条件，并且如果像您的第一个程序那样的程序被接受，那么很容易破坏类型安全。另一方面，GHC 也可以做得更好强制实例的全局一致性。）

简而言之，类型检查器围绕函数依赖关系的逻辑并不像您想象的那么强大，尤其是与 GADT 等较新的类型系统功能结合使用时。我建议在这些情况下使用类型族，如 Daniel Wagner 的回答所示。

https://ghc.haskell.org/trac/ghc/ticket/345 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]