Separate positive and negative occurrences of PHOAS variables in presence of recursive binders

Question

Structured Graph encoding in Parametric Higher Order Abstract Syntax (PHOAS)

I'm reading the paper "Functional Programming with Structured Graphs" by Olivera and Cook (Slides, draft paper.) proposing an elegant solution to encode sharing and cycles in graph-like structures using recursive bindings in PHOAS.

The AST (stream example)

For example, streams with back edges can be encoded as :

-- '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))

Folding (to list)

The AST can be folded into list without taking account of the cycles:

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]

Or produce an infinite list, by taking the fix-point of recursive binders:

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

Quasi-monadic join

The authors note that the encoding is a quasi-monad, having both join and return, but not 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

This can be used to unroll one level of recursive binding:

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 For Free

This reminded me the excellent article by Edward Kmett on FPComplete: PHOAS For Free. The idea is to make the AST a profunctor, separating negative and positive occurrence of PHOAS's variable.

The "fixpoint with place-order" of a functor is represented with a free-monad-like AST (Fegaras and 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)))

The problem

The join from the Rec monad instance is different than the original joinPS1 from the paper !

A literate translation of joinPS0 using the pattern synonyms is:

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

Whereas, inlining (>>=) and fmap in (>>= id) give us :

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

So my question is, why this difference?

The problem is that operations like unrollPS1 requires a join that "smash" both the positive and negative occurrences of the monad (like in the joinPS1 type).

I think it's related to the recursive nature of the binders. I tried to rewrite unrollPS1 by working with the types, but I'm not sure to have a full understanding of what is going on at the value level.

Remark

A fully general type of joinPS1 (inferred by the compiler) is

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

It can be specialized with a' ~ a ~ b and x' ~ x.

PS:

I don't try to achieve anything specific, it's more a matter of curiosity, like trying to connect the dots.

The full code with all the instances is available here (gist).

Answer 1

You can actually easily reconstruct the Olivera and Cook join from my "profunctor HOAS" free monad join:

joinPS1 = join . lmap Var

Their version does the only thing it can do in their type.

There they have to keep the a = b, so it does so by introducing a Var. Here we can just put it on separately. It isn't required for the monad, and shouldn't be done for all cases.

The need to keep a and b in sync is why theirs can only be a "pseudo-monad" and why profunctor HOAS lets you actually have a real monad.