4 ms·

Surely the meaningful distinction between BCPL and Scheme is that BCPL is not type safe and Scheme is type safe.

by igouy 8y ago

naasking 8y ago
I disagree. "Type safety" is not the only kind of safety, and it's not the kind of safety found in either Scheme or BCPL.
- igouy 8y ago
  > "Type safety" is not the only kind of safety Never said it was. "Type safety is the property that no primitive operation ever applies to values of the wrong type." I did say "BCPL is not type safe" (so on that we agree). Are you saying that, in Scheme, primitive operations can be applied to values of the wrong type? A string can be multiplied by 2?
  - naasking 8y ago
    > Are you saying that, in Scheme, primitive operations can be applied to values of the wrong type? Yes, that's a well-defined operation: it throws a runtime exception (which is also a value). All operations are well-defined in safe languages, that's what makes them safe. But dynamically "typed" languages aren't type safe. A truly undefined operation would immediately halt the program because the program simply cannot proceed. You can resolve this unsafety by defining semantics for these operations (like reifying errors as values as in dynamically typed languages), or you can add a type system which ensures only safe programs can be expressed.
    - igouy 8y ago
      You say "Yes" "primitive operations can be applied to values of the wrong type", but then you say that doesn't happen and what actually happens is that "it throws a runtime exception". What you seem to mean is that isn't what I (`naasking`) would call type safety. That may be. However, it clearly has been a text-book meaning of type safety.
      - naasking 8y ago
        > You say "Yes" "primitive operations can be applied to values of the wrong type", but then you say that doesn't happen and what actually happens is that "it throws a runtime exception". Because that's not a different type. It's the same (sum) type just with a different tag. > What you seem to mean is that isn't what I (`naasking`) would call type safety. [...] However, it clearly has been a text-book meaning of type safety. No, it's not.
        igouy 8y ago
        > It's the same (sum) type just with a different tag. Now it's — that isn't what I (`naasking`) would call a type. > No, it's not. page 263 "Programming Languages: Application and Interpretation" Shriram Krishnamurthi 2003
        naasking 8y ago
        A quote divorced from context is meaningless. Here's one too: "A type system is a syntactic method for enforcing levels of abstraction in programs. " [1] What syntactic methods are used in dynamically "typed" languages? The point of a technical term is to make distinctions. As I already explained, adding safety has at least two distinct approaches: ensure unsafe programs have no meaning, or ensuring every program has meaning by reifying unsafe expressions as values. These are clearly completely different approaches, and "type" has always meant the former from its inception as a solution to Russell's paradox. The fact that dynamic typing has some superficial similarities is completely irrelevant. Types can enforce properties that no dynamic "typing" can ever achieve. [1] https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/
        YouAreGreat 8y ago
        > "A type system is a syntactic method for enforcing levels of abstraction in programs. " [1] > What syntactic methods are used in dynamically "typed" languages? Interesting. You may have unwittingly provided one of the best justifications for the term "dynamically typed" I've seen so far. That's because operations that violate a (safe) dynamically typed language's chosen set of abstractions (built using bits, church encoding, whatever) are syntactically inaccessible.
    - naasking 8y ago
      I should clarify that dynamically typed languages are type safe in the trivial sense that they satisfy unityped type safety. What I meant is that they are not type safe by virtue of what they call types, in the sense that is used by non-unityped languages.

Surely the meaningful distinction between BCPL and Scheme is that BCPL is not type safe and Scheme is type safe.

by igouy 8y ago

Surely the meaningful distinction between BCPL and Scheme is that BCPL is not type safe and Scheme is type safe.

I disagree. "Type safety" is not the only kind of safety, and it's not the kind of safety found in either Scheme or BCPL.

igouy 8y ago
> "Type safety" is not the only kind of safety Never said it was. "Type safety is the property that no primitive operation ever applies to values of the wrong type." I did say "BCPL is not type safe" (so on that we agree). Are you saying that, in Scheme, primitive operations can be applied to values of the wrong type? A string can be multiplied by 2?
- naasking 8y ago
  > Are you saying that, in Scheme, primitive operations can be applied to values of the wrong type? Yes, that's a well-defined operation: it throws a runtime exception (which is also a value). All operations are well-defined in safe languages, that's what makes them safe. But dynamically "typed" languages aren't type safe. A truly undefined operation would immediately halt the program because the program simply cannot proceed. You can resolve this unsafety by defining semantics for these operations (like reifying errors as values as in dynamically typed languages), or you can add a type system which ensures only safe programs can be expressed.
  - igouy 8y ago
    You say "Yes" "primitive operations can be applied to values of the wrong type", but then you say that doesn't happen and what actually happens is that "it throws a runtime exception". What you seem to mean is that isn't what I (`naasking`) would call type safety. That may be. However, it clearly has been a text-book meaning of type safety.
    - naasking 8y ago
      > You say "Yes" "primitive operations can be applied to values of the wrong type", but then you say that doesn't happen and what actually happens is that "it throws a runtime exception". Because that's not a different type. It's the same (sum) type just with a different tag. > What you seem to mean is that isn't what I (`naasking`) would call type safety. [...] However, it clearly has been a text-book meaning of type safety. No, it's not.
      - igouy 8y ago
        > It's the same (sum) type just with a different tag. Now it's — that isn't what I (`naasking`) would call a type. > No, it's not. page 263 "Programming Languages: Application and Interpretation" Shriram Krishnamurthi 2003
        naasking 8y ago
        A quote divorced from context is meaningless. Here's one too: "A type system is a syntactic method for enforcing levels of abstraction in programs. " [1] What syntactic methods are used in dynamically "typed" languages? The point of a technical term is to make distinctions. As I already explained, adding safety has at least two distinct approaches: ensure unsafe programs have no meaning, or ensuring every program has meaning by reifying unsafe expressions as values. These are clearly completely different approaches, and "type" has always meant the former from its inception as a solution to Russell's paradox. The fact that dynamic typing has some superficial similarities is completely irrelevant. Types can enforce properties that no dynamic "typing" can ever achieve. [1] https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/
        YouAreGreat 8y ago
        > "A type system is a syntactic method for enforcing levels of abstraction in programs. " [1] > What syntactic methods are used in dynamically "typed" languages? Interesting. You may have unwittingly provided one of the best justifications for the term "dynamically typed" I've seen so far. That's because operations that violate a (safe) dynamically typed language's chosen set of abstractions (built using bits, church encoding, whatever) are syntactically inaccessible.
  - naasking 8y ago
    I should clarify that dynamically typed languages are type safe in the trivial sense that they satisfy unityped type safety. What I meant is that they are not type safe by virtue of what they call types, in the sense that is used by non-unityped languages.