Понимание типа подписи gfoldl от Data.Data.Data

Question

Data определяет в качестве одного из своих основных функций gfoldl:

gfoldl 
    :: (Data a) 
    => (forall d b. Data d => c (d -> b) -> d -> c b) 
    -> (forall g. g -> c g) 
    -> a 
    -> c a 

Что цель c и c (d -> b) в нем? Почему это не просто очередной раз, что-то вроде

gfoldl' 
    :: (Data a) 
    => (forall d. Data d => r -> d -> r) 
    -> r 
    -> a 
    -> r 

Answer 1

Идея заключается в том, что значение алгебраического типа данных в Haskell имеет вид

C x_1 x_2 ... x_n 

где C является конструктором и x_i являются аргументы. Что

gfoldl app con 

делает, чтобы превратить такое значение в

con C `app` x_1 `app` x_2 ... `app` x_n 

тем самым превращая a в c a. Давайте предположим, что тип C является

C :: T_1 -> T_2 -> ... -> T_n -> D 

тогда давайте рассмотрим типы промежуточных выражений:

con C         :: c (T_1 -> T_2 -> ... -> T_n -> D) 
con C `app` x_1       :: c (T_2 -> ... -> T_n -> D) 
con C `app` x_1 `app` x_2    :: c (... -> T_n -> D) 
con C `app` x_1 `app` x_2 ... `app` x_n :: c D 

Параметрирование через c позволяет все эти промежуточные типы быть различны. Если бы мы использовали простую складку, такую ​​как gfoldl', тогда все эти промежуточные типы должны были бы быть одинаковыми.

Мотивация gfoldl это быть одного обобщения, которое позволяет выразить функции НСБА gmapQ и gmapT (и некоторые другие). Типы gmapQ и gmapT являются:

gmapQ :: Data a => (forall d. Data d => d -> u) -> a -> [u] 
gmapT :: Data a => (forall b. Data b => b -> b) -> a -> a 

Хотя gmapQ разрушается в a в единый список u с и может быть выражены с помощью gfoldl', это не было бы возможным gmapT.

Однако, с gfoldl, мы можем использовать c = Identity, чтобы мы могли получить что-то вроде gmapT и c = Const, чтобы получить что-то вроде gmapQ.

Для получения более подробной информации, вы также можете посмотреть на бумаге Scrap your boilerplate Reloaded, который показывает, что gfoldl обыкновенный (еще высший порядок) складка из типа данных, который называется Spine в этой работе.

Использование идентичности и постоянных функторы, чтобы получить как преобразование и поведения обновления от одного базового представления имеют некоторое сходство с , как вы получите операции линзы из линз «Ван Laarhoven».