部分类型的家庭申请

Question

T 的递归定义未能通过类型检查。

class C a where
  type T a :: Type

newtype Compose (f :: Type -> Type) (g :: Type -> Type) (a :: Type) = Compose {getCompose :: f (g a)}

instance C (Maybe a) where
  type T (Maybe a) = NP (Compose T Identity) '[a]

具体错误：

    • The associated type family ‘T’ should have 1 argument, but has been given none
    • In the type instance declaration for ‘T’
      In the instance declaration for ‘C (Maybe a)’
   |
32 |   type T (Maybe a) = NP (Compose T Identity) '[a]
   |        ^

为什么 GHC 不能这样做？
有解决办法吗？

真实的class/instance长这样：

instance Ema (MultiSite models) where
  type RouteFor (MultiSite models) = NP (Compose RouteFor Site) models

这表示“多站点的路由是单个站点路由的 n 元乘积”，因此 RouteFor 必须递归定义。

Answer 1

类型族无法匹配，必须完全饱和。这意味着它们不能作为参数部分应用。这基本上就是错误消息所说的

• The associated type family ‘T’ should have 1 argument, but has been given none

目前，这在种类级别上没有区别（参见 Unsaturated type families 提案），但在 GHC 中有非常明显的区别。

根据 :kind T 和 Identity 具有相同的种类，而实际上 Identity 是 M 可匹配且T 是 Unmatchable:

Identity :: Type -> @M Type
T        :: Type -> @U Type

因为 Compose 的参数是 Type -> @M Type 你不能传递一个不匹配的类型族。类型语言是第一位的！ (Higher-Order Type-Level Programming in Haskell) 并且目前无法定义接受无法匹配的函数的 Compose。

如果比较稍微修改的T1和T2的种类，第一个在两个参数上都是不匹配的，而第二个在第二个参数上是匹配的

type  C1 :: Type -> @M Constraint
class C1 a where
  --   T1 :: Type -> @U Type -> @U Type
  type T1 a (b :: Type) :: Type

type  C2 :: Type -> @M Contraint
class C2 a where
  --   T2 :: Type -> @U Type -> @M Type
  type T2 a :: Type -> Type

一种可能性是将其包装在（可匹配的）新类型中

type    Wrapp'T :: Type -> @M Type
newtype Wrapp'T a = Wrapp'd (T a)

instance C (Maybe a) where
  type T (Maybe a) = NP (Compose Wrapp'T Identity) '[a]

部分类型的家庭申请

Partial type family application

haskell

ghc

type-families