When analysing types statically (if that’s the right term) do you consider the values also, or is that left for run-time? What I mean is, if we have something like: (let ([int x 2]) ...) Do we try to ensure that x is indeed being bound to an integer? Or are we simply checking that the “proposed” types are correct, and if the user has in fact “lied” about the type, that will be caught at run-time? I’m a little confused because, if you had: (let ([int x (read)]) ...) without annotations of any kind for read, you can’t “check” without actually running/evaluating the program, and of course you’re not going to prompt the user for input during compilation! :wink: Do you actually evaluate things, or just work on the proposed types alone? i.e. check that the user’s intentions are consistent, and not whether the actual values the ids will be bound to match up with those intentions (until run-time).

apologies if that was a bit hard to follow; this is my first real foray into this subject.

It’s a good question. What you’re getting at is what it means for a type system to be “sound,” and there isn’t one simple answer.

A type system from ten thousand feet doesn’t strictly “do” anything… it’s a system of logical rules. The system contains axioms, like “3 has type Integer,” and inference rules, like “if a has type Integer and b has type Integer, then a + b has type Integer.” Those rules probably match your intuition of what 3 and + mean.

But a type system is “just” a system of rules, and the rules don’t necessarily have to be intuitive. For example, you could have a type system where an axiom is “3 has type String” and an inference rule is “if a has type Foo and b has type Bar, then a + b has type FooBar.”

You could implement that type system as an algorithm, and you could run it on a program. You might even get a result. But would the result mean anything? Probably not, and it certainly wouldn’t mean anything useful.

So we have a problem: we clearly think the first of those type systems is somehow “good,” while the second is somehow “bad,” but what does that actually mean precisely? Your question is getting at that idea, too, from a slightly different angle.

A good starting point would be to connect the dynamic behavior of a program with what our static analysis produces as its output. For example, we probably want to be able to say that for any expression e, if our type system says e has type String, then when we evaluate e, the result will be a string.

But you’ll find that rule is true in very few programming languages. On one end of the spectrum, there’s C, where this statement is perfectly legal: char* x = (char*)42; The type system “thinks” that x has type char*, which we interpret to mean “a pointer to a character,” but it isn’t. C is an extreme example, but other languages have other problems. For example, in TypeScript, we can cheat the typechecker in a similar way: const x: any = 42; const y: string = x; // no error Now things have gone “wrong”—the type system thinks that y has type string, but we know it holds a number.

To say that it’s that black and white would be misleading, though, since even significantly “safer” languages don’t have the “forall e. e : String implies e evaluates to a string” rule. For example, in Java, we can write: Object x = 42; String y = (String) foo; and the compiler won’t complain. But unlike the C and TypeScript examples, we’ll get a runtime error. So Java is content with allowing this kind of type unsafety at compile-time, but it enforces a rule that the type is checked at runtime.

Even in Haskell, which has a pretty robust type system, relatively speaking, it’s possible to write let x :: String = error "bang" (which will crash), or even let x :: String = x (which will loop forever).

What am I getting at by saying all of this? Well, the question of what “right” thing to do is in the examples you gave doesn’t necessarily have a single answer. Lots of languages try to guarantee different things with their type systems. And different people have different definitions of what makes a type system, in their mind, “sound.” (Gradual typing also makes that question even more complicated.)

So, to summarize: type systems are “just” a set of logic rules, it’s up to you to ensure the logical rules mean what you think they mean, and it’s also up to you to decide what you want the type system to guarantee in the first place.

@lexi.lambda Thanks for the detailed response!

As painfully obvious as it sounds typing it out, I guess I just need to really think hard about what I want the type system to do/be, and try my best to implement that.

For now, I think I’ll stick with just ensuring that the programmer is consistent with what they want the types to be, and go from there. That seems like a decent starting point at least.