5
$\begingroup$

I have heard the simply typed lambda calculus is the internal language of Cartesian closed categories.

What's the internal language of the opposite type of category?

The rules dual to currying and uncurrying are:

$$ \mathrm{mal} : \mathrm{Hom}(b, a + c) \to \mathrm{Hom}(b \vdash a, c) \\ \mathrm{try} : \mathrm{Hom}(b \vdash a, c) \to \mathrm{Hom}(b, a + c) $$

I have the intuition the opposite category would correspond to continuation passing style or pattern matching but the opposite typing rules seem very strange and hard to figure out.

Trivially one could interpret/compile the simply typed lambda calculus in reverse but that would be extraordinarily confusing.

I have found with a little bit of finagling we can get rules that resemble continuation passing style.

$$ \mathrm{kont} : \mathrm{Hom}(x, b) \to \mathrm{Hom}(c, \mathrm{0}) \to \mathrm{Hom}(x, b \vdash c) \\ \mathrm{kont} \, x \, k = [\mathrm{absurd} \circ k , \mathrm{id}] \circ \mathrm{try} \, \mathrm{id} \circ x $$ $$ \mathrm{jump} : \mathrm{Hom}(x, b \vdash a) \to \mathrm{Hom}(b, a) \to \mathrm{Hom}(x, \mathrm{0}) \\ \mathrm{jump} \, k \, x = \mathrm{mal} \, ( \mathrm{i}_1 \circ x ) \circ k $$ $$ \mathrm{env} : \mathrm{Hom}(x, b \vdash a) \to \mathrm{Hom}(x, b) \\ \mathrm{env} \, k = \mathrm{mal} \, \mathrm{i}_2 \circ k$$

These are still pretty hard to figure out an interpretation for though.

Improve this question
$\endgroup$
6
  • $\begingroup$ This is mentioned in passing in A Cointuitionistic Adjoint Logic, but it doesn't go into detail. In the end, there's not much motivation for cointuitionistic logic, because you may always just take the opposite category and work with that. Note that you don't even have standard contexts in a coCCC, because you don't have products. $\endgroup$
    – varkor
    Sep 8, 2020 at 22:27
  • $\begingroup$ Ok suppose you add sums/coproducts to the simply typed lambda calculus. Then you can get products/contexts back? But any logical dual of simply typed lambda calculus should be exactly as powerful because you can always interprete it as the opposite simply typed lambda calculus. I think I think I get what you mean about contexts, I had to work around this by using parametric hoas and universal quantification. Instead of pair : Term a -> Term b -> Term (a, b) I had copair : (x a -> Term x c) -> (x b -> Term x c) -> x (a, b) -> Term x c $\endgroup$
    – Molly Stewart-Gallus
    Sep 8, 2020 at 23:18
  • $\begingroup$ You could indeed add sums in the opposite category to get ordinary contexts, but again: you may as well work directly with the STLC with sums. As a purely formal exercise, it's possible to do, but likely unenlightening. $\endgroup$
    – varkor
    Sep 8, 2020 at 23:25
  • $\begingroup$ Ok but I don't think it should be any less powerful. You can write a wrapper datatype to change the direction of arrows in any programming language newtype Op a b = Op (b -> a) but that doesn't change the power of it it just changes how you think about what's already there. So indeed you wouldn't write it with contexts the same way but thats the the point. $\endgroup$
    – Molly Stewart-Gallus
    Sep 9, 2020 at 0:11
  • $\begingroup$ Ugh. So I made a backwards interpretation that compiles higher order abstract syntax of backwards github.com/sstewartgallus/prologish and it's still confusing to me. $\endgroup$
    – Molly Stewart-Gallus
    Sep 12, 2020 at 18:35

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Browse other questions tagged or ask your own question.