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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
