Loose set of thoughts: 1. could you make a type system that somehow captures all information possible about every value in a codebase? Like where the following is true: if typeof(a) === number, then typeof(a + 1 + 2) === number+3 !== typeof(a) … 2. I might want to “pin” and “unpin” my types - e.g. before refactoring a function, to “pin” its return type. If I had a more powerful type system like described in part one, I wouldn’t want to have to write out the whole type, I would want to just say “pin this such that whatever changes I make could not possibly effect the outcome of the function for any input, or else give me errors describing exactly what part of the input space no longer maps logically the same to the output space” 3. Another way to think of this might be to say, rather than writing tests, to be able to say “assume infinite test coverage of this codebase (and all tests are passing), now let me refactor things”. 4. I have no idea how this would work, but it makes me think of getting fractions into “simplest form”. Maybe you could get two functions into “simplest form” to test their similarity? I wonder if anything like that exists, or if this is gesturing at some existing area of research?

Some pointers which may (or may not) relate to your interests here… re #1: Dependently typed languages let you put a ton of information about a value into its type. For instance, in Idris you can have a type

Vect n a

meaning “a vector of n elements of type a”, and then you can write an “append” function with type

Vect n a -> Vect m a -> Vect (n + m) a

. Using functions like this, you propagate information about the lengths of vectors as you perform computations on them. re #2: Neat idea. This may be less ambitious than you’re thinking, but I can imagine an IDE feature saying “turn the inferred type of this value into an explicit type annotation”. That way, you can make types explicit before a refactor to make sure you’re not changing types as you refactor. re all: Your interests here seem related to software verification and other “formal methods”. In case you haven’t seen that stuff, I’d suggest Dafny as an accessible starting point. It lets you write functions accompanied by logical specifications the functions are supposed to satisfy, and then to guide the system to proving that the functions satisfy these specifications. (Most systems like this cannot be automated in the same way that type inference is automated, because once you want to prove general properties of programs like “functions f and g do the same thing”, you get into things that are not computable in principle.)

Adjacent to this: There's even an extension of dependent typing, called quantitative typing that let's you track how many times (0,1 or more) a value has been consumed. Idris2 uses this: https://idris2.readthedocs.io/en/latest/tutorial/multiplicities.html

a type system that somehow captures all information possible about every value in a codebase

First thought: "all possible information" about a value includes the value itself. And then you quickly get to dependent types, as @Joshua Horowitz suggested. A more difficult problem is exploiting all that information in a useful way, i.e. come up with useful inference rules. I doubt that a single set of rules, i.e. a single type system, can capture all useful inferences while remaining usable. Unfortunately, the dogma of "thou shalt not have any type system other than the one of your one and only programming language" is rarely challenged.

It's certainly something people have thought a bit about. Once you step back far enough, you're really just talking about functions that take programs as input. So a type checker is one example, a compiler is another, or an interpreter, a partial evaluator. What makes some of these kinds of function feel more like typing as compared to execution? As examples: • On the execution side, we're usually concerned with concrete values. • On the typing side, we are usually interested in what will happen in both branches of a conditional. There's all kinds of fun to be had from playing in the middle: unification, nondeterminism, and so one.

Thank you all for the pointers! @Joshua Horowitz I agree being able to toggle making an inferred type explicit would be nice and not too hard - I wonder also whether it could be nice to have some kind of UI for “scrubbing through inferred type-space” for a particular value, rather than just a binary operation. @wtaysom I had not really thought of the “function that take programs as input” classification. That makes a lot of sense! To restate what you said for my own understanding, type systems try to execute the whole input space at once and represent a flow of possibilities through the program (across all branches), rather than concrete values and single execution paths. I am reading the docs on Idris2 now and it is really fascinating what you can do with dependent types. This is a tangent, but recently I came across the ideas of provably safe AI, such as expressed in this paper. My understanding is that this is an overlapping area of research, where the goal is to take a model that includes an AI system and its environment, and to make provable claims about the outcomes of such a system when given a distribution of input conditions. I’m very intrigued by the idea that language design, and specifically user interfaces to languages, could be useful for steering AI systems, and one of my goals right now is to learn more of the fundamentals to that whole problem space. Anyways I appreciate all of your responses 🙂

The other important thing about type systems is that they do let you ignore some details.

I know you mentioned the type system, but on the runtime side, I’ve heard that the AI code editor, Cursor, has some experimental work with a runtime package called

cursor/debug

mentioned in this post. Then, the work on replay.io is pretty interesting.