[Haskell-cafe] Re: Overloading functions based on arguments?
Tillmann Rendel
rendel at cs.au.dk
Sat Feb 14 12:37:00 EST 2009
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
More information about the Haskell-Cafe
mailing list