I have found an example that seems to be related to this thread. The
map function behaves like this:
map f [a1,a2,...,an] = [f a1, f a2, ..., f an]
Suppose a function f defined as:
f :: Maybe a -> Int
f Nothing = 1
f _ = 0
the following expression is type checked successfully:
sum [f Nothing, f (Just True), f (Just "hi")]
it counts the number of "Nothing"s appearing in the list (1). Replacing the
above expression folding map, that is,
sum (map f [Nothing, Just True, Just "hi"])
or even defining sum_nothings = sum . map f,
sum_nothings [Nothing, Just True, Just "hi"]
obviously does not type check. However, the expression has the same meaning as
the one unfolding the map. Well, suppose that you actually *type* the list as
[Nothing, Just True, Just "hi"] :: [Maybe _]
where _ is a *who-knows* type (heterogeneous type?). Now, the expression can
be typed because f :: Maybe a -> Int does not need to know what polymorphic
"a" really is ("a" is a *who-cares* type). Or supposing [True, "hi"] :: [_]
sum (map f (map Just [True, "hi"]))
also would be ok. I can imagine some kind of typing rule somehow
__ __
| |- x :: A | |- xs :: [B]
------------------------------- A/=B \/ A=_ \/ B=_
__
| |- x:xs :: [_]
does it make any sense? is it related to other stuff like dynamic or
existential typing?
--
Victor M. Gulias
