Manually deriving the type of fun xss = \f -> let ope x y = x . f . y in foldr1 ope xss

Question

I'm trying to manually derive the type of fun xss = \f -> let ope x y = x . f . y in foldr1 ope xss

f . y

y :: t1 -- First occurrence
f :: t2 -- First occurrence

(.) (b1 -> c1) -> (a1 -> b1) -> a1 -> c1 -- (.) definition

t1 ~ a1 -> b1 -- y unified with (a1 -> b1)
t2 ~ b1 -> c1 -- y unified with (b1 -> c1)

y :: a1 -> b1
f :: b1 -> c1
---
f . y :: a1 -> c1 -- Cancellation rule

\f -> let ope x y = x . f . y

(.) (b2 -> c2) -> (a2 -> b2) -> a2 -> c2 -- (.) definition

x :: t3 -- First occurrence

t3 ~ b2 -> c2 -- x unified with (b2 -> c2)
a1 -> c1 ~ a2 -> b2 -- f . y unified with (a2 -> b2)

a1 ~ a2
c1 ~ b2

y :: a2 -> b1 -- Substituing a1 by a2
f :: b1 -> b2 -- Substituing c1 by b2
x :: b2 -> c2 -- Substituing t3 by b2 -> c2
---
x . f . y :: a2 -> c2 -- Cancellation rule
(\f -> let ope x y :: x . f . y) 
          :: (b2 -> c2) -> (a2 -> b1) -> (b1 -> b2) -> a2 -> c2 -- Adding f

foldr1 ope xss

foldr1 :: (a -> a -> a) -> [a] -> a -- foldr1 definition

xss ~ t4 -- First occurrence

Then a ~ (b2 -> c2), a ~ (a2 -> b1), a ~ (b1 -> b2) and t4 ~ [a] which seems to be an error.

Any help?

Thanks,
Sebastián.

Answer 1

To start with the function

fun xss = \f -> let ope x y = x . f . y in foldr1 ope xss

I'll rewrite this as

fun xss f = foldr1 ope xss
    where ope x y = x . f . y

So we start with foldr1:

foldr1 :: (a -> a -> a) -> [a] -> a

So we can break down

foldrl1
    ope    -- (a -> a -> a)
    xss    -- [a]

So ope :: a -> a -> a, this is really useful to know since it simplifies the types of x and y to be restricted entirely to a, or put another way they both have the same type. Since they're both functions (as required by .), instead of unifying their types the long way I'll just say that x, y :: b -> c

ope x y =    x     .    f     .    y
--        (b -> c) . (s -> t) . (b -> c)

I've left f's type as unknowns right now, other than specifying that it has to be a function. Since we know that x and y have the same type, we can now say that y's output type is the same as f's input type, so s ~ c, and f's output type has to be the same as x's input type, so t ~ b, so we get

ope x y =    x     .    f     .    y
--        (b -> c) . (c -> b) . (b -> c)

So now we can fill fun's signature. We already know the type of xss, it's a ~ b -> c, and since foldr1's output type is also a, we get

 fun :: [b -> c] -> (c -> b) -> (b -> c)

And indeed this is the type that GHCi gives us