# 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?