Type question re: map
Given the following (usual) definition of "map": map :: (a -> b) -> [a] -> [b] map f [] = [] map f (x : xs) = f x : map f xs What's the type of "map map"? GHCi's :t command reveals: *Main> :t map map map map :: [a -> b] -> [[a] -> [b]] I'd be grateful if anyone could provide a systematic type calculation so that I can reason through more complicated examples myself. Thanks. _________________________________________________________________ Windows Live™: Life without walls. http://windowslive.com/explore?ocid=TXT_TAGLM_WL_allup_1a_explore_032009
2009/3/6 R J
Given the following (usual) definition of "map":
map :: (a -> b) -> [a] -> [b]
What's the type of "map map"?
The definition is irrelevant, so I removed it. To make it easier to reason about, I'm going to rename the second map to map'. It means the same thing, but this is just so we can talk about each "instance" of it clearly. Now I'm going to rename the free variables: map :: (a -> b) -> [a] -> [b] map' :: (c -> d) -> [c] -> [d] -> is right-associative, so I'll add the implied parentheses: map :: (a -> b) -> ([a] -> [b]) map' :: (c -> d) -> ([c] -> [d]) Whenever we have an application like f x, if f has type a -> b and x has type a, then f x has type b. So map map' says that (a -> b) should be unified with the type of map', and then the type of the result will be ([a] -> [b]). So the equation is: a -> b = (c -> d) -> ([c] -> [d]) Which implies a = c -> d b = [c] -> [d] That's as far as we can go with the unification, so the result will be [a] -> [b]. Substituting, we have [c -> d] -> [[c] -> [d]]. Does that help? What I have done is more-or-less the Hindley-Milner type inference algorithm. Luke
map :: (a -> b) -> [a] -> [b]
map takes a function and transforms a list of a's to b's.
map succ [1,2,3]
==> [succ 1, succ 2, succ 3]
==> [2, 3, 4]
In general,
map f :: [a] -> [b]
where a is domain-type of f and b is image-type of f (f :: a -> b).
map map [x, y, z]
==> [map x, map y, map z]
so, x,y,z should functions of type (a -> b).
and the result list, [map x, map y, map z], should have type [([a] -> [b])]
because
map x :: [a] -> [b] where x :: a -> b
On 3/6/09, R J
Given the following (usual) definition of "map":
map :: (a -> b) -> [a] -> [b] map f [] = [] map f (x : xs) = f x : map f xs
What's the type of "map map"?
GHCi's :t command reveals:
*Main> :t map map map map :: [a -> b] -> [[a] -> [b]]
I'd be grateful if anyone could provide a systematic type calculation so that I can reason through more complicated examples myself.
Thanks.
_________________________________________________________________ Windows Live™: Life without walls. http://windowslive.com/explore?ocid=TXT_TAGLM_WL_allup_1a_explore_032009
participants (3)
-
Luke Palmer -
R J -
sam lee