3 ms·

An alternate viewpoint is that static typing advocates invented a novel categorization that allows them to dismiss typing systems they disagree with. "Tag" does

by djur 12y ago

An alternate viewpoint is that static typing advocates invented a novel categorization that allows them to dismiss typing systems they disagree with. "Tag" doesn't have a consistent theory meaning "type determined at runtime"; on the other hand, "type determined at runtime" has been referred to simply as a "type" for decades.

eli_gottlieb 12y ago
The first type theories by Russell and Church were invented decades before practical computers allowed for programming languages high-level enough to even speak of their being typed or untyped. Type theory is primarily a constructive/computational foundation for mathematics, and secondarily a way of statically proving that programs will not exhibit undefined behavior.
- tel 12y ago
  (I find it tremendously amusing when people think that computer languages invented types instead of participated in a late-set convergent evolution with type theory.)
  - seanmcdirmid 12y ago
    Type is such a generic word though. You can use the word just by its basic definition (a category of people or things having common characteristics) and everyone would mostly understand what you are talking about. What Russell invented was a theory with types of a more formal definition.
    - tel 12y ago
      So is "force" and its basic definition has been well-understood for far longer than its precise definition. But for anyone practicing anywhere near physics you ought to learn and recognize the formalization. People reinvent it all the time, to varying degrees of validity, but it's fairly clear how to draw all of this back to Newton and then connect it to the mainline formal development which has occurred since then.
jroesch 12y ago
This is flat out not true. In the academic literature of type theory, "type" has a very particular meaning and is a construct for reasoning about programs before execution. The community may use "tag" but mostly as a means of distinguishing between "types" in type theory, and a runtime tag. Often the term "dynamic type", or "runtime type" will be used as well all as means of differentiation.

by djur 12y ago

eli_gottlieb 12y ago

The first type theories by Russell and Church were invented decades before practical computers allowed for programming languages high-level enough to even speak of their being typed or untyped. Type theory is primarily a constructive/computational foundation for mathematics, and secondarily a way of statically proving that programs will not exhibit undefined behavior.

tel 12y ago
(I find it tremendously amusing when people think that computer languages invented types instead of participated in a late-set convergent evolution with type theory.)
- seanmcdirmid 12y ago
  Type is such a generic word though. You can use the word just by its basic definition (a category of people or things having common characteristics) and everyone would mostly understand what you are talking about. What Russell invented was a theory with types of a more formal definition.
  - tel 12y ago
    So is "force" and its basic definition has been well-understood for far longer than its precise definition. But for anyone practicing anywhere near physics you ought to learn and recognize the formalization. People reinvent it all the time, to varying degrees of validity, but it's fairly clear how to draw all of this back to Newton and then connect it to the mainline formal development which has occurred since then.

jroesch 12y ago

This is flat out not true. In the academic literature of type theory, "type" has a very particular meaning and is a construct for reasoning about programs before execution. The community may use "tag" but mostly as a means of distinguishing between "types" in type theory, and a runtime tag. Often the term "dynamic type", or "runtime type" will be used as well all as means of differentiation.