Is Haskell's type system Curry-style or Church-style?
While researching Haskell's type system, I came across the terms Curry-style and Church-style. I would like to understand the differences between them.
- Curry-style is a system where type information is external to the program, and type checking is not mandatory for executing the program. The compiler automatically infers types without needing explicit type annotations.
- Church-style is a system where types are integrated into the language's semantics. Type annotations are mandatory, and type inference is also performed.
Given that Haskell's type system includes type inference and type annotations are not mandatory, I initially thought it to be classified as Curry-style. However, some literature suggests it also has characteristics of Church-style.
Should Haskell's type system be considered Curry-style or Church-style? Additionally, could you please explain the reasons for your opinion?
Haskell's type system is Haskell-style. It turns out that there just are more than two possibilities!
Broadly speaking, I tend to interact with it as if it were a curry-style system. But there are a few notable differences:
- In many cases, all of the type information about the program needed can be inferred. But there are a variety of situations where type annotations are required to guide the inference engine; examples include polymorphic recursion, ambiguous type class usage, higher-rank types, type family shenanigans, and GADTs.
- Type checking is mandatory for executing the program in most situations. Part of evaluating a program involves choosing type class instances, which cannot reliably be done without type checking.
- There are many reasons to attach type declarations to top-level definitions, so almost everybody does this, even for types whose inferred type would be the same as the declared type.