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

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 

完整的上下文：我有各自具有一个id实体的Graph，每个实体被分配到1个节点。您可以按实体查找节点。我也有一个Graph'，它由节点（可以分配一个实体）和查找节点，你需要提供节点的id，这是一个Int。 Graph内部使用Graph'。我有一个IdMap，它将实体的ID映射到Graph'中的节点的ID。这是我的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 Wagner的答案。

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]