On 11/10/2013 01:14 AM, Alexander Vieth wrote:
Due to polymorphism this is not quite the same as saying that the domain and co-domain match.
I believe it's the same as saying that the type of the co-domain can be refined to the type of the domain. Self-composability is already expressed at the type level, although it may not be immediately clear.
In the case of swap, it might seem like it's not possible because (b, a) can be refined to (a, b) only if a = b, but when we compose swap with itself we get fresh names for the type variables, and (b, a) can indeed be refined to (a1, b1). Trying to type (swap . swap) we find that the first swap has type (a, b) -> (b, a) and the second swap has type (a1, b1) -> (b1, a1) so if we set b = a1 and a = b1 then we recover the type (b1, a1) -> (b1, a1).
Hmm, you are right, I didn't quite think through the case of swap. Thanks! Another case would be to consider a function like: double :: a -> (a, a) double x = \x -> (x, x) then (double . double) is possible, but (I think) it's impossible to write a function for such compositions in general: e.g. Prelude> let involute = \f -> f . f Prelude> :t involute (\x -> (x, x)) <interactive>:1:18: Occurs check: cannot construct the infinite type: t0 = (t0, t1) I guess this is simply not type-able in System F? -- Ignas