2015-06-22 15 views
10

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.

risposta

7

ho scoperto che questo typechecks:

{-# LANGUAGE RankNTypes #-} 
module FoldableTA where 

import Control.Category 
import Prelude hiding (id, (.)) 

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 
    foldrTA f z t = appEndoTA (foldMapTA (\x -> TAEndo (f x)) t) z 

newtype TAEndo h c d = TAEndo { appEndoTA :: forall b. h b c -> h b d } 

instance Category (TAEndo h) where 
    id = TAEndo id 
    TAEndo f1 . TAEndo f2 = TAEndo (f1 . f2) 

idea se ha un senso, ma con tanti indici di tipo in tutto, dubito che c'è molto codice di tipo controllo che fa non ha senso .

+2

In effetti, sono abbastanza sicuro che tutto ciò che termina e ha il tipo giusto è garantito dalla parametrricità per essere corretta. Molte grazie! – dfeuer

Problemi correlati