Binders are explained using presheaves (Pitts/Gabbay A new approach to Abstract Syntax with variable binding)

What is the equivalent (categorical) theory to explain first class modules as in 1ML ?

  • 2
    $\begingroup$ One can understand modules (including first class modules) in a language with singleton kinds so any categorical model of singleton kinds will suffice. $\endgroup$ – Daniel Gratzer Oct 2 '17 at 15:52
  • $\begingroup$ And what would be a categorical model of singleton kinds ? $\endgroup$ – nicolas Oct 3 '17 at 10:52

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.