如何手动推导表达式类型？替代GHCi :type命令的算法式方法

Great question! Manually deriving Haskell types is such a valuable skill—it forces you to really grok how the type system fits together. Let's break this down from basics to that gnarly (.) . (.) example, using a systematic, algorithmic approach that works for any expression.

For simple expressions, you can often work it out just by looking at the components and how they interact:

• Literals: Things like 42 have the type Num a => a (since it can be any numeric type), while "hello" is String (aka [Char]).
• Variables: Without a type signature, variables are polymorphic (like x :: a), but context narrows them down. For example, x + 5 tells you x must be Num a => a because + requires numeric operands.
• Simple function application: If you have f x, take the type of f (say a -> b) and the type of x (say a), then the result is b. For example, succ 5: succ is Enum a => a -> a, 5 is Num a => a, so the result is Num a => a (since types like Int are both Enum and Num).

The key to tackling tricky expressions like (.) . (.) is type unification—a process where you match up type variables and substitute them consistently. Let's walk through this step by step.

First, recall the type of the basic function combinator (.):

(.) :: (b -> c) -> (a -> b) -> a -> c

This reads: "take a function from b to c, a function from a to b, and return a function from a to c."

Now, (.) . (.) is equivalent to ((.) (.)) (.)—we're using the first (.) to combine the second (.) with the third (.). To avoid confusion, let's assign unique type variables to each instance of (.):

• Let the leftmost (.) be f1: f1 :: (b -> c) -> (a -> b) -> a -> c
• Let the middle (.) be f2: f2 :: (d -> e) -> (f -> d) -> f -> e (this is the first argument to f1)
• Let the rightmost (.) be f3: f3 :: (g -> h) -> (i -> g) -> i -> h (this is the second argument to f1)

Step 1: Match f2 to f1's first argument #

Since f2 is the first input to f1, its type must equal f1's first parameter type b -> c. That gives us two equations:

• b = (d -> e) (the input type of f1's first argument matches f2's overall type)
• c = (f -> d) -> f -> e (the output type of f1's first argument matches f2's return type)

Step 2: Match f3 to f1's second argument #

f3 is the second input to f1, so its type must equal f1's second parameter type a -> b. This gives us two more equations:

• a = (g -> h) (input type of f1's second argument matches f3's overall type)
• b = (i -> g) -> i -> h (output type of f1's second argument matches f3's return type)

Step 3: Unify conflicting definitions of b #

From Step 1, b = (d -> e); from Step 2, b = (i -> g) -> i -> h. These must be equal, so we split the function types into their components:

• d = (i -> g) (the input type of the left b equals the input type of the right b)
• e = i -> h (the return type of the left b equals the return type of the right b)

Step 4: Substitute all variables into f1's return type #

f1 returns a -> c. Let's substitute all our solved variables:

• a = (g -> h) (from Step 2)
• c = (f -> d) -> f -> e (from Step 1). Replace d with (i -> g) and e with i -> h:
  c = (f -> i -> g) -> f -> i -> h

Putting it all together, the final type is:

(.) . (.) :: (g -> h) -> (f -> i -> g) -> f -> i -> h

We can rename variables to make it more intuitive (since type variable names don't matter):

(.) . (.) :: (c -> d) -> (a -> b -> c) -> a -> b -> d

This makes sense—it lets you compose a unary function with a binary function, e.g., (show .: (+)) 3 4 (where .: = (.) . (.)) evaluates to show (3+4) = "7".

Here's a repeatable process for any Haskell expression:

1. Write down the type signature of every function/variable involved, using unique type variables for each to avoid confusion.
2. For each function application, set the type of the argument equal to the expected input type of the function.
3. Solve the resulting equations by substituting equivalent type variables (unification).
4. Simplify the final type by removing redundant parentheses and renaming variables for readability.

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