Come inferire manualmente il tipo di '(.). (.). (.) '?

Question

Nel discorso di Edward Kmett Lenses, Folds, and Traversals, sullo scivolo "Il potere è nella Dot", egli mostra il tipo di (.) . (.) . (.) è

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

posso vedere, mostrando il suo tipo in GHCI. Ma mi piacerebbe anche sapere perché. L'altra cosa che vorrei capire è il motivo per cui c'è il modello nel cambiamento regolare dei parametri da (.) a (.) . (.) e (.) . (.) . (.):

(.)    :: (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. Ho provato a risolvere me stesso (.) . (.) espandendo la definizione di funzione di (.) . (.). Dopo aver applicato la definizione di (.) ho ottenuto:

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

Così ho dedotto i tipi:

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

Tuttavia mi sono perso il (.) . (.) . (.). E non so se questo è il modo giusto per fare inferenza di tipo manuale.

Answer 1

Con le funzioni,

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 = (.) 

così quello che in realtà hai è 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)) 

quali è

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

Perché fmap . fmap :: (a -> b) -> f (g a) -> f (g b)? Perché,

(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) 
-} 

La derivazione del tipo meccanico riguarda la sostituzione e la costante ridenominazione delle variabili di tipo. Vedi di più ad es. here o here.

Answer 2

(.) . (.) . (.) riduce in due fasi: in primo luogo ridurre puntini senza parentesi intorno:

((.) . (.) . (.)) f = (.) ((.) ((.) f)) 
        = (.) ((.) (f .)) 
        = (.) ((f .) .) 
        = ((f .) .) .) 

ridurre secondo il restante espressione

((f .) .) .) g = ((f .) .) . g 
       = \x -> ((f .) .) (g x) 
       = \x -> (f .) . g x 
       = \x y -> (f .) (g x y) 
       = \x y -> f . g x y 
       = \x y z -> f (g x y z) 

Quindi, prima di comporre n puntini tra parentesi usando n - 1 punti. Quindi applica questa costruzione alle funzioni f :: a -> b e g e ottieni (...((f .) .) ... .) g dove ogni punto corrisponde a un argomento ricevuto da g - ecco perché c'è un motivo: ogni punto tra parentesi gestisce un argomento di g e hai bisogno di un altro punto per comporre questo punto con tutto precedente. Dopo tutte le riduzioni l'espressione diventa

\x1 x2 ... xn -> f (g x1 x2 ... xn) 

e il suo tipo è ovvio.

---

Una cosa bella è che se avremmo operatori in forma suffissa potremmo scrivere (il codice è in Agda)

open import Function renaming (_∘′_ to _∘_) using() 

_% = _∘_ 

postulate 
    a b c d e : Set 
    f : a -> b 
    g : c -> d -> e -> a 

fg : c -> d -> e -> b 
fg = f % % ∘ g 

invece di ((f .) .) . g.