2 ms·

We're using different definitions for "type". Which explains the above discussion but otherwise doesn't really get us anywhere. I'd guess your "type system" is

We're using different definitions for "type". Which explains the above discussion but otherwise doesn't really get us anywhere. I'd guess your "type system" is a syntactic property of a language with strong termination properties, but you might have something else in mind. 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.

lmm 3y ago
A type system associates types to terms in a language; I wouldn't call it "syntactic" although I'm not sure what exactly you mena by that. 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.
- kazinator 3y ago
  A purely static type system is sometimes regarded as syntactic. Type errors caught without executing the code are issues of bad syntax. It's not purely context-free syntax of tokens having the right phrase structure rules; it's an enhanced syntax in which syntactic nodes of the program have type terms. Type terms are also just syntax. E.g. (array 100 int) is compatible with another (array 100 int) by comparing syntax, the same way that we could tell that (add x y) and (add x y) are the same syntax. 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.)
  - lmm 3y ago
    > The program graph or tree is dynamically typed while inside the compiler. 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.

lmm 3y ago

A type system associates types to terms in a language; I wouldn't call it "syntactic" although I'm not sure what exactly you mena by that. 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.

kazinator 3y ago
A purely static type system is sometimes regarded as syntactic. Type errors caught without executing the code are issues of bad syntax. It's not purely context-free syntax of tokens having the right phrase structure rules; it's an enhanced syntax in which syntactic nodes of the program have type terms. Type terms are also just syntax. E.g. (array 100 int) is compatible with another (array 100 int) by comparing syntax, the same way that we could tell that (add x y) and (add x y) are the same syntax. 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.)
- lmm 3y ago
  > The program graph or tree is dynamically typed while inside the compiler. 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.