Sto giocando con type-aligned sequences, e in particolare sto scherzando con l'idea di piegarli. Una sequenza di tipo allineato pieghevole simile a questa:Come posso esprimere foldr in termini di foldMap per le sequenze allineate al testo?
class FoldableTA fm where
foldMapTA :: Category h =>
(forall b c . a b c -> h b c) ->
fm a b d -> h b d
foldrTA :: (forall b c d . a c d -> h b c -> h b d) ->
h p q -> fm a q r -> h p r
foldlTA :: ...
E 'abbastanza facile da implementare foldrTA
in termini di foldMapTA
dal primo utilizzo foldMapTA
per convertire la sequenza a un elenco di tipo allineato in modo ingenuo (vale a dire, usando la categoria dell'elenco allineato al tipo) e quindi piegare su quell'elenco. Sfortunatamente, questo può essere abbastanza inefficiente perché le liste lunghe possono essere anteposte a quelle brevi. Ho cercato di capire un modo per utilizzare un trucco simile a quello utilizzato in Data.Foldable
per definire le pieghe destra e sinistra in modo più efficiente, ma i tipi mi stanno facendo girare la testa. Endo
non sembra abbastanza generale per fare il trucco, e ogni passo che passo in altre direzioni mi porta a più variabili di tipo di quante ne possa tenere traccia.
In effetti, sono abbastanza sicuro che tutto ciò che termina e ha il tipo giusto è garantito dalla parametrricità per essere corretta. Molte grazie! – dfeuer