Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
I am currently self learning Category Theory and Simply typed lambda calculus (STLC). For learning purposes, I have implemented an STLC interpreter as given in Types and Programming Languages book of Benjamin Pierce. Now i am wondering if I can extend this interpreter with category of sets (category Set ). i.e. interpret expressions to construct sets, pushouts, pullbacks etc.
Unable to find any directions on how to do this. Can someone please provide any helpful suggestions on this?
There are at least two directions in which you can proceed.
First, Church's simple type theory (see also this explanation) extends the simply typed $\lambda$-calculus with the types of natural numbers and booleans, and other constructs that make it sufficiently expressive to encode a certain kind of classical set theory. These ideas were pursued in the HOL theorem provers. For instance, HOL light for a small implementation. This approach has the flavor of doing logic, i.e., there is no general notion of computation - as opposed to the simply typed $\lambda$-calculus, which is a programming language.
Second, dependent type theory, of which there are many variants, is also an extension of the simply typed $\lambda$-calculus. It can be used as a foundation of mathematics. They are used in proof assistants, such as Coq, Agda, and Lean. Some variants, notably Martin-Löf type theory, do retain the character of a programming language. In fact, Idris is a programming language based on dependent type theory.
None of the above is "set theory", but these formalisms are quite suitable for expressing mathematics, including category theory.
