12 ms·

Untyped Programs Don’t Exist

45 points by gbrown_ 8y ago

porpoisely 8y ago
A couple of points. Javascript, Racket, etc that he listed aren't "untyped" languages. They are typed. Weakly/dynamically typed. Although I guess some people equate the two. So lets go with that. Also, division by zero is an runtime operation error, it is not really a type error. The division operation doesn't fail because it violated the type system, it fails because you can't mathematically divide by zero. Finally, x86 assembly doesn't really have what we call a type system in the general sense. But assuming his premises and logic, the conclusion should be "Typed Programs Don't Exist". If x86 checks its type at runtime ( division by zero ), then it is a dynamic language. Dynamic languages are untyped languages like javascript and racket. And since all programs are ultimately assembly programs and all assembly programs are created by dynamic languages then it must mean that all programs are untyped. Hence, no typed programs exist. Ultimately, the author's argument is that runtime division by zero error is proof of x86 type system. But if that is true, x86 assembly is a dynamic ( aka untyped ) language. And his conclusion is wrong.
- saagarjha 8y ago
  > Finally, x86 assembly doesn't really have what we call a type system in the general sense. I might argue that it kind of does, based on the width of the operands. For example, you can only movq a quadword–you will get a "compile error" if you try to use it on a 16-bit value.
  - firethief 8y ago
    I'm not sure encodability can usefully be considered to define x86's type system. rax can be used in places r8 can't.
    - saagarjha 8y ago
      As in, there are certain instructions that operate on rax but not r8? Maybe a more complex type system in this case where rax and r8 are specialized quadwords and certain instructions accept more specific arguments?
      - firethief 8y ago
        Every register besides r8-r15 has special functions, and different registers support different addressing operations. There are at most two pairs of equivalent registers: r8/r10 and r9/r11 (i.e. I don't know of any operation in which r8 couldn't be swapped with r10, and likewise for r9/r11). All other registers are unique (i.e., for any pair of them, there exist valid assembly programs that would become invalid if you swapped usage of the registers in that pair throughout the program). So you can define a type system isomorphic to a lot of things, but this seems to me a degenerate case. What's the point of considering it a type system when no two values can be of the same type, almost all operations are polymorphic, almost all operations are on multiple types, and almost every instruction involves a conversion between types?
  - kazinator 8y ago
    Machine instruction sets have data type systems which tend to give a well-defined meaning to type punning. If an integer is reinterpreted as a floating-point value, the meaning is precisely determined down to the last bit. Few restrictions are placed by machine instruction sets on how a datum that is written into memory by a store is later interpreted by a load, though the semantics is clear for any given value. This is better than "undefined behavior" (how C treats similar situations), because it is predictable, but it has to be identified as weak typing. We might call it "weak static typing". An assembly language program that assembles doesn't contain any undefined behavior due to misuse of type. When we assemble an instruction like "load 32 bits from the address given in R1 into R2", there is no possible type error there. In machine languages, there are other type rules at play besides just data type, and assembly languages tend to treat these poorly. For instance, whether a pointer is suitably aligned for a given access is arguably a type. It may be the case that only pointers ending in 00 (bits) have the right type for accessing a 32 bit value. However, we can assemble the "load 32 bits from [R1] into R2" instruction silently without the assembler providing any type check that R1 contains a suitably aligned pointer. If we work with arrays in a typical assembly language, we don't get static bounds checks. In short, machine language programs can exhibit horrible run-time errors due to misuse of memory, which are not statically caught by assemblers, even though we can pun among different kind of operands while remaining within non-failing behavior (no exceptions raised) and well-defined results being produced.
- fao_ 8y ago
  "Also, division by zero is an runtime operation error, it is not really a type error. The division operation doesn't fail because it violated the type system, it fails because you can't mathematically divide by zero." Zero is a different type from the type that consists of integers above N.
  - slededit 8y ago
    Its an interesting concept. Addition or subtraction now would have to dynamically return either a zero type or a non-zero type. I suppose the type system could force you to check and handle the zero case. In reality I think it would be too cumbersome. Division by zero is a relatively rare flaw and zero agnostic math on integers is common. I'd love to hear about any languages that do this.
    - joshuamorton 8y ago
      Not necessarily, additional and subtraction just return int, but you can define other operations over subsets of ints that return nonzero. Rust does something similar, floats by default can be NaN, but you can write a non-NaN float that just panics if it's Nan and then ignore the possibility of Nan in parts of your system.
  - smadge 8y ago
    What is "the type that consists of integers above N?" If N = -1, then 0 is in the set of integers greater than N. I think it makes more sense to say that division is a function F × (F - {0}) → F where F is a field. F is not the same set/type as F without 0. I think in the context of computer languages this would be called a refinement type. (https://en.wikipedia.org/wiki/Refinement_type https://en.wikipedia.org/wiki/Refinement_type)
  - tremon 8y ago
    Can you show a language that implements your concept of "integers above N" consistently? I fail to see how such a type would be remotely useful in the context of addition/subtraction operators. I think Ada comes closest to your definition with allowing modular and derived integer types, but the former does include 0 and I'm not sure if the latter even allows division.
- AnaniasAnanas 8y ago
  > Also, division by zero is an runtime operation error, it is not really a type error .. in most languages. This is not universally true however. Consider a language with dependent types whose division function has a type signature like so: div : Nat -> (y : Nat) -> (y > 0) = True -> Nat, which basically requires a proof that can be verified at compile time that y is bigger than 0. In such a language you would not have a division by zero runtime error. You can even have something similar (but much more painful to use) in languages without dependent types, consider: data Nat1 = Succ Nat1 | One data Nat = CNat1 Nat1 | Zero div : Nat -> Nat1 -> Nat
  - jepler 8y ago
    Ada is an example of a standardized, mature language with a "natural number" (strictly positive integer) type.
    - tremon 8y ago
      But Ada doesn't restrict its division operators (div, mod and rem) to just "natural number" divisors.
  - josephg 8y ago
    Right. You can also think of a type as a set of valid values that a variable could hold. In typescript you can define union types that simply hold one of a set of defined values. Eg: type OneOrThree = 1 | 3 or type Nullable<T> = T | null This is arguably nicer than Maybe / Option because you can loosen / tighten API constraints without changing the API. Eg, myfn(x: number) can be rewritten to myfn(x: number | null) with all the safety benefits of Maybe but without the need to change any callers. Its not just Ada - Rust also has non-zero integer types in the standard library. Eg: https://doc.rust-lang.org/std/num/struct.NonZeroU32.html https://doc.rust-lang.org/std/num/struct.NonZeroU32.html This was written mostly let Option<NonZeroU32> take up the same amount of space as u32. Ie, if you know your integer will never be zero, you can reuse the zero slot as a sentinal None value in a way thats API-compatible with everything else in rust.
- deleted 8y ago
  [deleted]
- clhodapp 8y ago
  Division by zero isn't necessarily a runtime error. You could define your division operation to only admit divisors that are statically known not to equal zero. You just need a type system that is strong enough to track whether a number has been confirmed not to equal zero.
  - kazinator 8y ago
    (Only problem is that such a type system is unwieldy compared to mathematics itself.)
    - 0db532a0 8y ago
      I suppose we’d better get you in contact with with all those silly mathematicians who like to use proof assistants to add rigour to their work.
      - kazinator 8y ago
        In run of the mill mathematics, I've never seen zero treated as a special type. In derivations, a restriction against zero (because some variable appeared in a denominator) is usually carried as a logical assertion that is attached to subsequent derivations, like "<.. equation ...>, x /= 0".
- naasking 8y ago
  > They are typed. Weakly/dynamically typed. Unityped, as in, they have only one type. You can assign any type to any variable, so all values have a single type. > Also, division by zero is an runtime operation error, it is not really a type error. The division operation doesn't fail because it violated the type system, it fails because you can't mathematically divide by zero. That is a type error in some type systems. The general notion of a type is a logical proposition. "Non-zero number" is a proposition and so you can represent this with types. The type of division is then `Num -> (Num != 0) -> Num`. > Dynamic languages are untyped languages like javascript and racket. This is not true. All languages are typed, either with rich types, or they are unityped (like the lambda calculus or JS). Machine language is typed, and the fundamental types are (roughly) word and double. These are the registers of machine language, which you can roughly think of as variables in programming languages.
  - int_19h 8y ago
    Values in JS still have different types (as evidenced by their different behavior). Variables could all be argued to have one type in JS, which is the root type (which everything else subtypes). So no, JS is still not untyped, merely dynamically typed. An example of a language that also has only one data type for value would be something like Tcl, where the only type is a string - and everything else is just an optimized way to store certain kinds of strings, that could be removed without affecting semantics of any program.
    - kazinator 8y ago
      They could be argued, but that would be wrong. If we define a variable, give it the value 42 and then never change it over the lifetime of the image, then that variable's type is integer. Or, even more specifically, its type is the set { 42 }. It may be the case that no such thing is actually analyzed and the implementation always retains the potential to reassign that variable; that doesn't change the mathematical fact that the set of values which that variable is fixed. That the implementation is not interested in examining the type of a variable (let alone checking for consistency with the rest of the program) shouldn't be mistaken for the absence of type. There is a mathematical fact about the program that isn't constrained by the quality and depth of its implementation.
- smadge 8y ago
  From the article: "Definition. A type is a statement of the invariants of some expressions." To the author, a type is any mathematical statement that can be proven about the code. This definition is so general that, yes, every computer language is typed, as we can prove things about programs in that language. For example: when provided with an integer as input this program produces as integer as output, this program will terminate, this program returns a sorted list of digits, this program will never divide by zero, this program recognizes sentences from this language, etc.
  - roenxi 8y ago
    On the one hand, I doubt the author was out to stir up criticism on HN. On the other, that definition is skirting quite close to defining everything in the known universe as typed - I suspect there is a hair splitting argument about whether the fundamentals of physics can be defined as a 'symbol' in an 'expression'. With that sort of starting point, it is no longer clear what the value of things being typed is. If everything has a type, what use is it to point out that a thing is typed? The results become too trivial to be worth discussing. A little further down this rabbit hole and we'll have discovered that mathematics encapsulates universal laws!
    - smadge 8y ago
      I think the main point of the article is to shift type systems from being necessarily a part of the language itself to something that can exist outside the language and used to analyze it. For instance I once wrote a program which would infer types on a subset of Python and identify simple type errors without running it. That said there are languages which are more amendable to type checking. For example type checking a Ruby program which dynamically adds methods to a class.
- tom_mellior 8y ago
  > Weakly/dynamically typed. These terms do not mean the same thing, and the two languages you mention are not weakly typed. Strong typing means, roughly, that type errors can be detected at some point. It is strong static typing if this detection is at compile time, and strong dynamic typing if it happens at runtime. Racket is strongly dynamically typed: > (car 42) car: contract violation expected: pair? given: 42 The type error is detected. Weak typing is the opposite of strong typing. Assembly languages are weakly typed: you never know what's in a register. So is Forth. So is C, if you allow pointer casts. But dynamically typed programming languages are not weakly typed: They need dynamic type information at runtime to execute, and they do use that information to detect errors.
  - Guthur 8y ago
    Pretty sure javascript is weakly typed.
    - tom_mellior 8y ago
      Can you show an example of a JavaScript type error that is not detected at any point? By "type error" I mean something like "applying integer add to a bit pattern representing an integer and a bit pattern representing a float", which you can do in assembly language or Forth or C, but not in any dynamically typed language I know of. Because you cannot take the bits that make up a float and pretend to the compiler that those bits actually represent an integer.
      - gugagore 8y ago
        I have heard that languages like javascript are weakly typed because of the effort they go through to evaluate an expression instead of throwing a type error. >> "5" - 3 < 2 It doesn't fit your example of a type error. Quite the opposite, the interpreter intentionally has code to do the specific thing for the specific types. But this feature is why javascript is "weakly typed" in many posts.
      - leshow 8y ago
        weak/strong typing has no formal definition. You can argue over it's meaning but neither of you will be right.
- igouy 8y ago
  these ['Strong and Weak Typing'] words have nearly no meaning at all. http://blogs.perl.org/users/ovid/2010/08/what-to-know-before-debating-type-systems.html http://blogs.perl.org/users/ovid/2010/08/what-to-know-before... So what is “strong typing”? This appears to be a meaningless phrase, and people often use it in a non-sensical fashion. To some it seems to mean “The language has a type checker”. To others it means “The language is sound” (that is, the type checker and run-time system are related). To most, it seems to just mean, “A language like Pascal, C or Java, related in a way I can’t quite make precise”. If someone uses this phrase, be sure to ask them to define it for you. (For amusement, watch them squirm.) page 263 "Programming Languages: Application and Interpretation" Shriram Krishnamurthi 2003
myWindoonn 8y ago
And most type systems don't actually reflect the subtyping relation inherent in the topos correspondent to their logic. As a result, there is a massive disconnect between type systems, which let us catch errors in programs without running them, and type theory, an essential and unavoidable part of doing maths. I think that we should take "typed", "untyped", etc. away from the dynamic-language haters and force them to justify their positions without this needlessly-perjorative attitude. "Types lend themselves to strong automated reasoning, automatically eliminate large classes of errors, and simplify the job of whoever is reasoning about the programs," writes the author, ignoring that there are piles of similar features in the language design space, like highlighting, typesetting, brace-matching, whitespace, capitalization conventions, docstrings, named variables, named procedures, 2D/spatial layout, ASCII/JIS/Unicode art, and the list goes on and on and on.
- AnaniasAnanas 8y ago
  > most type systems don't actually reflect the subtyping relation inherent in the topos correspondent to their logic Would you mind elaborating? With examples if possible. > ignoring that there are piles of similar features in the language design space, like highlighting, typesetting, brace-matching, whitespace, capitalization conventions, docstrings, named variables, named procedures, 2D/spatial layout, ASCII/JIS/Unicode art, and the list goes on and on and on. I am interested to see how any of these would protect against bugs that say a type system with dependent types would protect against.
  - myWindoonn 8y ago
    The most infamous example is that of Haskell. Reasoning in Haskell is not the same as reasoning in the category Hask [1], whose objects and arrows purport to be Haskell types and functions; many folks are actually reasoning in an idealized, simplified Hask. Papers like "Fast and Loose Reasoning is Morally Correct" [0] justify this stance. (There is, to be fair, work on determining Haskell's actual categorical properties. [2]) This attitude is popular across the ML family, but spikes in the Haskell community for some reason. I don't have a good citation for categorical subtypes, but it is well-known category-theory folklore that often objects have subobjects and that a given arrow `f : X -> Y` has fixed source object X and target object Y, and therefore that f likely embodies not just categorical structure but also subobject structure inside X. There may be many distinct arrows of type `X -> Y`, each with different subobject behavior. This is where concepts like dependent typing shine, right? I'm going to take the other branch of your implicit dilemma. Let's protect against the same bugs that dependent types protect against, but without dependent types. This is valid E [3] or Monte [4], and languages in the E family are what Haskellers would call "unityped" or "untyped". The specification is that `y >= x` and also that the return value `rv >= y`. The compiler is not obligated to infer corollaries like `x >= 0`. def f(x :Int, y :(Int >= x)) :(Int >= y) { return x + y } It is not accidental that Monte has a categorical semantics [5] at the level of values and not types. It seems to be the case that, even if the category of types is trivial, the category of values is rich. At the same time, studying only the category of types and never examining the values is insufficient! Ponder this Haskell REPL session: $ nix run nixpkgs.ghc -c ghci GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help Prelude> :t reverse reverse :: [a] -> [a] Prelude> :t const [] :: [a] -> [a] const [] :: [a] -> [a] :: [a] -> [a] Prelude> :t cycle cycle :: [a] -> [a] Prelude> :t map id map id :: [b] -> [b] Prelude> :t tail tail :: [a] -> [a] Studying the types alone, we are helpless. We need to know something of the values as well. [0] http://www.cse.chalmers.se/~nad/publications/danielsson-et-al-popl2006.pdf http://www.cse.chalmers.se/~nad/publications/danielsson-et-a... [1] https://wiki.haskell.org/Hask https://wiki.haskell.org/Hask [2] http://www.cs.gunma-u.ac.jp/~hamana/Papers/cpo.pdf http://www.cs.gunma-u.ac.jp/~hamana/Papers/cpo.pdf [3] http://erights.org/ http://erights.org/ [4] https://monte.readthedocs.io/ https://monte.readthedocs.io/ [5] https://monte.readthedocs.io/en/latest/category.html https://monte.readthedocs.io/en/latest/category.html
mlthoughts2018 8y ago
This is totally backwards. Typed programming languages don’t exist, as in at runtime it’s just instructions applied to sequences of bits. A type is just a convention about an agreed interpretation of those bits. It’s a temporary fiction that doesn’t exist at runtime.
- klodolph 8y ago
  There's some inconsistency in that argument. If a type is just a convention about an agreed interpretation of bits, then isn't it equally true that bits are just a convention about an agreed interpretation of voltages, charges, and magnetic domains? But worse yet, voltages, charges, and magnetic domains are just interpretations of the physical world, and they don't really "exist" either...
  - mlthoughts2018 8y ago
    I don’t see what the inconsistency is?
    - klodolph 8y ago
      We build layers of interpretation on top of one another, and we get this big stack with abstract things like types and programs on the top, bits and bytes somewhere in the middle, voltages and transistors farther down, and fundamental particles at or near the very bottom. We agree that the stuff at the bottom exists, if the word "exists" has any meaning at all. But if you argue that "things which are just conventions about how to interpret other things" (like types) are not real and do not exist, if you want to be consistent about that, the entire stack evaporates and you are left with whatever is at the bottom, such as fundamental particles. For a more concrete example, you said that, "A type is just a convention about an agreed interpretation of those bits." The major problem with this statement is that a program is also an agreed interpretation of some bits. Whether some piece of memory is an instruction or data is just a matter of interpretation. So if this argument says that types do not exist at runtime, then programs do not exist either. So if we accept that programs exist, the argument must be wrong.
madmax96 8y ago
I'm going to be a little nitpicky here: > Definition. An expression is a symbol of sequence of symbols given some interpretation. > Definition. A language is collection of expressions. I immediately reject these definition. A language is a subset of the free monoid over some alphabet [1]. This definition is widely used and the author changing the definition here is significant. Next, because the author requires that each expression be given an interpretation, the author conflates language (e.g. valid strings) with semantics (e.g. the interpretation of strings). > The result of this sequence of symbols is undefined in C. ... > Definition. Undefined behavior is the result of interpreting a non-expression. The author is mixing around a few definitions of "undefined behavior". Of course, C compilers will gladly compile programs containing expressions that are total nonsense. The resulting behavior of the program has no meaningful semantics but the program itself consists only of valid expressions. Because a program may contain expressions that exhibit UB when operating with standard definitions (e.g. the definitions of "expression" and "language" ubiquitously used when discussing programming languages and compilers) the proof is incorrect. The immediate implication of this result is that technically a C program with UB is free to modify itself non-deterministically and thereby prevent any existing proof system from predicting its behavior. However, definitions aren't really "right" or "wrong." The proof is otherwise sound. My critique is that real systems aren't built using the definitions the author uses and therefore the resulting theorem isn't really applicable in any practical circumstance. [1] https://en.wikipedia.org/wiki/Formal_language https://en.wikipedia.org/wiki/Formal_language
goto11 8y ago
I find it a bit of a strawman. "Untyped" is not a very common term for programming languages. "Dynamically typed" is much more common in my experience. I'd call something like CSV untyped.
- tom_mellior 8y ago
  Certain subsets of the statically typed functional programming research crowd (i.e., Haskell/OCaml/ML aficionados) do like to refer to dynamically typed languages as "untyped". For them it is a common term of derision. Unfortunately they do not know or care that the rest of the world uses the term differently.
  - Tade0 8y ago
    Derision is generally worryingly common among these people. This is of course anecdotal on my part but as someone working with JS on a daily basis I've received more than my share of insults based on my choice of career.
    - olau 8y ago
      I've seen the same. Yet good user interfaces are typically warty behind the scenes and full of exceptions, exactly the kind of thing where spending a lot of time on specifications/typing offers little reward. Au contraire, it can put you into a mindset where you'd rather fight the users than put in another difficult-to-handle-typewise exception. Some time ago I had a look at old Visual Basic which I've never personally used, and lo and behold, if you squint it's not actually that far from Javascript.
      - Tade0 8y ago
        Ha! I remember when VBScript was still a thing. What a different world we would be living in had Microsoft had its way.
    - klodolph 8y ago
      The derision towards JS programmers is very real, but I don't think it's fair to turn it into a generalization about "these people" (being PL researchers and Haskell/ML/etc aficionados). I've encountered enough JavaScript programmers telling me how important Node.js is, and how crazy I am for not using asynchronous programming, or for using a different language in the browser and the server, or how static typing is a waste of time and you should really be using tests. I'm not going to say that's worryingly common among JavaScript programmers, though. It's just very natural that people who work with a certain set of tools are acutely aware of those tools' advantages. And I've also encountered plenty of C++ programmers explaining to me how crazy it is that I'm using a garbage collector, or that I'm not compiling something down to native machine code ahead of time. And the people in industry will make fun of the people in academia, and the academics will make fun of people in industry.
deleted 8y ago
[deleted]
tabtab 8y ago
On C2-dot-com there used to be a long running debate about "tag based" dynamic typing versus tag-free dynamic typing. Tag-free is similar to "untyped", but that may depend heavily on which definitions are used. This debate included whether tag-free is "good", and how to define it, since "tag" implies an implementation and not really behavior. One may also use tags for compression and speed "under the hood" even under "tag-free", but the programmer may not otherwise have to care as a language user (outside of performance issues). Thus, how does one know as a language user that the language is "tag free"? I lean toward tag-free; it makes life simpler in my opinion. Interesting but thready debate. A battle of philosophy and definitions.

45 points by gbrown_ 8y ago

A couple of points. Javascript, Racket, etc that he listed aren't "untyped" languages. They are typed. Weakly/dynamically typed. Although I guess some people equate the two. So lets go with that. Also, division by zero is an runtime operation error, it is not really a type error. The division operation doesn't fail because it violated the type system, it fails because you can't mathematically divide by zero. Finally, x86 assembly doesn't really have what we call a type system in the general sense. But assuming his premises and logic, the conclusion should be "Typed Programs Don't Exist". If x86 checks its type at runtime ( division by zero ), then it is a dynamic language. Dynamic languages are untyped languages like javascript and racket. And since all programs are ultimately assembly programs and all assembly programs are created by dynamic languages then it must mean that all programs are untyped. Hence, no typed programs exist. Ultimately, the author's argument is that runtime division by zero error is proof of x86 type system. But if that is true, x86 assembly is a dynamic ( aka untyped ) language. And his conclusion is wrong.

saagarjha 8y ago
> Finally, x86 assembly doesn't really have what we call a type system in the general sense. I might argue that it kind of does, based on the width of the operands. For example, you can only movq a quadword–you will get a "compile error" if you try to use it on a 16-bit value.
- firethief 8y ago
  I'm not sure encodability can usefully be considered to define x86's type system. rax can be used in places r8 can't.
  - saagarjha 8y ago
    As in, there are certain instructions that operate on rax but not r8? Maybe a more complex type system in this case where rax and r8 are specialized quadwords and certain instructions accept more specific arguments?
    - firethief 8y ago
      Every register besides r8-r15 has special functions, and different registers support different addressing operations. There are at most two pairs of equivalent registers: r8/r10 and r9/r11 (i.e. I don't know of any operation in which r8 couldn't be swapped with r10, and likewise for r9/r11). All other registers are unique (i.e., for any pair of them, there exist valid assembly programs that would become invalid if you swapped usage of the registers in that pair throughout the program). So you can define a type system isomorphic to a lot of things, but this seems to me a degenerate case. What's the point of considering it a type system when no two values can be of the same type, almost all operations are polymorphic, almost all operations are on multiple types, and almost every instruction involves a conversion between types?
- kazinator 8y ago
  Machine instruction sets have data type systems which tend to give a well-defined meaning to type punning. If an integer is reinterpreted as a floating-point value, the meaning is precisely determined down to the last bit. Few restrictions are placed by machine instruction sets on how a datum that is written into memory by a store is later interpreted by a load, though the semantics is clear for any given value. This is better than "undefined behavior" (how C treats similar situations), because it is predictable, but it has to be identified as weak typing. We might call it "weak static typing". An assembly language program that assembles doesn't contain any undefined behavior due to misuse of type. When we assemble an instruction like "load 32 bits from the address given in R1 into R2", there is no possible type error there. In machine languages, there are other type rules at play besides just data type, and assembly languages tend to treat these poorly. For instance, whether a pointer is suitably aligned for a given access is arguably a type. It may be the case that only pointers ending in 00 (bits) have the right type for accessing a 32 bit value. However, we can assemble the "load 32 bits from [R1] into R2" instruction silently without the assembler providing any type check that R1 contains a suitably aligned pointer. If we work with arrays in a typical assembly language, we don't get static bounds checks. In short, machine language programs can exhibit horrible run-time errors due to misuse of memory, which are not statically caught by assemblers, even though we can pun among different kind of operands while remaining within non-failing behavior (no exceptions raised) and well-defined results being produced.
fao_ 8y ago
"Also, division by zero is an runtime operation error, it is not really a type error. The division operation doesn't fail because it violated the type system, it fails because you can't mathematically divide by zero." Zero is a different type from the type that consists of integers above N.
- slededit 8y ago
  Its an interesting concept. Addition or subtraction now would have to dynamically return either a zero type or a non-zero type. I suppose the type system could force you to check and handle the zero case. In reality I think it would be too cumbersome. Division by zero is a relatively rare flaw and zero agnostic math on integers is common. I'd love to hear about any languages that do this.
  - joshuamorton 8y ago
    Not necessarily, additional and subtraction just return int, but you can define other operations over subsets of ints that return nonzero. Rust does something similar, floats by default can be NaN, but you can write a non-NaN float that just panics if it's Nan and then ignore the possibility of Nan in parts of your system.
- smadge 8y ago
  What is "the type that consists of integers above N?" If N = -1, then 0 is in the set of integers greater than N. I think it makes more sense to say that division is a function F × (F - {0}) → F where F is a field. F is not the same set/type as F without 0. I think in the context of computer languages this would be called a refinement type. (https://en.wikipedia.org/wiki/Refinement_type https://en.wikipedia.org/wiki/Refinement_type)
- tremon 8y ago
  Can you show a language that implements your concept of "integers above N" consistently? I fail to see how such a type would be remotely useful in the context of addition/subtraction operators. I think Ada comes closest to your definition with allowing modular and derived integer types, but the former does include 0 and I'm not sure if the latter even allows division.
AnaniasAnanas 8y ago
> Also, division by zero is an runtime operation error, it is not really a type error .. in most languages. This is not universally true however. Consider a language with dependent types whose division function has a type signature like so: div : Nat -> (y : Nat) -> (y > 0) = True -> Nat, which basically requires a proof that can be verified at compile time that y is bigger than 0. In such a language you would not have a division by zero runtime error. You can even have something similar (but much more painful to use) in languages without dependent types, consider: data Nat1 = Succ Nat1 | One data Nat = CNat1 Nat1 | Zero div : Nat -> Nat1 -> Nat
- jepler 8y ago
  Ada is an example of a standardized, mature language with a "natural number" (strictly positive integer) type.
  - tremon 8y ago
    But Ada doesn't restrict its division operators (div, mod and rem) to just "natural number" divisors.
- josephg 8y ago
  Right. You can also think of a type as a set of valid values that a variable could hold. In typescript you can define union types that simply hold one of a set of defined values. Eg: type OneOrThree = 1 | 3 or type Nullable<T> = T | null This is arguably nicer than Maybe / Option because you can loosen / tighten API constraints without changing the API. Eg, myfn(x: number) can be rewritten to myfn(x: number | null) with all the safety benefits of Maybe but without the need to change any callers. Its not just Ada - Rust also has non-zero integer types in the standard library. Eg: https://doc.rust-lang.org/std/num/struct.NonZeroU32.html https://doc.rust-lang.org/std/num/struct.NonZeroU32.html This was written mostly let Option<NonZeroU32> take up the same amount of space as u32. Ie, if you know your integer will never be zero, you can reuse the zero slot as a sentinal None value in a way thats API-compatible with everything else in rust.
deleted 8y ago
[deleted]
clhodapp 8y ago
Division by zero isn't necessarily a runtime error. You could define your division operation to only admit divisors that are statically known not to equal zero. You just need a type system that is strong enough to track whether a number has been confirmed not to equal zero.
- kazinator 8y ago
  (Only problem is that such a type system is unwieldy compared to mathematics itself.)
  - 0db532a0 8y ago
    I suppose we’d better get you in contact with with all those silly mathematicians who like to use proof assistants to add rigour to their work.
    - kazinator 8y ago
      In run of the mill mathematics, I've never seen zero treated as a special type. In derivations, a restriction against zero (because some variable appeared in a denominator) is usually carried as a logical assertion that is attached to subsequent derivations, like "<.. equation ...>, x /= 0".
naasking 8y ago
> They are typed. Weakly/dynamically typed. Unityped, as in, they have only one type. You can assign any type to any variable, so all values have a single type. > Also, division by zero is an runtime operation error, it is not really a type error. The division operation doesn't fail because it violated the type system, it fails because you can't mathematically divide by zero. That is a type error in some type systems. The general notion of a type is a logical proposition. "Non-zero number" is a proposition and so you can represent this with types. The type of division is then `Num -> (Num != 0) -> Num`. > Dynamic languages are untyped languages like javascript and racket. This is not true. All languages are typed, either with rich types, or they are unityped (like the lambda calculus or JS). Machine language is typed, and the fundamental types are (roughly) word and double. These are the registers of machine language, which you can roughly think of as variables in programming languages.
- int_19h 8y ago
  Values in JS still have different types (as evidenced by their different behavior). Variables could all be argued to have one type in JS, which is the root type (which everything else subtypes). So no, JS is still not untyped, merely dynamically typed. An example of a language that also has only one data type for value would be something like Tcl, where the only type is a string - and everything else is just an optimized way to store certain kinds of strings, that could be removed without affecting semantics of any program.
  - kazinator 8y ago
    They could be argued, but that would be wrong. If we define a variable, give it the value 42 and then never change it over the lifetime of the image, then that variable's type is integer. Or, even more specifically, its type is the set { 42 }. It may be the case that no such thing is actually analyzed and the implementation always retains the potential to reassign that variable; that doesn't change the mathematical fact that the set of values which that variable is fixed. That the implementation is not interested in examining the type of a variable (let alone checking for consistency with the rest of the program) shouldn't be mistaken for the absence of type. There is a mathematical fact about the program that isn't constrained by the quality and depth of its implementation.
smadge 8y ago
From the article: "Definition. A type is a statement of the invariants of some expressions." To the author, a type is any mathematical statement that can be proven about the code. This definition is so general that, yes, every computer language is typed, as we can prove things about programs in that language. For example: when provided with an integer as input this program produces as integer as output, this program will terminate, this program returns a sorted list of digits, this program will never divide by zero, this program recognizes sentences from this language, etc.
- roenxi 8y ago
  On the one hand, I doubt the author was out to stir up criticism on HN. On the other, that definition is skirting quite close to defining everything in the known universe as typed - I suspect there is a hair splitting argument about whether the fundamentals of physics can be defined as a 'symbol' in an 'expression'. With that sort of starting point, it is no longer clear what the value of things being typed is. If everything has a type, what use is it to point out that a thing is typed? The results become too trivial to be worth discussing. A little further down this rabbit hole and we'll have discovered that mathematics encapsulates universal laws!
  - smadge 8y ago
    I think the main point of the article is to shift type systems from being necessarily a part of the language itself to something that can exist outside the language and used to analyze it. For instance I once wrote a program which would infer types on a subset of Python and identify simple type errors without running it. That said there are languages which are more amendable to type checking. For example type checking a Ruby program which dynamically adds methods to a class.
tom_mellior 8y ago
> Weakly/dynamically typed. These terms do not mean the same thing, and the two languages you mention are not weakly typed. Strong typing means, roughly, that type errors can be detected at some point. It is strong static typing if this detection is at compile time, and strong dynamic typing if it happens at runtime. Racket is strongly dynamically typed: > (car 42) car: contract violation expected: pair? given: 42 The type error is detected. Weak typing is the opposite of strong typing. Assembly languages are weakly typed: you never know what's in a register. So is Forth. So is C, if you allow pointer casts. But dynamically typed programming languages are not weakly typed: They need dynamic type information at runtime to execute, and they do use that information to detect errors.
- Guthur 8y ago
  Pretty sure javascript is weakly typed.
  - tom_mellior 8y ago
    Can you show an example of a JavaScript type error that is not detected at any point? By "type error" I mean something like "applying integer add to a bit pattern representing an integer and a bit pattern representing a float", which you can do in assembly language or Forth or C, but not in any dynamically typed language I know of. Because you cannot take the bits that make up a float and pretend to the compiler that those bits actually represent an integer.
    - gugagore 8y ago
      I have heard that languages like javascript are weakly typed because of the effort they go through to evaluate an expression instead of throwing a type error. >> "5" - 3 < 2 It doesn't fit your example of a type error. Quite the opposite, the interpreter intentionally has code to do the specific thing for the specific types. But this feature is why javascript is "weakly typed" in many posts.
    - leshow 8y ago
      weak/strong typing has no formal definition. You can argue over it's meaning but neither of you will be right.
igouy 8y ago
these ['Strong and Weak Typing'] words have nearly no meaning at all. http://blogs.perl.org/users/ovid/2010/08/what-to-know-before-debating-type-systems.html http://blogs.perl.org/users/ovid/2010/08/what-to-know-before... So what is “strong typing”? This appears to be a meaningless phrase, and people often use it in a non-sensical fashion. To some it seems to mean “The language has a type checker”. To others it means “The language is sound” (that is, the type checker and run-time system are related). To most, it seems to just mean, “A language like Pascal, C or Java, related in a way I can’t quite make precise”. If someone uses this phrase, be sure to ask them to define it for you. (For amusement, watch them squirm.) page 263 "Programming Languages: Application and Interpretation" Shriram Krishnamurthi 2003

myWindoonn 8y ago

And most type systems don't actually reflect the subtyping relation inherent in the topos correspondent to their logic. As a result, there is a massive disconnect between type systems, which let us catch errors in programs without running them, and type theory, an essential and unavoidable part of doing maths. I think that we should take "typed", "untyped", etc. away from the dynamic-language haters and force them to justify their positions without this needlessly-perjorative attitude. "Types lend themselves to strong automated reasoning, automatically eliminate large classes of errors, and simplify the job of whoever is reasoning about the programs," writes the author, ignoring that there are piles of similar features in the language design space, like highlighting, typesetting, brace-matching, whitespace, capitalization conventions, docstrings, named variables, named procedures, 2D/spatial layout, ASCII/JIS/Unicode art, and the list goes on and on and on.

AnaniasAnanas 8y ago
> most type systems don't actually reflect the subtyping relation inherent in the topos correspondent to their logic Would you mind elaborating? With examples if possible. > ignoring that there are piles of similar features in the language design space, like highlighting, typesetting, brace-matching, whitespace, capitalization conventions, docstrings, named variables, named procedures, 2D/spatial layout, ASCII/JIS/Unicode art, and the list goes on and on and on. I am interested to see how any of these would protect against bugs that say a type system with dependent types would protect against.
- myWindoonn 8y ago
  The most infamous example is that of Haskell. Reasoning in Haskell is not the same as reasoning in the category Hask [1], whose objects and arrows purport to be Haskell types and functions; many folks are actually reasoning in an idealized, simplified Hask. Papers like "Fast and Loose Reasoning is Morally Correct" [0] justify this stance. (There is, to be fair, work on determining Haskell's actual categorical properties. [2]) This attitude is popular across the ML family, but spikes in the Haskell community for some reason. I don't have a good citation for categorical subtypes, but it is well-known category-theory folklore that often objects have subobjects and that a given arrow `f : X -> Y` has fixed source object X and target object Y, and therefore that f likely embodies not just categorical structure but also subobject structure inside X. There may be many distinct arrows of type `X -> Y`, each with different subobject behavior. This is where concepts like dependent typing shine, right? I'm going to take the other branch of your implicit dilemma. Let's protect against the same bugs that dependent types protect against, but without dependent types. This is valid E [3] or Monte [4], and languages in the E family are what Haskellers would call "unityped" or "untyped". The specification is that `y >= x` and also that the return value `rv >= y`. The compiler is not obligated to infer corollaries like `x >= 0`. def f(x :Int, y :(Int >= x)) :(Int >= y) { return x + y } It is not accidental that Monte has a categorical semantics [5] at the level of values and not types. It seems to be the case that, even if the category of types is trivial, the category of values is rich. At the same time, studying only the category of types and never examining the values is insufficient! Ponder this Haskell REPL session: $ nix run nixpkgs.ghc -c ghci GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help Prelude> :t reverse reverse :: [a] -> [a] Prelude> :t const [] :: [a] -> [a] const [] :: [a] -> [a] :: [a] -> [a] Prelude> :t cycle cycle :: [a] -> [a] Prelude> :t map id map id :: [b] -> [b] Prelude> :t tail tail :: [a] -> [a] Studying the types alone, we are helpless. We need to know something of the values as well. [0] http://www.cse.chalmers.se/~nad/publications/danielsson-et-al-popl2006.pdf http://www.cse.chalmers.se/~nad/publications/danielsson-et-a... [1] https://wiki.haskell.org/Hask https://wiki.haskell.org/Hask [2] http://www.cs.gunma-u.ac.jp/~hamana/Papers/cpo.pdf http://www.cs.gunma-u.ac.jp/~hamana/Papers/cpo.pdf [3] http://erights.org/ http://erights.org/ [4] https://monte.readthedocs.io/ https://monte.readthedocs.io/ [5] https://monte.readthedocs.io/en/latest/category.html https://monte.readthedocs.io/en/latest/category.html

mlthoughts2018 8y ago

This is totally backwards. Typed programming languages don’t exist, as in at runtime it’s just instructions applied to sequences of bits. A type is just a convention about an agreed interpretation of those bits. It’s a temporary fiction that doesn’t exist at runtime.

klodolph 8y ago
There's some inconsistency in that argument. If a type is just a convention about an agreed interpretation of bits, then isn't it equally true that bits are just a convention about an agreed interpretation of voltages, charges, and magnetic domains? But worse yet, voltages, charges, and magnetic domains are just interpretations of the physical world, and they don't really "exist" either...
- mlthoughts2018 8y ago
  I don’t see what the inconsistency is?
  - klodolph 8y ago
    We build layers of interpretation on top of one another, and we get this big stack with abstract things like types and programs on the top, bits and bytes somewhere in the middle, voltages and transistors farther down, and fundamental particles at or near the very bottom. We agree that the stuff at the bottom exists, if the word "exists" has any meaning at all. But if you argue that "things which are just conventions about how to interpret other things" (like types) are not real and do not exist, if you want to be consistent about that, the entire stack evaporates and you are left with whatever is at the bottom, such as fundamental particles. For a more concrete example, you said that, "A type is just a convention about an agreed interpretation of those bits." The major problem with this statement is that a program is also an agreed interpretation of some bits. Whether some piece of memory is an instruction or data is just a matter of interpretation. So if this argument says that types do not exist at runtime, then programs do not exist either. So if we accept that programs exist, the argument must be wrong.

madmax96 8y ago

I'm going to be a little nitpicky here: > Definition. An expression is a symbol of sequence of symbols given some interpretation. > Definition. A language is collection of expressions. I immediately reject these definition. A language is a subset of the free monoid over some alphabet [1]. This definition is widely used and the author changing the definition here is significant. Next, because the author requires that each expression be given an interpretation, the author conflates language (e.g. valid strings) with semantics (e.g. the interpretation of strings). > The result of this sequence of symbols is undefined in C. ... > Definition. Undefined behavior is the result of interpreting a non-expression. The author is mixing around a few definitions of "undefined behavior". Of course, C compilers will gladly compile programs containing expressions that are total nonsense. The resulting behavior of the program has no meaningful semantics but the program itself consists only of valid expressions. Because a program may contain expressions that exhibit UB when operating with standard definitions (e.g. the definitions of "expression" and "language" ubiquitously used when discussing programming languages and compilers) the proof is incorrect. The immediate implication of this result is that technically a C program with UB is free to modify itself non-deterministically and thereby prevent any existing proof system from predicting its behavior. However, definitions aren't really "right" or "wrong." The proof is otherwise sound. My critique is that real systems aren't built using the definitions the author uses and therefore the resulting theorem isn't really applicable in any practical circumstance. [1] https://en.wikipedia.org/wiki/Formal_language https://en.wikipedia.org/wiki/Formal_language

goto11 8y ago

I find it a bit of a strawman. "Untyped" is not a very common term for programming languages. "Dynamically typed" is much more common in my experience. I'd call something like CSV untyped.

tom_mellior 8y ago
Certain subsets of the statically typed functional programming research crowd (i.e., Haskell/OCaml/ML aficionados) do like to refer to dynamically typed languages as "untyped". For them it is a common term of derision. Unfortunately they do not know or care that the rest of the world uses the term differently.
- Tade0 8y ago
  Derision is generally worryingly common among these people. This is of course anecdotal on my part but as someone working with JS on a daily basis I've received more than my share of insults based on my choice of career.
  - olau 8y ago
    I've seen the same. Yet good user interfaces are typically warty behind the scenes and full of exceptions, exactly the kind of thing where spending a lot of time on specifications/typing offers little reward. Au contraire, it can put you into a mindset where you'd rather fight the users than put in another difficult-to-handle-typewise exception. Some time ago I had a look at old Visual Basic which I've never personally used, and lo and behold, if you squint it's not actually that far from Javascript.
    - Tade0 8y ago
      Ha! I remember when VBScript was still a thing. What a different world we would be living in had Microsoft had its way.
  - klodolph 8y ago
    The derision towards JS programmers is very real, but I don't think it's fair to turn it into a generalization about "these people" (being PL researchers and Haskell/ML/etc aficionados). I've encountered enough JavaScript programmers telling me how important Node.js is, and how crazy I am for not using asynchronous programming, or for using a different language in the browser and the server, or how static typing is a waste of time and you should really be using tests. I'm not going to say that's worryingly common among JavaScript programmers, though. It's just very natural that people who work with a certain set of tools are acutely aware of those tools' advantages. And I've also encountered plenty of C++ programmers explaining to me how crazy it is that I'm using a garbage collector, or that I'm not compiling something down to native machine code ahead of time. And the people in industry will make fun of the people in academia, and the academics will make fun of people in industry.

deleted 8y ago

[deleted]

tabtab 8y ago

On C2-dot-com there used to be a long running debate about "tag based" dynamic typing versus tag-free dynamic typing. Tag-free is similar to "untyped", but that may depend heavily on which definitions are used. This debate included whether tag-free is "good", and how to define it, since "tag" implies an implementation and not really behavior. One may also use tags for compression and speed "under the hood" even under "tag-free", but the programmer may not otherwise have to care as a language user (outside of performance issues). Thus, how does one know as a language user that the language is "tag free"? I lean toward tag-free; it makes life simpler in my opinion. Interesting but thready debate. A battle of philosophy and definitions.