Interested in a weird graduate student project?
The question is can we bring the language of category theory1 and verifiable programs2 to the world of cognitive modeling? To be honest, I rather doubt it, at least in the near term, but I am going to try, and I would love to have some help on this quest, but anyone contemplating it should think long and hard about the trade-offs. It will be an adventure of exploration, fun to be sure, but a risky foundation for a career. The surer path to academic stability will be to grind away in a lab that is exploiting known science to accumulate incrementally new knowledge on a socially important topic.
This project also requires someone who feels comfortable expressing their ideas formally. One wouldn't need to know either category theory or how to program in Lean4, but you shouldn't be put off or scared of either programming or expressing oneself in the language of mathematics. Notably, most psychology students will not have the background for this sort of thing, unless you are a renegade from CS or Math.
What then is the idea in a bit more detail? There is talk of a "theory crisis" in psychology.3 And this talk goes back a long time, maybe to Wundt and Watson, but certainly to 1978.4 Why does it exist? One suggestion is that we don't actually teach theory construction in psychology,5 for others it seems more to be about the way we formulate our ideas around effects instead of causes and explanations.6 The suggested solution is that we should convert our ideas into a formal language so that we can clearly test their implications and be unambiguous in their expression. For some authors this means equations, and for others it means programs, but I don't feel that either prescription is sufficiently explicit.
If we want general theories in psychology, theories that apply broadly beyond particular domains or paradigms, then we need to express them in a more general formal language; a language with the capacity to accommodate many formal framings. This is, I think, the value of the mathematical Ur-language, category theory. And given the way we write software in science, I don't have much faith that we should assume a program written to implement the proto-theoretical ideas of Prof. X necessarily is a faithful honoring of the proto-theoretical specifications. It is not just bugs. It is that we humans are not very good at reasoning about complex situations or thinking hierarchically and considering all the edge cases and end results of long chains of implications. We want to offload all that to software and computers. That is why a programming language that emphasizes formal verification and is able to be used for everyday programming tasks is what we need, and right now Lean4 seems closest to this goal (but there are other contenders, maybe some combination of Haskell and Agda?).
All this resolves to a process of deliberate theory creation, followed by translation to a formal specification in category theory, that is then implemented as code in Lean. Simulations results in Lean are compared to empirical results collected in parallel.
If any of this interests you, even if you do not want to spend your graduate student years studying it, please reach out. I would love to hear more thoughts from more people on the feasibility of this approach, and any critiques of the specific tools I have chosen for my effort.
Footnotes:
Eugenia Cheng, The Joy of Abstraction: An Exploration of Math, Category Theory, and Life (Cambridge University Press, 2022), https://doi.org/10.1017/9781108769389; Tom Leinster, Basic Category Theory, Cambridge Studies in Advanced Mathematics ; 143 (Cambridge: Cambridge University Press, 2014); F. W. Lawvere, Conceptual Mathematics : a First Introduction to Categories, [Rev. ed.]. (Buffalo, NY: Buffalo Workshop Press, 1993).
Leonardo de Moura et al., “The Lean Theorem Prover (System Description),” in Automated Deduction - Cade-25 (Springer International Publishing, 2015), 378–88, https://doi.org/10.1007/978-3-319-21401-6_26.
Klaus Oberauer and Stephan Lewandowsky, “Addressing the Theory Crisis in Psychology,” Psychonomic Bulletin &Amp; Review 26, no. 5 (September 2019): 1596–1618, https://doi.org/10.3758/s13423-019-01645-2.
Paul E. Meehl, “Theoretical Risks and Tabular Asterisks: Sir Karl, Sir Ronald, and the Slow Progress of Soft Psychology.,” in The Restoration of Dialogue: Readings in the Philosophy of Clinical Psychology. (American Psychological Association, 1992), 523–55, https://doi.org/10.1037/10112-043.
Denny Borsboom et al., “Theory Construction Methodology: A Practical Framework for Building Theories in Psychology,” Perspectives on Psychological Science 16, no. 4 (February 2021): 756–66, https://doi.org/10.1177/1745691620969647.
Iris van Rooij and Giosuè Baggio, “Theory before the Test: How to Build High-Verisimilitude Explanatory Theories in Psychological Science,” Perspectives on Psychological Science, 2021, 174569162097060, https://doi.org/10.1177/1745691620970604.