Re: [Haskell-cafe] Re: Overloading functions based on arguments?

John A. De Goes wrote:

Take, for example, this function:

f :: [Char] -> Char

f [] = chr 0 f (c:cs) = chr (ord c + ord (f cs))

[] is typed as [Char], even though it could be typed in infinitely many other ways. Demonstrating yet again, that the compiler *does* use the additional information that it gathers to assist with typing.

I'm not sure about this example, since [] occurs in a pattern here, and I don't know how typing affects patterns. However, you seem to believe that in the expression 'x' : [] the subexpression [] has type [Char]. That is not correct, though. This occurence and every occurence of [] has type (forall a . [a]). This becomes clearer if one uses a calculus wih explicit type abstraction and application, like ghc does in its Core language. In such a calculus, we have a uppercase lambda "/\ <type var> -> <term>" which binds type parameters, and a type application "<term> <type>" similar to the lowercase lambda "\ <var> -> <term>" and term application "<term> [a] -> [a]). Since this type contains one type variable, (:) has to applied to one type argument before it is used on term arguments. The same is true for [], which has type (forall a . [a]). That means that the expression above is equivalent to (:) Char 'x' ([] Char) In this expression it is clear that [] has type (forall a . [a]), while ([] Char) has type [Char]. The job of type inference is not to figure out the type of [], but to figure out that this occurence of [] in Haskell really means ([] Char) in a calculus with explicit type application. Tillmann