Dérivation du type de (() foldr.)

Question

Je suis en train de tirer manuellement le type de (() foldr.)

(.) ::(b1 -> c1) -> (a1 -> b1) -> a1 -> c1 
foldr :: (a2 -> b2 -> b2) -> b2 -> [a2] -> b2 

Puis:

b1 = a2 -> b2 -> b2 
c1 = b2 -> [a2] -> b2 

correspondre les types que je reçois :

((a2 -> b2 -> b2) -> (b2 -> [a2] -> b2)) -> (a1 -> (a2 -> b2 -> b2)) -> a1 -> (b2 -> [a2] -> b2) 

Mais alors je suis confus sur la façon de réduire cette expression.

Une aide?

Thansks,
Sebastián.

Answer 1

Vous avez correctement compris le type de (.) dans (.) foldr. Le (.) est appliqué à un argument (la foldr) afin que vous puissiez jeter le ((a2 -> b2 -> b2) -> (b2 -> [a2] -> b2)) et ce qui reste est le type de (.) foldr:

(a1 -> a2 -> b2 -> b2) -> a1 -> (b2 -> [a2] -> b2) 

Assurez-vous que foldr peut avoir le type ((a2 -> b2 -> b2) -> (b2 -> [a2] -> b2)) avant de le jeter. Si vous avez le bon correspondant, cette vérification ne peut pas échouer, mais c'est un bon contrôle de santé mentale.

Answer 2

Si nous avons

(.) :: (b -> c) -> (a -> b) -> (a -> c) 
foldr :: (x -> y -> y) -> y -> [x] -> y 

Ensuite, pour (.) foldr, le b -> c doit aligner avec le type de foldr, si

b    -> c 
(x -> y -> y) -> (y -> [x] -> y) 

Ce qui implique

b ~ (x -> y -> y) 
c ~ (y -> [x] -> y) 

Donc, en remplaçant retour dans:

--     b      c 
(.) foldr :: (a -> (x -> y -> y)) -> (a -> (y -> [x] -> y)) 

Depuis -> est associative gauche, nous pouvons laisser tomber les parenthèses supplémentaires:

(.) foldr :: (a -> x -> y -> y) -> (a -> y -> [x] -> y) 

Et si vous voulez, vous pouvez aller plus loin avec

(.) foldr :: (a -> x -> y -> y) -> a -> y -> [x] -> y 

Donc, si nous demandons GHCi ce le type est, nous obtenons

> :t (.) foldr 
(.) foldr :: (a -> a1 -> b -> b) -> a -> b -> [a1] -> b 

Où a ~ a, a1 ~ x, et b ~ y, donc nous sommes arrivés à la bonne réponse.