<p>Predicative foundations puts restrictions on power sets and function sets.</p>
<p>Entirely apart from the philosophy predicative theories are a lot easier to prove things about and this sounds interesting to me for type theory purposes.</p>
<p>But lots of constructs in type theory correspond to substructural logic and co-intuitionistic logic. So dually shouldn't one consider &quot;predicative coimplication&quot; as well as predicative implication?</p>
<p>I find the idea of &quot;predicative coimplication&quot; really hard to understand though.</p>
<p>So very vaguely in computer programs resource management, nondeterminism and nonlocal control flow corresponds to constructs in substructural logics and co-intuitionistic logic.</p>
<p>So one ought to have some notion of &quot;predicative exception types&quot; and &quot;predicative continuations.&quot;</p>
<p>It seems reasonable to me to have some restricted &quot;predicative&quot; notion of control flow for easier metatheory but I just have no idea what predicative control flow ought to mean.</p>

CC BY-SA 4.0
2022-03-19T08:05:58.903Z
But why do you think that "normal flow control is impredicative? Impredicativity usually involves some sort of small completeness (all small suprema, all small categorical limits). For instance, what is impredicative about exceptions?
Andrej Bauer
CC BY-SA 4.0
2022-03-19T15:01:01.057Z
@AndrejBauer my intuition would be that exceptions are restricted enough they probably aren't impredicative. You would probably want full continuations for some sort of impredicativity. But I'm not sure how to think about that.
Ms. Molly Stewart-Gallus
<type-theory><type-systems><linear-logic>
What does impredicativity mean in substructural and co-intuitionistic logics?
Ms. Molly Stewart-Gallus
# What does impredicativity mean in substructural and co-intuitionistic logics?

(Asked by: username_0 on 2022-03-18)

Predicative foundations puts restrictions on power sets and function sets.

Entirely apart from the philosophy predicative theories are a lot easier to prove things about and this sounds interesting to me for type theory purposes.

But lots of constructs in type theory correspond to substructural logic and co-intuitionistic logic. So dually shouldn't one consider "predicative coimplication" as well as predicative implication?

I find the idea of "predicative coimplication" really hard to understand though.

So very vaguely in computer programs resource management, nondeterminism and nonlocal control flow corresponds to constructs in substructural logics and co-intuitionistic logic.

So one ought to have some notion of "predicative exception types" and "predicative continuations."

It seems reasonable to me to have some restricted "predicative" notion of control flow for easier metatheory but I just have no idea what predicative control flow ought to mean.

**Tags:** type-theory, type-systems, linear-logic
> **Comments:**
> **username_1**: But why do you think that "normal flow control is impredicative? Impredicativity usually involves some sort of small completeness (all small suprema, all small categorical limits). For instance, what is impredicative about exceptions?  
> **username_0**: @AndrejBauer my intuition would be that exceptions are restricted enough they probably aren't impredicative. You would probably want full continuations for some sort of impredicativity. But I'm not sure how to think about that.  

---

## 0 answers

