Haskell类型系统应归为Curry式还是Church式？

首先明确Curry式和Church式类型系统的核心区别：

• Curry式：类型属于程序的外部元信息，和代码核心语法完全分离。程序可不带任何类型注解运行，类型检查是可选操作，类型推导完全基于无类型的代码项。
• Church式：类型是语言语法和语义的一部分，代码项本身需要携带类型信息（或必须显式注解），类型检查是程序合法性的必要环节，无类型的代码可能不被视为合法程序。

回到你的问题：Haskell确实有很多Curry式的表现——比如支持全局类型推导，绝大多数日常代码不需要写显式类型注解，写代码时可以先实现逻辑再让编译器补全类型。但它本质上更偏向Church式，理由如下：

1. 核心语义基于带类型的λ演算：Haskell的类型系统根源是System Fω（带类型的高阶多态λ演算），而Curry式系统通常对应无类型λ演算的类型指派。这意味着Haskell的底层语义依赖类型信息，并非先有无类型代码再附加类型。
2. 类型是语法的必要部分：某些场景下必须写显式类型注解才能让程序合法，比如高阶多态（Rank-N Types）、存在类型，或者当类型类实例存在歧义时。这些不是"可选优化"，是语言语义的硬性要求。
3. 类型直接影响程序行为：比如类型类的约束、forall量化的类型，这些都是代码语义的一部分，而非单纯的元信息。例如forall a. a -> a和Int -> Int在Haskell中是完全不同的类型，会直接影响多态函数的使用方式。

结论：Haskell不是纯粹的Curry式或Church式，它结合了Curry式的便利性（自动推导、可选注解）和Church式的核心特征（类型融入语义、基于带类型的λ演算）。但从底层语义和类型在语言中的核心地位来看，更接近Church式类型系统。

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