Блог

Структурированное кодирование графов в параметрическом абстрактном синтаксисе высшего порядка (PHOAS)

Я читаю статью Оливера и Кука «Функциональное программирование со структурированными графами» (слайды, черновик документа.), предлагающую элегантное решение для кодирования совместного использования и циклов в графоподобных структурах с использованием рекурсивных привязок в PHOAS.

AST (пример потока)

Например, потоки с обратными ребрами могут быть закодированы как :

 -- 'x' is the element type, 'b' is the PHOAS's abstract variable:
data PS0 x b = Var0 b
             | Mu0 (b -> PS0 x b) -- recursive binder
             | Cons0 x  (PS0 x b)
-- Closed terms:
newtype Stream0 x = Stream0 { runS0 :: forall b. PS0 x b }

-- Example : [0, 1, 2, 1, 2, 1, 2, ...
exPS0 = Stream0 $ Cons0 0 (Mu0 $ x -> Cons0 1 (Cons0 2 $ Var0 x))
  

Сворачивание (в список)

AST можно свернуть в список без учета циклов:

 toListPS0 :: Stream0 x -> [x]
toListPS0 = go . runS0
  where
    go (Var0 x) = x
    go (Mu0 h) = go . h $ [] -- nil
    go (Cons0 x xs) =  x : go xs

-- toListPS0 exPS0 == [0, 1, 2]
  

Или создайте бесконечный список, взяв фиксированную точку рекурсивных связующих:

 toListRecPS0 :: Stream0 x -> [x]
toListRecPS0 = go . runS0
  where
    go (Var0 x) = x
    go (Mu0 h) = fix $ go . h -- fixpoint
    go (Cons0 x xs) = x : go xs

-- toListRecPS0 exPS0 == [0, 1, 2, 1, 2, 1, 2, ...
  

Квазимонадический join

Авторы отмечают, что кодирование представляет собой квазимонаду, имеющую оба join и return , но не fmap .

 returnPS0 :: b -> PS0 x b
returnPS0 = Var0

joinPS0 :: PS0 x (PS0 x b) -> PS0 x b
joinPS0 (Var0 b) = b
joinPS0 (Mu0 h) = Mu0 $ joinPS0 . h . Var0
joinPS0 (Cons0 x xs) = Cons0 x $ joinPS0 xs
  

Это можно использовать для развертывания одного уровня рекурсивной привязки:

 unrollPS0 :: Stream0 x -> Stream0 x
unrollPS0 s = Stream0 $ joinPS0 . go $ runS0 s
  where
    go (Mu0 g) = g . joinPS0 . Mu0 $ g
    go (Cons0 x xs) = Cons0 x $ go xs
    go e = e

-- toListPS0 . unrollPS0 $ exPS0 == [0, 1, 2, 1, 2]
  

PHOAS бесплатно

Это напомнило мне отличную статью Эдварда Кметта о FPComplete: PHOAS бесплатно. Идея состоит в том, чтобы сделать AST профунктором, разделяющим отрицательное и положительное вхождение переменной PHOAS.

«Фиксированная точка с порядком размещения» функтора представлена AST, подобным свободной монаде (Fegaras и Sheard):

 data Rec p a b = Place b
               | Roll (p a (Rec p a b))
  

Provided that p is a profunctor (or that p a is a functor), Rec p a is a monad (and a functor !).

The stream AST can be encoded with the non-recursive functor PSF :

 data PSF x a b = MuF (a -> b)
               | ConsF x   b

-- Type and pattern synonyms:
type PS1 x = Rec (PSF x)
pattern Var1 x = Place x
pattern Mu1 h = Roll (MuF h)
pattern Cons1 x xs = Roll (ConsF x xs)

-- Closed terms:
newtype Stream1 x = Stream1 { runS1 :: forall b. PS1 x b b }

-- Example : [0, 1, 2, 1, 2, 1, 2, ...
exPS1 = Stream1 $ Cons1 0 (Mu1 $ x -> Cons1 1 (Cons1 2 (Var1 x)))
  

Проблема

Экземпляр join из Rec экземпляра monad отличается от оригинала joinPS1 из статьи!

Грамотный перевод joinPS0 использования синонимов шаблона:

 joinPS1 :: PS1 x (PS1 x b b) (PS1 x b b) -> PS1 x b b
joinPS1 (Var1 b) = b
joinPS1 (Mu1 h) = Mu1 $ joinPS1 . h . Var1 -- Var1 affects the negative occurrences
joinPS1 (Cons1 x xs) = Cons1 x $ joinPS1 xs
  

Принимая во внимание, что встраивание (>>=) и fmap (>>= id) ввод дают нам :

 joinFreePSF :: PS1 x a (PS1 x a b) -> PS1 x a b
joinFreePSF (Var1 b) = b
joinFreePSF (Mu1 h) = Mu1 $ joinFreePSF . h -- No Var1 !
joinFreePSF (Cons1 x xs) = Cons1 x $ joinFreePSF xs
  

Итак, мой вопрос в том, почему эта разница?

Проблема в том, что такие операции, как unrollPS1 required join , которые «разбивают» как положительные, так и отрицательные вхождения монады (например, в joinPS1 типе).

Я думаю, что это связано с рекурсивным характером связующих. Я пытался переписать unrollPS1 , работая с типами, но я не уверен, что полностью понимаю, что происходит на уровне значений.

Замечание

Полностью общий тип joinPS1 (выводимый компилятором)

 joinPS1 :: PS1 x (PS1 x' a a') (PS1 x a' b) -> PS1 x a' b
  

Он может быть специализирован на a' ~ a ~ b и x' ~ x .

PS:

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

Полный код со всеми экземплярами доступен здесь (gist).

На самом деле вы можете легко восстановить Olivera и Cook join из моего соединения с монадой «profunctor HOAS»:

 joinPS1 = join . lmap Var
  

Их версия делает единственное, что она может делать в их типе.

Там они должны сохранять a = b , поэтому он делает это, вводя a Var . Здесь мы можем просто включить его отдельно. Это не требуется для монады и не должно выполняться для всех случаев.

Необходимость сохранения a и b синхронизации заключается в том, почему они могут быть только «псевдо-монадой» и почему profunctor HOAS позволяет вам на самом деле иметь настоящую монаду.