Haskell函数类型签名可实现性（inhabitation）验证问询

咱们先把核心问题拆解清楚：给定一个Haskell类型签名，怎么判断它有没有合法的总实现——也就是这个类型是不是inhabited（存在符合要求的非错误、非无限循环的函数值）。结合你提到的parametricity（参数多态性）和类型检查规则，咱们可以从这几个角度入手分析：

1. 从基础类型的可实现性入手 #

先从简单场景建立直觉：

• 像 Int -> Bool 这种带具体类型的签名，显然是可实现的，比如写个 const True 就行。
• 但完全多态的 a -> b 就不一样了——根据parametricity，你没办法凭空把任意类型a的转成任意类型b，除非用undefined这种“作弊”的错误值。如果只讨论总函数（不会出错、不会无限循环的函数），这个类型就是不可实现的。

2. 用Parametricity定理做核心判断 #

Parametricity的核心是：多态函数的行为必须对所有类型参数保持一致，不能依赖类型的具体结构。这是判断的关键工具：

• 比如 forall a. a -> a：唯一的总实现就是id，所以这个类型是inhabited的。
• 再比如 forall a b. (a -> b) -> [a] -> [b]：这就是map的类型，完全符合parametricity的要求——它只能对列表做元素级的转换，不能做任何依赖具体类型的操作，所以显然有合法实现。
• 反过来，forall a. a -> Int：你没办法从任意a得到一个确定的Int（总函数层面），所以这个类型是uninhabited的。

3. 类型多态性与子类型的关联 #

你提到的“推断类型的多态性至少不低于签名类型”，是Haskell类型检查的规则：如果函数实现的推断类型比签名更泛化（比如签名是Int -> Int，推断类型是forall a. a -> a），没问题；但如果签名更泛化（比如签名是forall a. a -> a，推断类型是Int -> Int），就会报错。

但回到验证签名可实现性的场景，咱们不需要关心具体实现的推断类型，而是要判断是否存在某个总函数，其类型是签名类型的子类型（或者说，签名类型能被这个函数的类型所满足）。

4. 进阶：借助Curry-Howard同构 #

更深层的逻辑可以用Curry-Howard同构来理解：Haskell的类型对应逻辑命题，函数实现对应命题的证明。所以判断类型是否inhabited，等价于判断对应的逻辑命题是不是重言式：

• a -> a 对应逻辑中的A → A，显然是重言式，对应实现就是id。
• a -> b 对应A → B，这不是重言式，所以没有合法的总实现（即没有对应的逻辑证明）。
• 再比如 (a -> b -> c) -> (a -> b) -> a -> c 对应(A→B→C) → (A→B) → A→C，这是重言式，对应的实现就是\f g x -> f x (g x)。

5. 工具辅助验证 #

如果不想手动推导，也可以用工具帮你判断：

• 用ghci的:type命令可以验证你写的实现是否符合签名，但要是想直接检查签名是否可实现，可以试试agda或idris这类依赖类型语言——它们的类型检查器能直接判断命题是否可证，间接对应Haskell类型是否inhabited。

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