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

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添加到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映射到节点的id Graph'.这是我的Graph定义:

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

---

答:使用类型系列,请参阅Daniel Wagner的回答.有关完整的故事,请参阅Reid Barton的回答.

Answer 1

在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]

Answer 2

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]

也许您可以将这个想法适应您的更大范例.