4 ms·

Untyped computation in the academic sense you refer to is untyped in the sense of Forth and assembler. The untyped lambda calculus doesn't even have numbers. P

Untyped computation in the academic sense you refer to is untyped in the sense of Forth and assembler. The untyped lambda calculus doesn't even have numbers. Pragmatically, a language in which type errors occur is a typed language. Nor does it make sense to conflate "typed and untyped" with "statically typed and dynamically typed". These are simply very different things. Julia is an example of a dynamically typed language with a quite sophisticated type system and pervasive use of type annotations, it would be insane to call it untyped. Typescript is an example of a dynamic language which is nonetheless statically typed: because type errors in Typescript prevent the program from compiling, they're part of the static analysis of the program, not part of its dynamic runtime. The fact that it's uncommon to use untyped languages now is not a good reason to start describing certain type systems as 'untyped'! A good term for a language like annotation-free Python is unityped: it definitely has a (dynamic) type system, but the type of all variables and parameters is "any". Using this term involves typing one extra letter, and the payoff is you get to make a correct statement rather than one which is wrong. I think that's a worthwhile tradeoff.

lolinder 2y ago
From Benjamin Pierce's Types and Programming Languages, which is basically the definitive work on types: > A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute. And later on: > A type system can be regarded as calculating a kind of static approximation to the runtime behaviors of the terms in a program. ... Terms like "dynamically typed" are arguably misnomers and should probably be replaced by "dynamically checked," but the usage is standard. The definitions you're using are the ones that he identifies as "arguably misnomers" but "standard". That is, they're fine as colloquial definitions but they are not the ones used in academic works. Academically speaking, a type system is a method of statically approximating the behavior of a computer program in order to rule out certain classes of behavior. Dynamic checks do not count. As I've said elsewhere, I don't have a problem with people using the colloquial definitions. I do have a problem with people actively correcting someone who's using the more correct academic definitions. We should have both sets in our lexicons and be understanding when someone uses one versus the other.
- samatman 2y ago
  Benjamin Pierce is entitled to his opinion, which you have posted over and over as though it were carved upon stone tablets. "One guy says that dynamic typing is arguably a misnomer" is not a strong case. The Wikipedia article on type systems is well sourced and fairly well written: https://en.wikipedia.org/wiki/Type_system https://en.wikipedia.org/wiki/Type_system It has this section: https://en.wikipedia.org/wiki/Type_system#Dynamic_type_checking_and_runtime_type_information https://en.wikipedia.org/wiki/Type_system#Dynamic_type_check... Here's a pull quote: > Dynamic type checking is the process of verifying the type safety of a program at runtime. Implementations of dynamically type-checked languages generally associate each runtime object with a type tag (i.e., a reference to a type) containing its type information. This accords with ordinary usage in the profession, agreeing with the person you're disagreeing with. You should read it. It provides no support at all for the argument that Python is untyped in any sense. It quotes Pierce several times, including the first citation, so it isn't ignorance on the editor's part. You are advancing the argument that type theory, as you understand it (there being many paper-publishing respectable academics who do not agree with you on this), trumps type systems in practice, but other than insistence you give no reason why anyone should agree with this premise. Computer scientists aren't discovering laws of nature, nor are they writing proscriptive regulations as to how engineering should be accomplished or discussed. They have their own world and vocabulary to go along with it, but they do not have standing (as you do not) to dictate how terms should be used by others. I don't accept that argument. If someone wants to make a narrower statement like "according to Pierce you could call Python untyped" I might question its relevance but I'd let it pass. Without such qualification, if someone says Python is untyped I will laugh at them and say "what's it doing when it throws a TypeError then, offering an opinion?". Or on a message board just reply that, no, it's dynamically typed, or unityped if you must, but untyped means something else. Which, indeed, it does.
  - intalentive 2y ago
    After taking a programming languages course I came away with the impression that Python is untyped. Type annotations are not required or enforced, and expression types are not evaluated prior to execution. So here’s another vote for the academics.

lolinder 2y ago

From Benjamin Pierce's Types and Programming Languages, which is basically the definitive work on types: > A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute. And later on: > A type system can be regarded as calculating a kind of static approximation to the runtime behaviors of the terms in a program. ... Terms like "dynamically typed" are arguably misnomers and should probably be replaced by "dynamically checked," but the usage is standard. The definitions you're using are the ones that he identifies as "arguably misnomers" but "standard". That is, they're fine as colloquial definitions but they are not the ones used in academic works. Academically speaking, a type system is a method of statically approximating the behavior of a computer program in order to rule out certain classes of behavior. Dynamic checks do not count. As I've said elsewhere, I don't have a problem with people using the colloquial definitions. I do have a problem with people actively correcting someone who's using the more correct academic definitions. We should have both sets in our lexicons and be understanding when someone uses one versus the other.

samatman 2y ago
Benjamin Pierce is entitled to his opinion, which you have posted over and over as though it were carved upon stone tablets. "One guy says that dynamic typing is arguably a misnomer" is not a strong case. The Wikipedia article on type systems is well sourced and fairly well written: https://en.wikipedia.org/wiki/Type_system https://en.wikipedia.org/wiki/Type_system It has this section: https://en.wikipedia.org/wiki/Type_system#Dynamic_type_checking_and_runtime_type_information https://en.wikipedia.org/wiki/Type_system#Dynamic_type_check... Here's a pull quote: > Dynamic type checking is the process of verifying the type safety of a program at runtime. Implementations of dynamically type-checked languages generally associate each runtime object with a type tag (i.e., a reference to a type) containing its type information. This accords with ordinary usage in the profession, agreeing with the person you're disagreeing with. You should read it. It provides no support at all for the argument that Python is untyped in any sense. It quotes Pierce several times, including the first citation, so it isn't ignorance on the editor's part. You are advancing the argument that type theory, as you understand it (there being many paper-publishing respectable academics who do not agree with you on this), trumps type systems in practice, but other than insistence you give no reason why anyone should agree with this premise. Computer scientists aren't discovering laws of nature, nor are they writing proscriptive regulations as to how engineering should be accomplished or discussed. They have their own world and vocabulary to go along with it, but they do not have standing (as you do not) to dictate how terms should be used by others. I don't accept that argument. If someone wants to make a narrower statement like "according to Pierce you could call Python untyped" I might question its relevance but I'd let it pass. Without such qualification, if someone says Python is untyped I will laugh at them and say "what's it doing when it throws a TypeError then, offering an opinion?". Or on a message board just reply that, no, it's dynamically typed, or unityped if you must, but untyped means something else. Which, indeed, it does.
- intalentive 2y ago
  After taking a programming languages course I came away with the impression that Python is untyped. Type annotations are not required or enforced, and expression types are not evaluated prior to execution. So here’s another vote for the academics.