Skip to main content
added 381 characters in body
Source Link
varkor
  • 10.7k
  • 29
  • 72

fosco gives a good overview of the general theory in their answer. I would like to point out two different generalisations of algebraic theory that are not, as far as I am aware, subsumed by any of these, but are relevant to your comment:

For instance I would be interested to hear about what can be done to obtain type theories as some kind algebraic theories.

Simple type theories may be described as algebraic structures with multisorted binding operators and algebraic sort structure. A step in this direction, from the perspective of algebraic theories, is taken by Fiore and Mahmoud in Second-Order Algebraic Theories. They consider a generalisation of algebraic theory in which one considers categories with finite products and an exponentiable object. The exponentiable object permits the representation of second-order operators, like the $\lambda$-abstraction operator from the simply-typed $\lambda$-calculus. They only consider the single-sorted setting, but it is easy enough to extend to the multisorted setting. The equivalence with an equational logic is contained in Fiore and Hur's Second-Order Equational Logic.

For type operators (including type operators with binding, as are found in the polymorphic $\lambda$-calculus), an operadic/presheaf-theoretic approach is contained in Fiore and Hamana's Multiversal Polymorphic Algebraic Theories, which also contains the equivalence with an equational logic.

For substructural type theories, one starting point is the work of Power and Tanaka, such as Pseudo-distributive laws and axiomatics for variable binding, which is also based on the operadic/presheaf-theoretic approach.

Representing other kinds of type theory in this way, such as dependent type theories, is mostly an open question. (By "type theory", I mean at least some structure with a notion of variable binding operator.)

fosco gives a good overview of the general theory in their answer. I would like to point out two different generalisations of algebraic theory that are not, as far as I am aware, subsumed by any of these, but are relevant to your comment:

For instance I would be interested to hear about what can be done to obtain type theories as some kind algebraic theories.

Simple type theories may be described as algebraic structures with multisorted binding operators and algebraic sort structure. A step in this direction, from the perspective of algebraic theories, is taken by Fiore and Mahmoud in Second-Order Algebraic Theories. They consider a generalisation of algebraic theory in which one considers categories with finite products and an exponentiable object. The exponentiable object permits the representation of second-order operators, like the $\lambda$-abstraction operator from the simply-typed $\lambda$-calculus. They only consider the single-sorted setting, but it is easy enough to extend to the multisorted setting. The equivalence with an equational logic is contained in Fiore and Hur's Second-Order Equational Logic.

For type operators (including type operators with binding, as are found in the polymorphic $\lambda$-calculus), an operadic/presheaf-theoretic approach is contained in Fiore and Hamana's Multiversal Polymorphic Algebraic Theories, which also contains the equivalence with an equational logic.

Representing other kinds of type theory in this way, such as dependent type theories, is mostly an open question.

fosco gives a good overview of the general theory in their answer. I would like to point out two different generalisations of algebraic theory that are not, as far as I am aware, subsumed by any of these, but are relevant to your comment:

For instance I would be interested to hear about what can be done to obtain type theories as some kind algebraic theories.

Simple type theories may be described as algebraic structures with multisorted binding operators and algebraic sort structure. A step in this direction, from the perspective of algebraic theories, is taken by Fiore and Mahmoud in Second-Order Algebraic Theories. They consider a generalisation of algebraic theory in which one considers categories with finite products and an exponentiable object. The exponentiable object permits the representation of second-order operators, like the $\lambda$-abstraction operator from the simply-typed $\lambda$-calculus. They only consider the single-sorted setting, but it is easy enough to extend to the multisorted setting. The equivalence with an equational logic is contained in Fiore and Hur's Second-Order Equational Logic.

For type operators (including type operators with binding, as are found in the polymorphic $\lambda$-calculus), an operadic/presheaf-theoretic approach is contained in Fiore and Hamana's Multiversal Polymorphic Algebraic Theories, which also contains the equivalence with an equational logic.

For substructural type theories, one starting point is the work of Power and Tanaka, such as Pseudo-distributive laws and axiomatics for variable binding, which is also based on the operadic/presheaf-theoretic approach.

Representing other kinds of type theory in this way, such as dependent type theories, is mostly an open question. (By "type theory", I mean at least some structure with a notion of variable binding operator.)

Source Link
varkor
  • 10.7k
  • 29
  • 72

fosco gives a good overview of the general theory in their answer. I would like to point out two different generalisations of algebraic theory that are not, as far as I am aware, subsumed by any of these, but are relevant to your comment:

For instance I would be interested to hear about what can be done to obtain type theories as some kind algebraic theories.

Simple type theories may be described as algebraic structures with multisorted binding operators and algebraic sort structure. A step in this direction, from the perspective of algebraic theories, is taken by Fiore and Mahmoud in Second-Order Algebraic Theories. They consider a generalisation of algebraic theory in which one considers categories with finite products and an exponentiable object. The exponentiable object permits the representation of second-order operators, like the $\lambda$-abstraction operator from the simply-typed $\lambda$-calculus. They only consider the single-sorted setting, but it is easy enough to extend to the multisorted setting. The equivalence with an equational logic is contained in Fiore and Hur's Second-Order Equational Logic.

For type operators (including type operators with binding, as are found in the polymorphic $\lambda$-calculus), an operadic/presheaf-theoretic approach is contained in Fiore and Hamana's Multiversal Polymorphic Algebraic Theories, which also contains the equivalence with an equational logic.

Representing other kinds of type theory in this way, such as dependent type theories, is mostly an open question.