如何将类型族作为类型同义词的参数？Haskell类型编程问题

首先咱们拆解下你遇到的问题核心：
你定义的G要求第一个参数是一个类型构造器（kind为Nat -> Nat的类型级函数），但你用的Id是一个类型族——类型族本质是类型级函数，但它们不能直接作为高阶参数传递给需要类型构造器的位置，这就是编译器报错说Id需要1个参数却没被传入的原因。

最简单的解决方案：用类型同义词代替类型族 #

你完全不需要用类型族实现类型级恒等函数，直接定义一个多态的类型同义词就能完美匹配G的参数要求：

{-# LANGUAGE GADTs, TypeFamilies, DataKinds, TypeInType, PolyKinds #-}

-- 你的原始GADT定义
data G f n a where
  G :: a -> G f n a -> G f (f n) a

-- 多态恒等类型同义词，kind为 k -> k，可适配任意类型kind
type Id (a :: k) = a

-- 现在可以正常定义目标类型同义词了
type G'' n a = G Id n a

这个Id是真正的类型构造器，当传给G时，Haskell会自动将它的kind实例化为Nat -> Nat，完全符合G的要求。

为什么之前的类型族不行？ #

类型族type family Id a where Id a = a虽然语义上是恒等，但它是类型函数而非类型构造器。Haskell类型系统中，类型族不能直接作为高阶参数传递给需要类型构造器的位置——你必须显式传入它的参数，而G的第一个参数位置需要的是一个“待应用”的类型级函数（即类型构造器），所以编译器会判定你漏传了Id的参数，从而抛出错误。

关于Data.Functor.Identity的补充 #

你之前尝试的Identity之所以不适用，是因为它的kind是* -> *，只能作用于普通Haskell类型（比如Int、String），而G需要的是作用于Nat（由DataKinds提升后的类型级自然数）的函数，kind完全不匹配。而我们上面定义的Id是多态kind的，可以适配任意类型kind，包括Nat。

内容的提问来源于stack exchange，提问作者Eliza Brandt