部分类型家族应用

Question

这个 的递归定义T无法进行类型检查。

\n

class C a where\n  type T a :: Type\n\nnewtype Compose (f :: Type -> Type) (g :: Type -> Type) (a :: Type) = Compose {getCompose :: f (g a)}\n\ninstance C (Maybe a) where\n  type T (Maybe a) = NP (Compose T Identity) \'[a]\n

\n

具体错误：

\n

    \xe2\x80\xa2 The associated type family \xe2\x80\x98T\xe2\x80\x99 should have 1 argument, but has been given none\n    \xe2\x80\xa2 In the type instance declaration for \xe2\x80\x98T\xe2\x80\x99\n      In the instance declaration for \xe2\x80\x98C (Maybe a)\xe2\x80\x99\n   |\n32 |   type T (Maybe a) = NP (Compose T Identity) \'[a]\n   |        ^\n

\n

\n
1. 为什么GHC无法做到这一点？
\n
2. 有解决方法吗？
\n

\n

真实的类/实例如下所示：

\n

    \xe2\x80\xa2 The associated type family \xe2\x80\x98T\xe2\x80\x99 should have 1 argument, but has been given none\n    \xe2\x80\xa2 In the type instance declaration for \xe2\x80\x98T\xe2\x80\x99\n      In the instance declaration for \xe2\x80\x98C (Maybe a)\xe2\x80\x99\n   |\n32 |   type T (Maybe a) = NP (Compose T Identity) \'[a]\n   |        ^\n

\n

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

\n

Answer 1

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

\n

\n

\xe2\x80\xa2 关联的类型族 \xe2\x80\x98 T\xe2\x80\x99 应有 1 个参数，但没有给出任何参数

\n

\n

目前，这在种类层面上没有区别（参见不饱和类型族提案），但 GHC 内有非常明显的区别。

\n

根据:kind两者T和Identity具有相同类型，而实际上Identity是可匹配的和T不可匹配的：

\n

Identity :: Type -> @M Type\nT        :: Type -> @U Type\n

\n

因为 的参数Compose是Type -> @M Type您不能传递不匹配的类型族。类型语言是一阶的！（Haskell 中的高阶类型级编程Compose）并且目前无法定义接受无法匹配的函数。

\n

T1如果比较稍微修改过的and的类型T2，第一个在两个参数中都是不匹配的，而第二个在第二个参数中是匹配的

\n

type  C1 :: Type -> @M Constraint\nclass C1 a where\n  --   T1 :: Type -> @U Type -> @U Type\n  type T1 a (b :: Type) :: Type\n\ntype  C2 :: Type -> @M Contraint\nclass C2 a where\n  --   T2 :: Type -> @U Type -> @M Type\n  type T2 a :: Type -> Type\n

\n

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

\n

type  C1 :: Type -> @M Constraint\nclass C1 a where\n  --   T1 :: Type -> @U Type -> @U Type\n  type T1 a (b :: Type) :: Type\n\ntype  C2 :: Type -> @M Contraint\nclass C2 a where\n  --   T2 :: Type -> @U Type -> @M Type\n  type T2 a :: Type -> Type\n

\n