4 ms·

The lisp type systems are usually completely solid at runtime - you get errors on misuse of values, not data corruption - but the language can express construct

The lisp type systems are usually completely solid at runtime - you get errors on misuse of values, not data corruption - but the language can express constructs which are not checkable before execution, as it does not yet know whether the data it is operating on will hit type errors. The soundness question is different to the checking ahead of time question but the two are usually conflated under the name "type system".

lmm 3y ago
> The lisp type systems are usually completely solid at runtime - you get errors on misuse of values, not data corruption 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.
- JonChesterfield 3y ago
  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.
- kazinator 3y ago
  > That's memory safety, a valuable property but nothing to do with types. 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.
  - lmm 3y ago
    > 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. 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.

lmm 3y ago

> The lisp type systems are usually completely solid at runtime - you get errors on misuse of values, not data corruption 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.

JonChesterfield 3y ago
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.
kazinator 3y ago
> That's memory safety, a valuable property but nothing to do with types. 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.
- lmm 3y ago
  > 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. 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.