@flawr The Curry-Howard correspondence associates types with logical statements and terms with proofs. For example, the type (.) :: (b -> c) -> (a -> b) -> (a -> c) corresponds to the logical statement ∀A,B,C. (B → C) → ((A → B) → (A → C)).

The problem is that bottoms let you "prove" any time. For example, undefined = undefined has the type a, which corresponds to ∀A. A, a logical statement which is obviously not true. The simplest way to resolve this problem is to ban unrestricted recursion, which typically entails a totality checker that only permits recursion in certain circumstances so as to guarantee that functions will always halt.

If you choose a different system of logic for your type system, you will end up with a different type system. For example, affine logic corresponds to an affine type system (like that of Rust) where (most) values cannot be used twice. The problem I described earlier is only really a problem if you use a logic in which a single inconsistency makes everything explode.

However, there are logics which permit some contradictory statements without permitting everything; these are called paraconsistent logics. My question was whether such logics could be used for a "paraconsistent type system" that would permit some nonterminating programs.

@EsolangingFruit oh that is intersting.

@EsolangingFruit Thanks for this really well written explanation!!