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$ 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 you have read our privacy policy.

Browse other questions tagged or ask your own question.