It's not about what the types themselves are, it's about how they relate to the rest of the program. A type is something associated with terms (roughly, expressions) in a language - you have to have rules for assigning types to every term, or to put it another way you have to exclude terms that you can't type from your language. So saying 2 is of type integer and + is of type integer -> integer -> integer is a start, but for those to be types you need to be able to say that (2 + 2) is of type integer, not just that 4 is of type integer once you've evaluated it.
Unless you replace is with can, you're just spewing dogma, not computer science.
Under a particular paradigm, we can choose to associate types with the nodes in the program's abstract syntax tree, and to have types nowhere else. Then within that paradigm, when we say type, we refer to information attached only to the nodes in the program, and nowhere else.
While that is valid, it doesn't speak to everything that type is or can be.
Even, say, the .jpeg suffix on a file is a type, in a certain context.
Words have to mean something if we're to communicate at all.
> Under a particular paradigm, we can choose to associate types with the nodes in the program's abstract syntax tree, and to have types nowhere else. Then within that paradigm, when we say type, we refer to information attached only to the nodes in the program, and nowhere else.
This stuff predates programming, it goes back to formal language research. That's what type means! If you want to mean something else you should say something else.
Oh? Which ones?
I believe I can fix that, but I can't make a move without a repro test case.
If the language was able to reliably check types, surely they would express that as an actual language feature. If the language creators don't trust their type system enough to call it a type system (and regard any uncaught error as a bug) then why should any mere user do so?
The soundness question is different to the checking ahead of time question but the two are usually conflated under the name "type system".
That's memory safety, a valuable property but nothing to do with types. If you have a sound type system then you can use that as part of your language's memory safety strategy, but that's not the only way to accomplish that.
> The soundness question is different to the checking ahead of time question but the two are usually conflated under the name "type system".
Misusing "type system" to talk about something that checks some runtime property of values is sadly common, but hopefully HN can rise about such muddled thinking.
The runtime property of values being checked by the "type system" is the "type" of the value. Something like "you're adding a number to a list, error". Where 'a number' means 'is an element of the set of numbers', possibly defined implicitly by a predicate or possibly explicitly by an enumeration of elements of that set.
When the error is reported (e.g. 'compile time' for some phase separation thing) is one property, which errors are detected is a different one. You could define "type" as compile time detection of syntactic errors, with some hand waving around what errors are, but that's not the only useful definition.
For concrete examples, lisp and python have similar type systems, and forth and assembly have similar type systems, but python's one isn't very similar to assembly. SML is a different thing again. They all have constraints on values that can occur in various contexts.
The system you're describing sounds rather unlike a type system, but in any case it's certainly not what a given lisp implementation is using at compile time, which was the original context of this dicussion. The thing that is being used at compile time in the original comment is almost certainly a type system (because at compile time one has the expression tree, especially in a lisp, and one needs information that there is no other reasonable way of determining); having a quite different thing called a "type system" only adds to the programmer's confusion when trying to understand what the thing that is being done at compile time does and doesn't guarantee.
A static type system associates the syntactic nodes in a program with type.
A dynamic type system associates run-time objects with a type.
I don't see what is so difficult.
It's all objects anyway: in a static compiler, the terms are objects, and get associated with a type. The program graph or tree is dynamically typed while inside the compiler.
The terms of a dynamically typed program can be identified as having type, and diagnosed as well as optimized accordingly. Just if that analysis is incomplete, the program can be compiled and executed anyway, with the safety net of dynamic typing catching whatever hadn't been diagnosed. (Or even what had been, in cases when the diagnostics are warnings.)
No? This is getting into implementation details, but the compiler will need to form a typed AST at least once in order to typecheck the program (technically we can consider that part of the parsing stage - as you say, it's syntactic in a sense - but either way it has to be done), and will generally keep it in that form for at least some of the analysis stages; like any other program you can do this in a more or less typesafe representation (e.g. maybe you allow a function call node to have any kind of children, but you make it easier for yourself if you represent that only callable things can be called). Of course it eventually needs to be lowered into executable form, but that can happen quite late in the process.
> The terms of a dynamically typed program can be identified as having type, and diagnosed as well as optimized accordingly. Just if that analysis is incomplete, the program can be compiled and executed anyway
But you have to actually represent that in the compiler somehow! Your "analysis is incomplete" AST nodes still have to be compiled, and whatever checking/diagnostics you're doing still has to run on them. So there will be a type (in the true sense, something associated with terms in your language) that your compiler ascribes to them, your compiler really does have a type system that it's using when analysing programs - it's just that this type system is not visible or accessible to you, and is confusingly almost-but-not-quite the same as the "dynamic type" system that your language also has.
No, it isn't. It's safety of the kind which asserts that a value of a certain type can only be operated on by suitably typed functions and operators.
The underlying memory may be safe either way: with or without the bad type punning. E.g. if a fixnum integer were treated as a character, that wouldn't be a memory problem, since they aren't heap allocated and both occupy a valid cell of the same size.
All type safety is "bit safety" at the implementation level, because in the actual semantics of the running program, objects are represented by bits, and type safety ultimately prevents bits intended to be interpreted and used one way as being used in a different way.
Memory safety is related to type safety because bits can represent pointers, and pointers can be valid or invalid, or point to objects of only so many bytes and no more.
All type checks related to pointers are providing some measure of memory safety, because if we use a non-pointer object as a pointer, or an object of one size as an object of a different size (all of which are type mismatch errors), we may end up with corruption or a crash.
Nope. Programs can be interpreted by humans, or by non-bit-based mechanical computers. Type safety can be used to enforce a wide range of properties you might want, which don't necessarily have any connection with "how bits are interpreted" beyond the trivial sense in which that's true of everything you can say about a program.
Diagnostics which have not been made requirements in a language, and are therefore not implemented, indeed cannot be relied upon to be there, and we can write test cases which show that some situations would benefit from those diagnostics (all else being equal, which it usually isn't). Under TDD, we can write a test case that fails for something that is not implemented and not a requirement (but about to become one).
That's a different claim though.
I am saying that. You can't rely on something that's not part of the specification (formal or otherwise). If I call an unknown function and f(2, 3) = 5 and f(7, 8) = 15, I would still be crazy to trust that f is the plus function if it wasn't actually documented or specified as such, even if I haven't come up with a concrete test case where it isn't yet.
Bullshit. Either it's a sound type system (perhaps with some escape hatches) - in which case why would you ever not expose it as a real static type system - or it's not and you can't rely on it.
(There is no contradiction between having good inference and having a real static type system; e.g. if you're using Hindley-Milner then you have "perfect" type inference where you could remove all the type annotations from your program and it will still be correctly typed. But it's still very useful to have a syntax for annotating expressions with their types!)
And of course if you really want an ML style BDSM type system in Common Lisp there's Coalton[1].
Then they're not types. Types go on terms, i.e. expressions, not on values.
> This presents some code generation challenges, but it will warn on correctness just fine.
Warn on correctness it may, but it's simply impossible for a setup like that to reliably error on incorrectness at compile time; a Turing-complete language like Common Lisp cannot determine any nontrivial property of expressions (in a way that works in all cases) without evaluating them. If your types go with your values then you can't check your types without evaluating your values, at which point compile time is long gone.