4 ms·

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 thro

by 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
        > 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. They are semantically inaccessible, not syntactically inaccessible. These languages enforce abstractions by attaching meaning to the tags implicit to all values, and these meanings combined with the operation are what drive the next evaluation step, ie. success or raise error value. This is not what happens in typed languages. Lexical scoping is an example of a syntactic method commonly employed by dynamically typed languages. It's possibly the only one. Edit: I have both of Pierce's "Types and Programming Languages", and "Advanced Topics in Types and Programming Languages". "Dynamic typing" is mentioned exactly once, on page 2 of the first text where Pierce says: > The word "static" is sometimes added explicitly [...] to distinguish the sorts of compile-time analysis we are considering here from the dynamic or latent typing found in languages such as Scheme, where runtime type tags are used to distinguish different kinds of structures on the heap. Terms like "dynamically typed" are arguably misnomers and should probably be replaced by "dynamically checked".
        YouAreGreat 8y ago
        > semantically inaccessible, not syntactically inaccessible. You can give the semantics of everything that happens in a safe d-t language in terms of church encoded tag-value pairs and yet the programmer can't break the abstraction because abstraction-breaking operations are syntactically unavailable. It should count as testament to the success of dynamic typing that the abstractions are so safely enforced that you can squint and suddenly the whole language is semantically founded on them.

by igouy 8y ago

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
      > 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. They are semantically inaccessible, not syntactically inaccessible. These languages enforce abstractions by attaching meaning to the tags implicit to all values, and these meanings combined with the operation are what drive the next evaluation step, ie. success or raise error value. This is not what happens in typed languages. Lexical scoping is an example of a syntactic method commonly employed by dynamically typed languages. It's possibly the only one. Edit: I have both of Pierce's "Types and Programming Languages", and "Advanced Topics in Types and Programming Languages". "Dynamic typing" is mentioned exactly once, on page 2 of the first text where Pierce says: > The word "static" is sometimes added explicitly [...] to distinguish the sorts of compile-time analysis we are considering here from the dynamic or latent typing found in languages such as Scheme, where runtime type tags are used to distinguish different kinds of structures on the heap. Terms like "dynamically typed" are arguably misnomers and should probably be replaced by "dynamically checked".
      - YouAreGreat 8y ago
        > semantically inaccessible, not syntactically inaccessible. You can give the semantics of everything that happens in a safe d-t language in terms of church encoded tag-value pairs and yet the programmer can't break the abstraction because abstraction-breaking operations are syntactically unavailable. It should count as testament to the success of dynamic typing that the abstractions are so safely enforced that you can squint and suddenly the whole language is semantically founded on them.