Учитывая глубокое внедрение простой DSL обработки данных [1]:

мы можем реализовать знакомый синтез-производитель-потребитель так

Небольшой пример, показывающий, как это работает:

Там другой, гораздо менее известный [2], тип слияния, называемый sibling fusion, который удаляет множественные обходы одного и того же входа. Идея состоит в том, чтобы заменить что-то вроде

Если перемещение ys намного дешевле, чем перемещение xs (например, если xs является файлом в сети), или если мы можем, например, используйте слияние производителей-потребителей, чтобы позже сливать немаркировку с каким-либо другим обходом, это победа.

В то время как слияние производителей и потребителей легко реализуется с использованием нашего стандарта AST выше, я не вижу, как реализовать слияние с братом, используя это представление.

Проблема заключается в том, что, хотя мы можем легко выявить возможности слияния производителей-производителей путем сопоставления шаблонов на ConcatMap ... (ConcatMap ... ...), два потребителя одного входа, которые приводят к возможности совместного использования брака, не обязательно "близки" друг к другу в AST таким же образом.

Если бы мы могли пройти АСТ в противоположном направлении, то есть, начиная с Input s, было бы легче обнаружить параллельных потребителей одного входа. Я не могу понять, как это сделать, однако, учитывая, что каждая операция относится только к ее вводу, а не к выходным файлам.

Вопрос: Может ли слияние слияния быть реализовано с использованием этого представления AST или есть какое-то другое (например, графическое или продолжение) представление, которое позволило бы нам реализовать sibling fusion? Предпочтительно, при использовании GADT для безопасности типов.

Ответы

Ответ 1

Я создал монстра, которого я сейчас развяжу в мире. Вот реализация вашей трансформации в Идрисе.

Сначала я начал изучать это в Haskell, и проблема в том, что мы по существу ищем способ сбора для каждой переменной набора функций f1 :: a -> b1, f2 :: a -> b2, .... Придумать хорошее представление для этого в Haskell сложно, потому что, с одной стороны, мы хотели бы скрыть типы b1, b2, ... за экзистенциальным, но, с другой стороны, когда мы видим a ConcatMap, нам нужно построить функцию который извлекает правильные координаты из нашего [Either b1 (Either b2 (...))] только в правильном типе.

Итак, прежде всего, давайте удостовериться, что ссылки на переменные хорошо скопированы и хорошо напечатаны путем индексирования Dist с переменными в области видимости и с помощью индексации De Bruijn для вхождения переменных:

%default total

Ctx : Type
Ctx = List Type

data VarPtr : Ctx -> Type -> Type where
  here : VarPtr (a :: ctx) a
  there : VarPtr ctx b -> VarPtr (a :: ctx) b

data Dist : Ctx -> Type -> Type where
  Input : Dist ctx a
  Concat2 : Dist ctx a -> Dist ctx a -> Dist ctx a
  ConcatMap : (a -> List b) -> Dist ctx a -> Dist ctx b
  Let : Dist ctx a -> Dist (a :: ctx) b -> Dist ctx b
  Var : VarPtr ctx a -> Dist ctx a

Как можно видеть, я сделал два упрощения Dist:

В любом случае все всегда похоже на список. ConcatMap тип Dist ctx a -> Dist ctx b вместо Dist ctx (List a) -> Dist ctx (List b). Только с комбинаторами, указанными в исходном вопросе, единственные значения Dist, которые можно построить, - это списки в любом случае. Это делает реализацию проще (другими словами, я сталкивался со всеми видами ненужных осложнений, прежде чем я сделал это изменение).
Concat2 является двоичным вместо n-арного. Изменение fuseHoriz ниже для supprot n-ary concatenation - упражнение, оставленное читателю.

Пусть сначала внедряется вертикальное слияние, просто чтобы намочить ноги:

fuseVert : Dist ctx a -> Dist ctx a
fuseVert Input = Input
fuseVert (Concat2 xs ys) = Concat2 (fuseVert xs) (fuseVert ys)
fuseVert (ConcatMap f d) = case fuseVert d of
    ConcatMap g d' => ConcatMap (concatMap f . g) d'
    d' => ConcatMap f d'
fuseVert (Let d0 d) = Let (fuseVert d0) (fuseVert d)
fuseVert (Var k) = Var k

До сих пор так хорошо:

namespace Examples
  f : Int -> List Int
  f = return . (+1)

  g : Int -> List Int
  g = return . (* 2)

  ex1 : Dist [] Int
  ex1 = ConcatMap f $ ConcatMap g $ Input

  ex1' : Dist [] Int
  ex1' = ConcatMap (concatMap f . g) $ Input

  prf : fuseVert ex1 = ex1'
  prf = Refl

Теперь для забавной части. Нам нужно хорошее представление "набора функций из одной области" и способ указать на определенную функцию (с определенным кодоманом) в этой коллекции. Мы будем собирать эти функции из вызовов ConcatMap f (Var v), с помощью v; а затем замените сам вызов отверстием, которое будет заполнено, как только мы закончим собирать все.

Когда мы сталкиваемся с Concat2 d1 d2, нам нужно будет объединить функции, собранные с обеих сторон, а затем ослабить отверстия в d1 и d2 для этого расширенного набора. По этой причине я использую двоичное дерево вместо плоского списка, так что ослабление легко реализовать.

Он находится в своем собственном пространстве имен, так как я повторно использую терминологию here/there:

namespace Funs
  data Funs : Type -> Type where
    None : Funs a
    Leaf : (a -> List b) -> Funs a
    Branch : Funs a -> Funs a -> Funs a

  instance Semigroup (Funs a) where
    (<+>) = Branch

  data FunPtr : Funs a -> Type -> Type where
    here : FunPtr (Leaf {b} _) b
    left : FunPtr fs b -> FunPtr (Branch fs _) b
    right : FunPtr fs b -> FunPtr (Branch _ fs) b

Теперь, когда у нас есть представление для набора всех функций, применяемых к данной переменной, мы можем, наконец, добиться некоторого прогресса в реализации горизонтального слияния.

Чтобы повторить, цель состоит в том, чтобы сделать что-то вроде

let xs = Input :: [A]
in Concat2 (E $ ConcatMap f xs) (F $ ConcatMap g xs)
where
  f :: A -> [B]
  g :: A -> [C]

во что-то вроде

let xs = Input :: [A]
    xs' = ConcatMap (\x -> map Left (f x) ++ map Right (g x)) xs :: [(Either B C)]
in Concat2 (E $ ConcatMap (either return (const []) xs') (F $ ConcatMap (either (const []) return) xs')

Итак, прежде всего, мы должны иметь возможность кодировать memoizer (определение xs') из набора функций, примененных в xs:

  memoType : Funs a -> Type
  memoType None = ()
  memoType (Leaf {b} _) = b
  memoType (Branch fs1 fs2) = Either (memoType fs1) (memoType fs2)

  memoFun : (fs : Funs a) -> (a -> List (memoType fs))
  memoFun None = const []
  memoFun (Leaf f) = f
  memoFun (Branch fs1 fs2) = (\xs => map Left (memoFun fs1 xs) <+> map Right (memoFun fs2 xs))

  memoExpr : (fs : Funs a) -> Dist (a :: ctx) (memoType fs)
  memoExpr fs = ConcatMap (memoFun fs) (Var here)

Это будет не очень полезно, если мы не сможем найти эти мемуаризованные результаты позже:

  lookupMemo : {fs : Funs a} -> (i : FunPtr fs b) -> (memoType fs -> List b)
  lookupMemo {fs = Leaf f} here = \x => [x]
  lookupMemo {fs = (Branch fs1 fs2)} (left i) = either (lookupMemo i) (const [])
  lookupMemo {fs = (Branch fs1 fs2)} (right i) = either (const []) (lookupMemo i)

Теперь, когда мы пересекаем исходное дерево, мы, естественно, собираем способы использования (через ConcatMap) нескольких переменных одновременно, так как вполне возможно иметь что-то вроде

let xs = ...
in Concat2 (ConcatMap f xs) (let ys = ... in ... (ConcatMap g xs) ...)

Это будет заселено в lockstep с помощью контекста переменной, поскольку в каждой привязке Let мы также можем сгенерировать memoizer всех применений новой переменной.

namespace Usages
  data Usages : Ctx -> Type where
    Nil : Usages []
    (::) : {a : Type} -> Funs a -> Usages ctx -> Usages (a :: ctx)

  unused : {ctx : Ctx} -> Usages ctx
  unused {ctx = []} = []
  unused {ctx = _ :: ctx} = None :: unused {ctx}

  instance Semigroup (Usages ctx) where
    [] <+> [] = []
    (fs1 :: us1) <+> (fs2 :: us2) = (fs1 <+> fs2) :: (us1 <+> us2)

Мы зарезервируем пространство для этих синтетических переменных:

  ctxDup : {ctx : Ctx} -> Usages ctx -> Ctx
  ctxDup {ctx = []} us = []
  ctxDup {ctx = t :: ts} (fs :: us) = (memoType fs) :: t :: ctxDup us

  varDup : {us : Usages ctx} -> VarPtr ctx a -> VarPtr (ctxDup us) a
  varDup {us = _ :: _} here = there here
  varDup {us = _ :: _} (there v) = there $ there $ varDup v

Теперь мы, наконец, готовы определить внутреннее промежуточное представление оптимизатора: "Dist с отверстиями". Каждое отверстие представляет собой приложение функции для переменной, которое будет заполнено, когда мы будем знать все обычаи, и у нас есть все синтетические переменные для них в области:

namespace HDist
  data Hole : Usages ctx -> Type -> Type where
    here : FunPtr u b -> Hole (u :: us) b
    there : Hole us b -> Hole (_ :: us) b

  resolve : {us : Usages ctx} -> Hole us b -> Exists (\a => (VarPtr (ctxDup us) a, a -> List b))
  resolve (here i) = Evidence _ (here, lookupMemo i)
  resolve (there h) with (resolve h) | Evidence a (v, f) = Evidence a (there $ there v, f)

  data HDist : Usages ctx -> Type -> Type where
    HInput : HDist us a
    HConcat : HDist us a -> HDist us a -> HDist us a
    HConcatMap : (b -> List a) -> HDist us b -> HDist us a
    HLet : HDist us a -> (fs : Funs a) -> HDist (fs :: us) b -> HDist us b
    HVar : {ctx : Ctx} -> {us : Usages ctx} -> VarPtr ctx a -> HDist us a
    HHole : (hole : Hole us a) -> HDist us a

Итак, как только мы получим такой дырявый Dist, заполнение его - это просто вопрос его ходьбы и разрешения дыр:

fill : HDist us a -> Dist (ctxDup us) a
fill HInput = Input
fill (HConcat e1 e2) = Concat2 (fill e1) (fill e2)
fill (HConcatMap f e) = ConcatMap f $ fill e
fill (HLet e0 fs e) = Let (fill e0) $ Let (memoExpr fs) $ fill e
fill (HVar x) = Var (varDup x)
fill (HHole h) with (resolve h) | Evidence a (v, f) = ConcatMap f $ Var v

Горизонтальное слияние - это всего лишь проблема смазки локтя: превращение a Dist ctx a в HDist us a, так что каждый ConcatMap f (Var v) превращается в HHole. Нам нужно сделать дополнительный забавный танец, чтобы сдвинуть отверстия вокруг, объединяя два Usages с двух сторон Concat2.

weakenHoleL : Hole us1 a -> Hole (us1 <+> us2) a
weakenHoleL {us1 = _ :: _} {us2 = _ :: _} (here i) = here (left i)
weakenHoleL {us1 = _ :: _} {us2 = _ :: _} (there h) = there $ weakenHoleL h

weakenHoleR : Hole us2 a -> Hole (us1 <+> us2) a
weakenHoleR {us1 = _ :: _} {us2 = _ :: _} (here i) = here (right i)
weakenHoleR {us1 = _ :: _} {us2 = _ :: _} (there h) = there $ weakenHoleR h

weakenL : HDist us1 a -> HDist (us1 <+> us2) a
weakenL HInput = HInput
weakenL (HConcat e1 e2) = HConcat (weakenL e1) (weakenL e2)
weakenL (HConcatMap f e) = HConcatMap f (weakenL e)
weakenL {us1 = us1} {us2 = us2} (HLet e fs x) = HLet (weakenL e) (Branch fs None) (weakenL {us2 = None :: us2} x)
weakenL (HVar x) = HVar x
weakenL (HHole hole) = HHole (weakenHoleL hole)

weakenR : HDist us2 a -> HDist (us1 <+> us2) a
weakenR HInput = HInput
weakenR (HConcat e1 e2) = HConcat (weakenR e1) (weakenR e2)
weakenR (HConcatMap f e) = HConcatMap f (weakenR e)
weakenR {us1 = us1} {us2 = us2} (HLet e fs x) = HLet (weakenR e) (Branch None fs) (weakenR {us1 = None :: us1} x)
weakenR (HVar x) = HVar x
weakenR (HHole hole) = HHole (weakenHoleR hole)

fuseHoriz : Dist ctx a -> Exists {a = Usages ctx} (\us => HDist us a)
fuseHoriz Input = Evidence unused HInput
fuseHoriz (Concat2 d1 d2) with (fuseHoriz d1)
  | Evidence us1 e1 with (fuseHoriz d2)
    | Evidence us2 e2 =
        Evidence (us1 <+> us2) $ HConcat (weakenL e1) (weakenR e2)
fuseHoriz {ctx = _ :: ctx} (ConcatMap f (Var here)) =
    Evidence (Leaf f :: unused) (HHole (here here))
fuseHoriz (ConcatMap f d) with (fuseHoriz d)
  | Evidence us e = Evidence us (HConcatMap f e)
fuseHoriz (Let d0 d) with (fuseHoriz d0)
  | Evidence us0 e0 with (fuseHoriz d)
    | Evidence (fs :: us) e =
        Evidence (us0 <+> us) $ HLet (weakenL e0) (Branch None fs) $ weakenR {us1 = None :: us0} e
fuseHoriz (Var v) = Evidence unused (HVar v)

Мы можем использовать это чудовище, объединив его с fuseVert и подав его на fill:

fuse : Dist [] a -> Dist [] a
fuse d = fill $ getProof $ fuseHoriz . fuseVert $ d

И престо:

namespace Examples
  ex2 : Dist [] Int
  ex2 = Let Input $
        Concat2 (ConcatMap f (Var here))
                (ConcatMap g (Var here))

  ex2' : Dist [] Int
  ex2' = Let Input $
         Let (ConcatMap (\x => map Left [] ++ map Right (map Left (f x) ++ map Right (g x))) (Var here)) $
         Concat2 (ConcatMap f' (Var here)) (ConcatMap g' (Var here))
    where
      f' : Either () (Either Int Int) -> List Int
      f' = either (const []) $ either return $ const []

      g' : Either () (Either Int Int) -> List Int
      g' = either (const []) $ either (const []) $ return

  prf2 : fuse ex2 = ex2'
  prf2 = Refl

Добавление

Мне жаль, что я не мог слить fuseVert в fuseHoriz, так как я думаю, что все, что ему нужно, это дополнительный случай:

fuseHoriz (ConcatMap f (ConcatMap g d)) = fuseHoriz (ConcatMap (concatMap f . g) d)

Однако это смутило проверку проверки Idris, если я не добавлю assert_smaller в ConcatMap (concatMap f . g) d vs ConcatMap f (ConcatMap g d)), который я не понимаю, потому что у меня есть еще один слой конструкторов ConcatMap, чем другой.

Внедрение слияния с использованием стандартного АСТ

Ответы

Ответ 1

Добавление