<p>Type systems are more often than not at least an important aspect in language design. A type allows abstract reasoning about a thing and by the Curry-Howard correspondence, we have that typing is similar to logic. Usually, one wants logic to be consistent, no contradiction should follow from the axioms.</p>
<p>In the <a href="https://www.xn--pdrot-bsa.fr/articles/dcbpv.pdf" rel="noreferrer">fire triangle</a> paper, the authors are arguing that a dependent type system cannot have the substitution lemma, effects, and dependent elimination at the same time without giving up consistency. This is obviously bad if you want to do mathematics in such a system.
However, is there anything that really hurts a general purpose programming language's design if its type system is not consistent?</p>

<language-design><types>
Why care about consistency?
CC BY-SA 4.0
2023-07-02T20:30:00.197Z
Perhaps a consistent language can be compiled more efficiently because proofs can be safely erased?
Labbekak
CC BY-SA 4.0
2023-05-17T00:26:20.560Z
Why the downvote? This question looks perfectly legitimate to me.
ice1000
CC BY-SA 4.0
2024-03-22T04:08:38.107Z
What is consistency in PL?
Delfin
<h1>Nothing</h1>
<p>Idris2 is a general-purpose programming language with first-class types. It is inconsistent for now.</p>
<p>Consistency is very difficult to have. You need to at least be:</p>
<ul>
<li>Turing incomplete, because general recursion proves false</li>
<li>Restrict inductive types to a strictly positive fragment, because it's otherwise inconsistent</li>
<li>Be fairly predicative, at least you can't have impredicative universe (not to even mention type-in-type). But you can have an impredicative universe of propositions.</li>
</ul>
<p>And many more. All of these impose difficulties! But we may only write <em>more</em> code without those features.</p>

CC BY-SA 4.0
2023-05-16T20:39:35.863Z
2023-05-16T20:39:35.863Z
ice1000
# Why care about consistency?
Posted by: username_0 on 2023-05-16
Type systems are more often than not at least an important aspect in language design. A type allows abstract reasoning about a thing and by the Curry-Howard correspondence, we have that typing is similar to logic. Usually, one wants logic to be consistent, no contradiction should follow from the axioms.

In the [fire triangle](https://www.xn--pdrot-bsa.fr/articles/dcbpv.pdf) paper, the authors are arguing that a dependent type system cannot have the substitution lemma, effects, and dependent elimination at the same time without giving up consistency. This is obviously bad if you want to do mathematics in such a system.
However, is there anything that really hurts a general purpose programming language's design if its type system is not consistent?
**Tags:** language-design types
> **Comments:**
> **username_2**: Why the downvote? This question looks perfectly legitimate to me.  
> **username_1**: Perhaps a consistent language can be compiled more efficiently because proofs can be safely erased?  
> **username_3**: What is consistency in PL?  
---
## 1 answers
### Answer by username_2 on 2023-05-16. Score: 8 | Accepted answer
# Nothing

Idris2 is a general-purpose programming language with first-class types. It is inconsistent for now.

Consistency is very difficult to have. You need to at least be:

* Turing incomplete, because general recursion proves false
* Restrict inductive types to a strictly positive fragment, because it's otherwise inconsistent
* Be fairly predicative, at least you can't have impredicative universe (not to even mention type-in-type). But you can have an impredicative universe of propositions.

And many more. All of these impose difficulties! But we may only write *more* code without those features.
---
