Partial evaluation with expansion and contraction

This is still work-in-progress because I was distracted by reddit last week.

Lets model bicartesian closed categories quickly in Haskell.

First the functors.

data Ft
    = Var Int
    | Terminal
    | Prod Ft Ft
    | Exp Ft Ft
    | Sum Ft Ft
    deriving (Show, Eq)

Then the natural transformations.

data Nt
    = Atom Int
    | Const Ft
    | Pair Nt Nt
    | Cur Nt
    | Alt Nt Nt
    | Fst Ft Ft
    | Snd Ft Ft
    | Ap Ft Ft
    | Inl Ft Ft
    | Inr Ft Ft
    | Comp Nt Nt
    deriving (Show, Eq)

To verify that our construction of natural transformations is valid, we need to define what is a valid NT construction. We can retrieve the left and right functor from a valid natural transformation.

is_valid :: Nt -> Maybe (Ft, Ft)
is_valid (Atom n) = pure (Var n, Var n)
is_valid (Const y) = pure (Terminal, y)
is_valid (Pair f g) = do
    (x, x') <- is_valid f
    (y, y') <- is_valid g
    guard (x' == y')
    pure (Prod x y, x') 
is_valid (Cur f) = do
    (x, w) <- is_valid f
    (y, z) <- is_prod w
    pure (Exp x z, y)
is_valid (Alt f g) = do
    (x, x') <- is_valid f
    (y, y') <- is_valid g
    guard (x == y)
    pure (x, Sum x' y') 
is_valid (Fst x y) = pure (x, Prod x y)
is_valid (Snd x y) = pure (y, Prod x y)
is_valid (Ap x y) = pure (x, Prod (Exp x y) y)
is_valid (Inl x y) = pure (Sum x y, x)
is_valid (Inr x y) = pure (Sum x y, y)
is_valid (Comp f g) = do
    (x, x') <- is_valid f
    (y, y') <- is_valid g
    guard (x' == y)
    pure (x, y')

is_prod :: Ft -> Maybe (Ft, Ft)
is_prod (Prod x y) = pure (x, y)

is_exp :: Ft -> Maybe (Ft, Ft)
is_exp (Exp x y) = pure (x, y)

There's a natural transformation for every functor. We can describe them like this:

ft :: Ft -> Nt
ft (Var n)    = Atom n
ft Terminal   = Const Terminal
ft (Prod x y) = Pair (Fst x y) (Snd x y)
ft (Exp x y)  = Cur (Ap x y)
ft (Sum x y)  = Alt (Inl x y) (Inr x y)

This also means that we can expand every functor into an "expanded" natural transformation:

prod :: Nt -> Nt -> Maybe Nt
prod f g = do
    (x, x') <- is_valid f
    (y, y') <- is_valid g
    pure (Pair (f `Comp` Fst x' y')
               (g `Comp` Snd x' y'))

exp :: Nt -> Nt -> Maybe Nt
exp f g = do
    (x, x') <- is_valid f
    (y, y') <- is_valid g
    p <- prod (ft (Exp x' y)) g
    pure (Cur (f `Comp` Ap x' y `Comp` p))

sum :: Nt -> Nt -> Maybe Nt
sum f g = do
    (x, x') <- is_valid f
    (y, y') <- is_valid g
    pure (Alt (Inl x y `Comp` f)
              (Inr x y `Comp` g))

I've explained some of this in earlier posts. That is why this has been really fast-faced so far.

This model is different from earlier structures by natural transformations being described. The identity natural transformations are no longer explicit constructs. It also means that instead of just using unit/counit natural transformations it's necessary to pick a "factorizer", a map from morphisms of one category into an another category.

I picked the representation slightly based on what I'd expect to be convenient to normalise. The next step would be to contract every contractible natural transformation pair.

It's possible to normalise the structure from left to right, or from right to left. We haven't tried the left-to-right yet.

Now, can we give this thing so unneccessarily abstract and incomprehensible implementation that half of the audience pukes on a floor?

data S r
    = Cons ((S r -> r) -> r) ((S r -> r) -> r)
    | Func Nt (S r)
    | LeftSide (S r)
    | RightSide (S r)
    | Syn r

class N r where
    alt :: (S r -> r) -> (S r -> r) -> (S r -> r)

lwnf :: N r => Nt -> (S r -> r) -> (S r -> r)
lwnf (Atom n) f = f
lwnf (Pair i j) f = \q -> f (Cons (\ret -> lwnf i ret q)
                                  (\ret -> lwnf j ret q))
lwnf (Cur i) f = f . Func i
lwnf (Alt i j) f = alt (lwnf i f) (lwnf j f)
lwnf (Fst a b) f = select_left where select_left (Cons a _) = a f
lwnf (Snd a b) f = select_right where select_right (Cons _ b) = b f
lwnf (Ap a b) f = apply where
    apply (Cons a b) = a (cont f b)
    cont ret arg (Func nt sr) = lwnf nt ret (Cons ($sr) arg)
lwnf (Inl a b) f = f . LeftSide
lwnf (Inr a b) f = f . RightSide
lwnf (Comp i j) f = lwnf j (lwnf i f)

instance N Nt where
    alt f g x = Alt (f x) (g x)

nf :: Nt -> Maybe Nt
nf f = do
    (lhs, rhs) <- is_valid f
    pure $ reflect rhs (lwnf f (reify lhs rhs))

reify :: Ft -> Ft -> S Nt -> Nt
reify (Var n) _ (Syn x) = x
reify (Terminal) ty _ = Const ty
reify (Prod a b) ty (Cons f g) = Pair (f (reify a ty)) (g (reify b ty))
reify (Exp a b) ty (Func nt sr) = Cur (lwnf nt
                                            (reify a (Prod ty b))
                                            (Cons ($sr) (reflect b)))
reify (Sum a b) ty (LeftSide x) = Inl a b `Comp` reify a ty x
reify (Sum a b) ty (RightSide x) = Inr a b `Comp` reify b ty x

reflect :: Ft -> (S Nt -> Nt) -> Nt
reflect (Var n) f = f $ Syn (Atom n)
reflect (Terminal) f = f $ Syn (Const Terminal)
reflect (Prod a b) f = f $ Cons (reflect a) (reflect b) 
reflect (Exp a b) f = f $ Func _ _
reflect (Sum a b) f = Alt (reflect a f) (reflect b f)

The answer seem to be... what?

This isn't a complete program. I'm still wondering what the 'reflect' should end up constructing in the function case. I suppose it should construct Ap -structure.

So is this just plain gibberish? Nope. The lwnf stands for 'left weak normal form'. Since every structure is expanded, we can trust it to have a constructor concealed inside. However a trail needs to be followed to locate it. Likewise I added a "continuation" because the trail may split by the sum type.

I'm not sure whether the reify/reflect is correct there.

The result is an evaluator. Again. Well I'll try to figure the missing structure on the weekdays. I think it's just requires a slightly different organization on the Func -structure.

Though there's also an another idea lurking there.. The lwnf is resembles a functor. Though I don't recognize S r -> r, what is that? Well, it seems like an algebra, as the S forms a functor.

In the source category the objects would be functors and morphisms natural transformations between them. But how would that result in (S r -> r) -> (S r -> s) as the type of the morphism?

Similar posts