3 ms·

How do type theorists distinguish Forth from PHP from Haskell without recognizing "dynamic typing" as a concept?

• Locke1689 14y ago
  Haskell is typed. The rest are not (or unityped if you're Harper).
• trhtrsh 14y ago
  They do, parent was just wrong, and ignoring the fact that people use "language" colloquially to include the operational semantics, and pretending that only denotational semantics exist. Dynamically typed languages have a typed runtime, do not a type in the static program text. Hence the commonly used correct qualifiere: "dynamic" and "static". http://research.microsoft.com/apps/pubs/default.aspx?id=67527 http://research.microsoft.com/apps/pubs/default.aspx?id=6752...
  • Locke1689 14y ago
    Please read TAPL again. 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. The word “static” is sometimes added explicitly--we speak of a “statically typed programming language,” for example--to distinguish the sorts of compile-time analyses we are considering here from the dynamic or latent typing found in languages such as Scheme (Sussman and Steele, 1975; Kelsey, Clinger, and Rees, 1998; Dybvig, 1996), where run-time type tags are used to distinguish different kinds of structures in the heap. Terms like “dynamically typed” are arguably misnomers and should probably be replaced by “dynamically checked,” but the usage is standard. Perhaps I should have been more clear that we use the words "dynamically typed" because they have entered the lexicon, but they are misnomers -- they do not properly capture what type theorists mean when they say "type".