The core predicates are, but can you represent in a type system a sorted collection? Represent constraints such as "the index keys set must be equal to the set of values associated with this key for all records"? Predicates are way looser, you'll have to work hard to formalize an entire type system around them

If Phil Wadler and his friends are right, type systems are logic systems. Find a logic system that is predicative and you've found the appropriate type system

I can represent in a type system a sorted collection – if the type system is implemented with predicates! That is to say, the distinction you're drawing seems to beg the question: if predicative systems count as type systems, then the answer to your question is trivially "yes".

Static type checkers are always developing new capabilities. Dependent and refinement types are an area of active research, and Rust's linear types were theoretical until Rust implemented them. Before these implementations, it still would have been correct to describe those ideas abstractly and call them type systems.

Similarly, coherent models which lack a total formalization, like runtime predicate checks, might also reasonably be called type systems, just as a statically typed language built without a theoretical model in mind already has a type system waiting to be described.

I'm asking a different question - what is the logic system which corresponds to predicative types. There is some calculus associated with it. The realization type systems correspond to a logical calculus system (such as lambda calculus) takes it far from type checkers. There is a formal theory there waiting to be discovered

I don't really know what logic system would correspond to it, but I'm not sure why we would need an answer to that question. We've had plenty of type systems whose formal theories were only developed after the implementations, haven't we?

I don't think so. These developments have sometimes been independent and later converged under the same name, see HM type system, one logician one computer scientists. The field of logic, being less constrained, usually develops these first, but it is not a strict requirement

Maybe predicate types will be the first

Maybe you can reduce them to another system

The existence of this paper would suggest to me that Java's type system was first built, and only later analyzed formally: https://www.researchgate.net/publication/220299005_A_Formal_Type_System_for_Java

A skim suggests to me that, as of that paper's publication, the formal analysis work wasn't even yet complete (but I might be wrong about that)

I'm drawing a distinction between a specific type system implementation, a theoretical type system, and a logic system. Could be that formal analysis was applied to Java's type system after it was written, but it must have corresponded to an existing logical system (or a yet undiscovered one) https://www.youtube.com/watch?v=IOiZatlZtGU

> Rust's linear types were theoretical until Rust implemented them FYI there's an impl of linear types in this 1991 paper https://www.cs.utexas.edu/users/hunt/research/hash-cons/hash-cons-papers/BakerLinearLisp.pdf

I think linear types relate to substructural logic https://en.m.wikipedia.org/wiki/Substructural_logic

> FYI there's an impl of linear types in this 1991 paper I stand corrected! But I think my point is still valid, and I hope it's still clear

> Could be that formal analysis was applied to Java's type system after it was written, but it must have corresponded to an existing logical system (or a yet undiscovered one) That last parenthetical note makes all the difference, imo. It means that one does not need to point to a known equivalent logical system to be able to say that something is a type system.

The idea underlying this is that there isn't a sound type system that doesn't have a corresponding logical system. You either find the one which already maps on to it, or discover a new one 🙂

Well hold on, adding sound as a qualifier changes everything 😆 Plenty of real-life type systems have been unsound, and have in some cases even been useful despite that.

Which is why I don't think the question of logic systems bears upon my original question. Something can fail to correspond to any known logical system, or even be found to be unsound when you try to formalize it, while still being a type system.

http://lambda-the-ultimate.org/node/412