Is Haskell's type system Curry-style or Church-style?

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.

The original sense of Church-style typing, applied to lambda calculus, did include explicit type annotations on binders. But nowadays, “Church-style” primarily refers to intrinsic typing, and that’s what Haskell has. Every term and variable has a single intrinsic type, and ill-typed code doesn’t have a defined meaning as a program.

Adding type inference doesn’t necessarily change the type system, it just reconstructs some of the type annotations for you.

Likewise, Curry-style typing now conventionally means extrinsic typing, where a program has a meaning independent of typechecking. A given term could have multiple valid types, none of which is the most general among them, and the choice of type doesn’t change the semantics. This is why it didn’t require type annotations in its original context of lambda calculus.

The Haskell Report defines the language assuming intrinsic types. Not only does it say when “a static error occurs”, but the semantics of certain language features such as pattern matching and typeclasses are defined in terms of intrinsic types.

GHC’s deferred type errors (-fdefer-type-errors) might appear to let you run a partially defined program. But if an expression has a type error, it still won’t produce a value, so this doesn’t change the nature of the types—it just replaces some untypeable parts of the code with well-typed terms like throw (TypeError "…") to make a well-typed program.