Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic

We formalise and study the notion of polymorphic algebraic theory, as understood in the mathematical vernacular as a theory presented by equations between polymorphically-typed terms with both type and term variable binding. The prototypical example of a polymorphic algebraic theory is System F, but our framework applies more widely. The extra generality stems from a mathematical analysis that has led to a unified theory of polymorphic algebraic theories with the following ingredients: ; polymorphic signatures that specify arbitrary polymorphic operators (e.g. as in extended λ-calculi and algebraic effects); ; metavariables, both for types and terms, that enable the generic description of meta-theories; ; multiple type universes that allow a notion of translation between theories that is parametric over different type universes; ; polymorphic structures that provide a general notion of algebraic model (including the PL-category semantics of System F); ; a Polymorphic Equational Logic that constitutes a sound and complete logical framework for equational reasoning. Our work is semantically driven, being based on a hierarchical two-levelled algebraic modelling of abstract syntax with variable binding.