Let's try explicitly unifying the types in your map example. We'll assume that map already has the following explicit type: data List a = Nil | Cons a (List a) type Function a b = a -> b map :: Function (Function a b) (Function (List a) (List b)) I've defined new "List" and "Function" types since the "[]" and "->" may cause confusion. The "a" and "b" are placeholders; they give us *constraints* by telling us which types must be the same, but they don't tell us what those types actually are. These placeholders can be re-used in different type declarations, but I'll use different letters to prevent any confusion. Now let's look at the arguments given to map in your example. First the identity function, written like this in Haskell, with some unknown type: (\x -> x) :: ? The simple placeholder "?" is my way of saying 'we don't know yet'. In fact, we already know that the value is a function, so we can write that down: (\x -> x) :: Function ? ? Now we can calculate the output type by *assuming* that the input type holds. In other words, to calculate the type of the output value we need to assume that we've been given an input value. Here we will assume that we've been given a value of some type "c": x :: c Now we can calculate the type of the output expression: x :: ? Since we assumed that x :: c, we can immediately write down the type of the output, since it's the same: x :: c Hence we've found that the output type happens to be the same as the input type: (\x -> x) :: Function c c Now let's look at the other argument: (Cons 1 (Cons 2 (Cons 3 Nil))) :: ? This is [1,2,3] written using my List type. We know that Cons gives us a List, so we can write that down: (Cons 1 (Cons 2 (Cons 3 Nil))) :: List ? Now we need to know the types of "1", "2" and "3". Haskell treats numbers in a special way, using the "Num" typeclass, but that will just complicate things, so I'll pretend that they're Ints: (Cons 1 (Cons 2 (Cons 3 Nil))) :: List Int Notice that this type has no placeholders, it is 'concrete'. Now let's look at the full example: map (\x -> x) (Cons 1 (Cons 2 (Cons 3 Nil))) We can only apply a function to arguments of the correct type, which means that the following equations must be satisfied: Function a b = Function c c List a = List Int We can see that the 'top level' constraints are OK: we have a Function type equal to a Function type and a List type equal to a List type. Next we need to check their arguments (known as "type arguments"): a = c b = c a = Int This looks OK, since we don't have any nonsense like Int = Bool or anything. However, we still haven't worked out what the types actually are. It looks like this is where typed clojure gives up:
We take the simple approach that all the the arguments' types must be determined before calculation of any missing type arguments.
In Haskell we can go a bit further by rearranging these equations using substitution. We can see that the first and third equations both use "a", hence we can substitute one for the other: Int = c This uses "c" and so does the middle equation, so we can do another substitution: b = Int Now we have concrete types for all of our placeholders, specifically: a = Int b = Int c = Int Hence we can substitute these back into the type of our map expression: Function (Function Int Int) (Function (List Int) (List Int)) Or, with the conventional notation for types: (Int -> Int) -> [Int] -> [Int] The extra step of solving simultaneous equations to get the type arguments is the reason Haskell can infer this type and typed clojure cannot. Regards, Chris