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$ Oct 2, 2017 at 15:52
  • $\begingroup$ And what would be a categorical model of singleton kinds ? $\endgroup$
    – nicolas
    Oct 3, 2017 at 10:52


Your Answer

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