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

I have a written a compiler from the STLC to CCCs but this involves a lot of ugly tuple shuffling.

Is it possible to get the STLC for free from the definition of a closed Cartesian category?

  • $\begingroup$ Have you seen Compiling to Categories? $\endgroup$
    – jmite
    Sep 3, 2020 at 2:31
  • $\begingroup$ @jmite yeah. I have even written such compilers myself as I mentioned in the question. But one can compile to assembly code as well. I feel like lambda calculus is supposed to have a deeper relationship to cccs than to assembly code. $\endgroup$ Sep 5, 2020 at 23:59


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.