为何类型族/同义词不可部分应用？已有规避方案的情况下

问题场景复现 #

首先定义一个类似map的类型族：

type Map :: (k1 -> k2) -> [k1] -> [k2] 
type family Map f l where
  Map _ '[] = '[]
  Map f (x : xs) = f x : Map f xs

接着定义一个类型同义词：

type MkPair a = (a, a)

尝试将这个同义词作为参数传入Map时会报错——类型同义词无法部分应用：

-- 编译失败：无法部分应用类型同义词 MkPair
type Blah = Map MkPair [Int, Char]

迂回实现方案 #

可以通过封装成数据类型+类型族的方式规避限制，实现相同需求：

type Mapper :: k1 -> k2 -> Type
data Mapper k1 k2 where
  Mapper :: Type -> Mapper k1 k2

type MapF :: Mapper k1 k2 -> [k1] -> [k2] 
type family MapF f l where
  MapF _ '[] = '[]
  MapF ft (x : xs) = MapFT ft x : MapF ft xs

type MapFT :: Mapper k1 k2 -> k1 -> k2
type family MapFT kt k1 

-- 定义具体的映射标识
data MkPair

-- 为MkPair实现映射逻辑
type instance MapFT ('Mapper MkPair :: Mapper Type Type) a = (a, a)

-- 现在可以正常使用
type Blah = MapF ('Mapper MkPair :: Mapper Type Type) [Int, Char]

-- 编译验证通过
f :: Proxy Blah -> Proxy '[(Int, Int), (Char, Char)]
f = id 

甚至可以扩展到其他类型映射场景：

data SymMap

type instance MapFT ('Mapper SymMap :: Mapper Symbol Type) a = Proxy a

g :: Proxy (MapF ('Mapper SymMap :: Mapper Symbol Type) ["hello", "world"]) -> Proxy '[Proxy "hello", Proxy "world"]
g = id 

这种转换是机械可行的，且暂未发现适用边界。由此产生疑问：既然可以通过类型族绕开限制，那Haskell最初禁止类型同义词（以及类型族）部分应用的设计初衷是什么？

解答 #

Haskell禁止类型同义词部分应用，核心原因在于类型同义词的本质是“宏替换”而非一等公民：

• 类型同义词是纯语法层面的别名，在类型检查阶段会被直接展开替换，本身不具备独立的类型身份。如果允许部分应用，会导致类型检查的复杂度爆炸——比如需要跟踪未完全展开的同义词，处理潜在的递归、歧义展开等问题，破坏类型系统的简洁性和可预测性。
• 早期Haskell的类型系统设计更侧重确定性和可判定性：部分应用的同义词会引入“延迟展开”的需求，这会让类型相等性检查变得更复杂，甚至可能引入不可判定的情况，违背了Haskell类型系统设计时追求的强规范性。

而用数据类型+类型族的方式规避限制，本质是把“部分应用的同义词”转换成了一等的类型级值：数据构造器Mapper MkPair是一个具体的类型级实体，MapFT则是基于这个实体的模式匹配，这完全符合Haskell类型系统对一等类型构造器的处理规则——类型族本身是支持模式匹配和实例化的一等类型构造器，和同义词的“宏替换”本质完全不同。

另外，这种转换的繁琐性也恰恰体现了设计意图：Haskell不鼓励用同义词模拟一等类型函数，而是引导用户使用更规范的类型族、数据类型来实现类型级计算，保持类型系统的清晰分层。

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