On Fri 08 May, Victor M. Gulias wrote:
> 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?
I'm not sure if this is related to to my original question about typing
of successful pattern matches. Expecting a type checker to allow sub-
expressions which are badly typed (even if the result of evaluating
that expression would be ok type wise) seems to be asking too much.
Couldn't allowing this sort of thing also make some possible program
transformations fail at run-time? I think I'm getting way out of my depth
here (I haven't a clue what a 'heterogeneous type' is), so I'll say no more
about your idea, other than it seems to require a pretty radical new type
system which is probably beyond my comprehension :-)
My original point (that a variable which is bound to a particular pattern
should be typed the same way as the corresponding expression when the
variable is used in expressions) seems to me to be entirely consistent
with the current Haskell type system and doesn't require any new theory
about typing. Only the type checker needs to be modified to accomodate
this.
Regards
--
Adrian Hey
