Monads and Logic ---------------- In a sentence, is it possible to parametrize a _logic_ by a monad just as one parametrizes a _programming language_ by a monad? If intuitionistic logic is the logic of a functional programming language with sums and products (call it FPL), what is the logic of FPL over a monad? In "Deduction and Computation" (from "Logic of Programming and Calculi of Discrete Design" ed. Broy), Gerard Huet says, "All this development concerns the so-called intuitionistic logic, where operators (inference rules) are deterministic. It is possible to generalize the inference systems to classical logic, using a generalized notion of sequent where the right part is also a _set_ of propositions. It is possible to explain the composition of such non-deterministic operators, which leads to Gentzen's systems NK and LK. ..." Huet makes it sound as though you could parametrize intuitionistic logic by a monad and use the lists monad to obtain classical logic. In Murthy's work, he uses the control operator for backtracking, so instantiating intuitionistic logic by the continuation monad should also yield classical logic, except that you would get a single value, and a continuation for more, rather than all values. In terms of programs, I suppose one could imagine an extensible theorem prover (rather than an extensible interpreter).