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, privacy policy and cookie policy

Browse other questions tagged or ask your own question.