能否从带有关联类型族的类实例中省略类型实例化？

你想把instance C Integer简化成不带类型族关联的形式完全可行，但得先给类里的类型族T a加上一个默认的关联类型，不然编译器没法自动推断T Integer应该是什么。

为什么原代码不能直接简化？ #

看你原来的类定义：

class C a where
  type T a = r | r -> a
  pred :: T a -> Bool
  default pred :: T a ~ [a] => T a -> Bool
  pred = not . null

这里只给pred提供了默认实现，且这个实现要求T a必须等于[a]，但没有给类型族T a指定默认的关联类型。所以如果实例里不显式写type T Integer = [Integer]，编译器根本不知道T Integer该对应什么类型，会直接报错。

调整后的完整代码 #

只需要给T a加一行默认的类型关联即可：

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE DefaultSignatures #-}
module Study where

class C a where
  type T a = r | r -> a
  -- 给类型族添加默认关联：默认T a就是[a]
  type T a = [a]
  pred :: T a -> Bool
  default pred :: T a ~ [a] => T a -> Bool
  pred = not . null

-- 现在可以直接写这个简化的实例了！
instance C Integer

测试效果和原来完全一致 #

运行起来和你原来的代码结果一样：

λ Study.pred [1,2,3]
True
λ Study.pred ([] :: [Integer])
False

额外说明 #

• 依赖类型族的r -> a约束确保了每个关联类型r只能对应唯一的a，比如[Integer]只能对应Integer，不会出现一个r对应多个a的歧义问题，这很重要。
• 如果之后要给其他类型写实例，且T a不是[a]，那还是需要显式指定T a的类型，并且得自己实现pred（因为默认pred的约束T a ~ [a]不满足了）。比如：

  instance C Bool where
    type T Bool = Maybe Bool
    pred (Just _) = True
    pred Nothing = False
  

内容的提问来源于stack exchange，提问作者Ignat Insarov