[Haskell-cafe] Expressing "self-composable" functions at the type level

[Ignas Vyšniauskas]

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