8
$\begingroup$

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 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?

$\endgroup$
3
  • 2
    $\begingroup$ Why the downvote? This question looks perfectly legitimate to me. $\endgroup$
    – ice1000
    Commented May 17, 2023 at 0:26
  • $\begingroup$ Perhaps a consistent language can be compiled more efficiently because proofs can be safely erased? $\endgroup$
    – Labbekak
    Commented Jul 2, 2023 at 20:30
  • $\begingroup$ What is consistency in PL? $\endgroup$
    – Delfin
    Commented Mar 22 at 4:08

1 Answer 1

7
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .