Как я могу выразить foldr в терминах foldMap для последовательностей, выровненных по типу?

Я играю с последовательностями, выровненными по типу, и в частности, я возился с идеей сложить их. Складная последовательность, выровненная по типу, выглядит примерно так:

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 :: ...

Довольно легко реализовать foldrTA в терминах foldMapTA, сначала используя foldMapTA для преобразования последовательности в список с выравниванием по типу наивным способом (т. е. используя категорию списка с выравниванием по типу), а затем свернув этот список. К сожалению, это может быть весьма неэффективно, потому что длинные списки могут быть добавлены перед короткими. Я пытался найти способ использовать трюк, подобный тому, что использовался в Data.Foldable, чтобы более эффективно определять правую и левую складки, но типы вызывают у меня головокружение. Endo не кажется достаточно общим, чтобы добиться цели, и каждый шаг, который я делаю в других направлениях, приводит меня к большему количеству переменных типа, чем я могу уследить.


person dfeuer    schedule 22.06.2015    source источник


Ответы (1)


Я обнаружил, что это 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)

Понятия не имею, имеет ли это какой-то смысл, но с таким количеством индексов типов я сомневаюсь, что есть много кода проверки типов, который не имеет смысла.

person Joachim Breitner    schedule 22.06.2015
comment
В самом деле, я почти уверен, что все, что завершается и имеет правильный тип, гарантируется параметризацией как правильное. Большое спасибо! - person dfeuer; 22.06.2015