Fork me on GitHub
Drew Verlee05:02:00

Also, philosophically speaking, correctness isn't a property of types, but of ... <waves hands>...

Colin P. Hill13:02:14

What's the difference between a type system and a predicate value system? If a type is a set of values, and a set can be defined by a membership predicate, then it seems like these are the same thing implemented in different ways

Ben Sless18:02:04

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

Ben Sless18:02:11

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

Colin P. Hill14:02:27

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".

Colin P. Hill14:02:46

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.

Colin P. Hill14:02:47

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.

Ben Sless14:02:15

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

Colin P. Hill14:02:42

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?

Ben Sless14:02:44

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

Ben Sless14:02:17

Maybe predicate types will be the first

Ben Sless14:02:30

Maybe you can reduce them to another system

Colin P. Hill15:02:00

The existence of this paper would suggest to me that Java's type system was first built, and only later analyzed formally:

Colin P. Hill15:02:08

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)

Ben Sless15:02:38

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)


> Rust's linear types were theoretical until Rust implemented them FYI there's an impl of linear types in this 1991 paper

Ben Sless06:02:44

I think linear types relate to substructural logic

Colin P. Hill17:02:53

> 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

Colin P. Hill17:02:12

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

Ben Sless17:02:06

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 🙂

Colin P. Hill19:02:04

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.

Colin P. Hill19:02:49

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.

Colin P. Hill13:02:53

Heck, some of the core predicates are type checks, just at runtime


This conversation seems like it's going to open Pandora's box: