2
$\begingroup$

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 ?

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

0

Reset to default

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.