3
$\begingroup$

In total dependently typed languages, general recursion is forbidden, since this can allow for non-terimination. However, dependently typed language can still describe Turing-complete computations (without running them), using free monads (see also here).

However, recursion is not the only source of non-termination in dependently typed languages. Having $Set : Set$ allows for Girard's paradox, inductive data types must be strictly positive, since otherwise we can write an interpreter for the untyped lambda calculus.

I'm wondering, is there an equivalent of the General Recursion monad for describing (but not running) computations involving $Set : Set$ or non-strictly positive data types? Or is there a way that we can express these in terms of a general-recursion monad?

Improve this question
$\endgroup$
9
  • 2
    $\begingroup$ Everything else is true, but I proposed an edit from “simply-typed” to untyped: a interpreter for STLC (that is, without added fixpoints) is entirely fine, the problem is untyped LC. $\endgroup$
    – Blaisorblade
    Jan 23 '20 at 9:21
  • 1
    $\begingroup$ On the actual question: non-strictly positive datatypes can be encoded by solving “recursive domain equations” in either the category of domains, or a “new” technique called the category of OFEs / topos of trees / step-indexing / guarded type theory, worked on mostly by Birkedal. An example is cs.au.dk/~birke/papers/pcf-in-s.pdf. $\endgroup$
    – Blaisorblade
    Jan 23 '20 at 9:28
  • 1
    $\begingroup$ Can you be a bit more precise about which monad you have in mind when you say the "General Recursion monad"? As for set-in-set, that would be easier to tackle if you write it out in terms of Tarski universes, instead of Russell universes. $\endgroup$
    – Andrej Bauer
    Jan 23 '20 at 9:46
  • $\begingroup$ @AndrejBauer I'm thinking of something like from the McBride paper, but I'm open to anything, really. I'm just looking for a way to describe (potentially) infinite computations, where the source of divergence is either negative inductive types or Girard's paradox. $\endgroup$
    – jmite
    Jan 26 '20 at 4:20
  • 1
    $\begingroup$ The models which support $\mathsf{Set} : \mathsf{Set}$ that I know of also support solutions to recursive domain equations, and so recursive types as well. What are these sneaky ways? How do you know you don't have a trivial model? $\endgroup$
    – Andrej Bauer
    Jan 27 '20 at 17:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.