<p>In total dependently typed languages, general recursion is forbidden, since this can allow for non-terimination. However, dependently typed language can still <em>describe</em> Turing-complete computations (without running them), <a href="https://strathprints.strath.ac.uk/60166/1/McBride_LNCS2015_Turing_completeness_totally_free.pdf" rel="nofollow noreferrer">using free monads</a> (see also <a href="http://adam.chlipala.net/cpdt/html/GeneralRec.html" rel="nofollow noreferrer">here</a>).</p>

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

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

CC BY-SA 4.0
2020-01-23T09:21:31.630Z
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.
Blaisorblade
CC BY-SA 4.0
2020-01-23T09:28:15.377Z
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 https://cs.au.dk/~birke/papers/pcf-in-s.pdf.
Blaisorblade
CC BY-SA 4.0
2020-01-23T09:46:05.920Z
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.
Andrej Bauer
CC BY-SA 4.0
2020-01-26T04:20:47.033Z
@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.
Joey Eremondi
CC BY-SA 4.0
2020-01-26T18:08:27.200Z
Just throw in recursive types and be done with it.
Andrej Bauer
CC BY-SA 4.0
2020-01-27T06:57:12.887Z
Are you planning to use $\mathsf{Set} : \mathsf{Set}$ as a source of general recursion? Or are you more interested in being able to formulate unrestricted recursions? If the former, that's weird, if the lattter, the most direct way to do that is to have recursive types.
Andrej Bauer
CC BY-SA 4.0
2020-01-27T16:08:16.310Z
@AndrejBauer it's more that I'm trying to give semantics to a language with Set:Set (or something like it) via a shallow embedding into a static dependent typed language. I'm working with gradual types, where we don't have Set:Set but you can achieve it in sneaky ways.
Joey Eremondi
CC BY-SA 4.0
2020-01-27T17:19:08.713Z
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?
Andrej Bauer
CC BY-SA 4.0
2020-04-23T07:31:52.717Z
How about coinductive types?
ice1000
<pl.programming-languages><type-theory><lambda-calculus><type-systems><dependent-type>
Set:Set or Negative Inductives in a Total Language?
Joey Eremondi
# Set:Set or Negative Inductives in a Total Language?

(Asked by: username_0 on 2020-01-22)

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](https://strathprints.strath.ac.uk/60166/1/McBride_LNCS2015_Turing_completeness_totally_free.pdf) (see also [here](http://adam.chlipala.net/cpdt/html/GeneralRec.html)).

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?

**Tags:** pl.programming-languages, type-theory, lambda-calculus, type-systems, dependent-type
> **Comments:**
> **username_1**: 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.  
> **username_1**: 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 https://cs.au.dk/~birke/papers/pcf-in-s.pdf.  
> **username_2**: 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.  
> **username_0**: @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.  
> **username_2**: Just throw in recursive types and be done with it.  
> **username_2**: Are you planning to use $\mathsf{Set} : \mathsf{Set}$ as a source of general recursion? Or are you more interested in being able to formulate unrestricted recursions? If the former, that's weird, if the lattter, the most direct way to do that is to have recursive types.  
> **username_0**: @AndrejBauer it's more that I'm trying to give semantics to a language with Set:Set (or something like it) via a shallow embedding into a static dependent typed language. I'm working with gradual types, where we don't have Set:Set but you can achieve it in sneaky ways.  
> **username_2**: 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?  
> **username_3**: How about coinductive types?  

---

## 0 answers

