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

[Tillmann Rendel]

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> <term" 
we already have in Haskell.

Now, the type of (:) is (forall a . a -> [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