Dependently-typed languages often work this way! See for instance "Inductively Defined Propositions" in Coq. (remembering, of course, that propositions are ty

Dependently-typed languages often work this way! See for instance "Inductively Defined Propositions" in Coq. (remembering, of course, that propositions are types [2], which proof assistants take quite literally) [1] https://softwarefoundations.cis.upenn.edu/lf-current/IndProp.html https://softwarefoundations.cis.upenn.edu/lf-current/IndProp... [2] https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as...