<p>Binders are explained using presheaves (<a href="https://scholar.google.fr/scholar?client=safari&amp;rls=en&amp;oe=UTF-8&amp;gfe_rd=cr&amp;dcr=0&amp;um=1&amp;ie=UTF-8&amp;lr&amp;cites=2646104348392885758" rel="nofollow noreferrer">Pitts/Gabbay A new approach to Abstract Syntax with variable binding</a>)</p>

<p>What is the equivalent (categorical) theory to explain first class modules as in <a href="https://people.mpi-sws.org/~rossberg/1ml/" rel="nofollow noreferrer">1ML</a> ?</p>

CC BY-SA 3.0
2017-10-02T15:52:42.533Z
One can understand modules (including first class modules) in a language with singleton kinds so any categorical model of singleton kinds will suffice.
daniel gratzer
CC BY-SA 3.0
2017-10-03T10:52:38.233Z
And what would be a categorical model of singleton kinds ?
nicolas
<pl.programming-languages><ct.category-theory>
Categorical model of binding / first class modules
nicolas
# Categorical model of binding / first class modules

(Asked by: username_0 on 2017-10-02)

Binders are explained using presheaves ([Pitts/Gabbay A new approach to Abstract Syntax with variable binding](https://scholar.google.fr/scholar?client=safari&rls=en&oe=UTF-8&gfe_rd=cr&dcr=0&um=1&ie=UTF-8&lr&cites=2646104348392885758))

What is the equivalent (categorical) theory to explain first class modules as in [1ML](https://people.mpi-sws.org/~rossberg/1ml/) ?

**Tags:** pl.programming-languages, ct.category-theory
> **Comments:**
> **username_1**: One can understand modules (including first class modules) in a language with singleton kinds so any categorical model of singleton kinds will suffice.  
> **username_0**: And what would be a categorical model of singleton kinds ?  

---

## 0 answers

