Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

How to manually infer the type of '(.) . (.) . (.)'?

In Edward Kmett's talk Lenses, Folds, and Traversals, on the slide "The Power is in the Dot", he shows the type of (.) . (.) . (.) is

(a -> b) -> (c -> d -> e -> a) -> c -> d -> e -> b

I can see it by showing its type in GHCI. But I'd also like to know why. The other thing I'd like to understand is why there's the pattern in the regular change of parameters from (.) to (.) . (.) and (.) . (.) . (.):

(.)             :: (a -> b) -> (c ->           a) -> c ->           b
(.) . (.)       :: (a -> b) -> (c -> d ->      a) -> c -> d ->      b
(.) . (.) . (.) :: (a -> b) -> (c -> d -> e -> a) -> c -> d -> e -> b

P.S. I tried to resolve (.) . (.) myself by expanding the function definition of (.) . (.). After applying the definition of (.) I got:

\x y z t -> x ((y z) t)

So I inferred the types:

x :: a -> b
y :: c -> d -> a
z :: c
t :: d

However I got lost on (.) . (.) . (.). And I don't know if this is the right way to do manual type inference.

like image 938
Xiaogang Liu Avatar asked Jan 10 '16 01:01

Xiaogang Liu


1 Answers

With functions,

instance Functor ((->) r) where
   -- fmap :: (a -> b) ->   f   a  ->   f   b
   --         (a -> b) -> (r -> a) -> (r -> b)
   fmap          p           q         x = p (q x)   -- fmap = (.)

so what you actually have is fmap . fmap . fmap:

fmap               :: (a -> b) -> f       a   -> f       b
fmap . fmap        :: (a -> b) -> f (g    a)  -> f (g    b)
fmap . fmap . fmap :: (a -> b) -> f (g (h a)) -> f (g (h b))

which is

 (a -> b) -> (c -> (d -> (e -> a))) -> (c -> (d -> (e -> b)))   ~
 (a -> b) -> (c ->  d ->  e -> a)   -> (c ->  d ->  e -> b)     

Why is fmap . fmap :: (a -> b) -> f (g a) -> f (g b)? Because,

(fmap . fmap) foo = fmap (fmap foo)
{-
fmap            :: (a  ->  b) -> f a     -> f b
foo             ::  a  ->  b
fmap foo        ::               f a     -> f b
fmap foo        :: g a -> g b
fmap (fmap foo) ::               f (g a) -> f (g b)
-}

Mechanical type derivation is all about substitution and consistent renaming of type variables. See more e.g. here or here.

like image 99
Will Ness Avatar answered Oct 10 '22 08:10

Will Ness