Hacker News Reader

Comment by porpoisely | Hacker News Reader

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.

View on HN

> 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.

Pretty sure javascript is weakly typed.

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.

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.

weak/strong typing has no formal definition. You can argue over it's meaning but neither of you will be right.

From the console output you have shown, from that output alone, how do we know whether that's a static or dynamic type check?

From that output alone we don't know that. I assumed some background knowledge on the reader's part, namely, that Racket is not statically typed by default.

> These terms do not mean the same thing

What do they mean?

"Weakly typed" means that the type system doesn't detect and prevent all situations whereby a datum is misused as if it were of a different type. Programs may misbehave due to type confusion, running off with incorrect results.

"Dynamic typing" means that run-time values carry type information.

Dynamic typing that checks that type information everywhere and diagnoses misuses can be called strongly typed.

Static and dynamic situations can be weakly or strongly typed.

Ada is more strongly typed than C.

Common Lisp is more strongly typed than someone's one-weekend project whose car function cheerfully accepts an integer-typed value and uses it as a cons cell.

"Type safety is the property that no primitive operation ever applies to values of the wrong type."

page 263 "Programming Languages: Application and Interpretation" Shriram Krishnamurthi 2003

----

"Historically, people have sometimes used the phrase strong typing to reflect the kind of type-checking that ML and Java use, and weak typing for the other kinds. However, these phrases are at best poorly defined.

…

Indeed, the phrases are not only poorly defined, they are also wrong, because the problem is not with the “strength” of the type checker but rather with the nature of the run-time system that backs them. The phrases are even more wrong because they fail to account for whether or not a theorem backs the type system."

https://papl.cs.brown.edu/2018/safety-soundness.html#%28part...

Also, there has been a use of "strongly typed" to denote the idea that alias names for types such as integers are incompatible.

In this sense, Pascal family languages were called "strongly typed", whereas C isn't, because a typedef int user_id_t; isn't a new type, but just a name for int that can be passed everywhere an int can be passed. C character handling is also "weakly typed": characters are just kinds of integers: we don't need ord(ch) to get a character's code, or chr(n) to produce a character. C implicit arithmetic conversion behaviors are also weakly typed in this sense.

It's been used to mean this, it's been used to mean that -- now it means we always have to ask what someone actually means.

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.

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!

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.

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.

(Only problem is that such a type system is unwieldy compared to mathematics itself.)

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.

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".

these ['Strong and Weak Typing'] words have nearly no meaning at all.

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

> 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.

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.

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.

Javascript is Unityped. In Haskell/ML, you would define the type of Javascript objects by doing something like this:

    data JSObj
      = Num Double
      | Str String
      | Obj (Hashtable String JSObj)
      | True
      | False
      | Nil
      | Undefined

> Values in JS still have different types (as evidenced by their different behavior).

Behaviour is based on values, not types. 1+2 will print out a different value than 1+1, but these expressions have the same type (typically).

> So no, JS is still not untyped, merely dynamically typed.

I said JS was unityped, not untyped.

Values also have types, it's not something that's exclusive to expressions and bindings.

That is simply not so. Values and variables are not the same thing. Just because variables do not have a type (can potentially hold any value) doesn't mean that values have no type.

Furthermore, variables potentially holding any value doesn't mean they have no type. It is just a potential. A variable effectively has that type which is actually put into it.

If a given variable is always either a string or nil, then that's what it's type is; the sum type of null (the type that contains nil) and the string type.

It may be the case that in a given language implementation, this fact about the variable is not calculated; but it's still a fact.

Neglecting to analyze the types of variables (and other nodes in the program) is an implementation quality/depth choice, not a kind of type system design.

> Just because variables do not have a type (can potentially hold any value) doesn't mean that values have no type. Furthermore, variables potentially holding any value doesn't mean they have no type.

I said they have one type, I didn't say they have no type.

That basically means the same thing. "Typeless dynamic language" and "all variables and object slots having one type" are essentially the same claim: that the bindings or storage locations are all indistinguishable and can take on any value.

(If they have one type, what is that type? And can values be of that type?)

> Unityped, as in, they have only one type.

If there are no distinguishable properties ("one type") then untyped vs unityped seems a distinction without a difference.

Upon further thought, there's probably a useful distinction to be made here. Let's take the classical untyped lambda calculus as a canonical untyped language. Every value is a lambda, so there is clearly only one type, and no deeper structure at play.

Now contrast with something like Scheme or JS. Clearly there is richer underlying structure than mere lambdas, but since every value is still interchangeable (a global sum type) I think this suggests a "unityped" label as a meaningful distinction from the untyped case.

So I would amend my original comment to move the lambda calculus out of unityped and into untyped, and possibly Tcl as well since everything is conceptually a string there.

Let's take BCPL —

'The major difference between BCPL and ALGOL is that all ALGOL variables are declared with data-types (integer, real, boolean, string, array, procedure, label, pointer, etc.), whereas all BCPL variables have the same data-type: a 16-bit number.

In ALGOL, the meaning of an expression is dependent both on its context and on the data-types of the entities involved, and only expressions with certain data-types may appear in a given context.

In BCPL, any expression may be used in any context; the context alone determines how the 16-bit value of the expression is interpreted. BCPL never checks that a value is "appropriate" for use in a given way.'

http://www.bitsavers.org/pdf/xerox/alto/bcpl/BCPL_Reference_...

( I haven't been able to figure out what happens on divide-by-zero:

The division operator / yields the correct result if E1 is divisible by E2; it is otherwise implementation dependent but the rounding error is never greater than 1.

https://www.bell-labs.com/usr/dmr/www/bcpl.pdf )

Surely the meaningful distinction between BCPL and Scheme is that BCPL is not type safe and Scheme is type safe.

I disagree. "Type safety" is not the only kind of safety, and it's not the kind of safety found in either Scheme or BCPL.

> "Type safety" is not the only kind of safety

Never said it was.

"Type safety is the property that no primitive operation ever applies to values of the wrong type."

I did say "BCPL is not type safe" (so on that we agree).

Are you saying that, in Scheme, primitive operations can be applied to values of the wrong type?

A string can be multiplied by 2?

> Are you saying that, in Scheme, primitive operations can be applied to values of the wrong type?

Yes, that's a well-defined operation: it throws a runtime exception (which is also a value). All operations are well-defined in safe languages, that's what makes them safe.

But dynamically "typed" languages aren't type safe.

A truly undefined operation would immediately halt the program because the program simply cannot proceed. You can resolve this unsafety by defining semantics for these operations (like reifying errors as values as in dynamically typed languages), or you can add a type system which ensures only safe programs can be expressed.

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.

> 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.

> 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

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/

> "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.

> 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".

> 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.

> 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.

This strikes me as just a Turing tarpit argument. Sure you can represent and enforce semantics syntactically, and you can probably also do this via automatic translations in many or most cases. Why is this compelling? And what does this have to do with types?

The definition of type system I gave is, "a syntactic method for enforcing levels of abstraction in programs". Ergo, not all syntactic methods qualify as a type system, but a specific kind of syntactic method classify type systems. Why do you think your translation qualifies?

> A quote divorced from context is meaningless.

I'll take that non sequitur to be an acknowledgement that your previous denial was incorrect.

> … and "type" has always meant…

"Language safety is not the same thing as static type safety."

p6 Types and Programming Languages

Apparently the author thought the phrase "type safety" more ambiguous than you do.

> Types can enforce properties that no dynamic "typing" can ever achieve.

Yes, static type checking can enforce properties that dynamic type checking can not.

I should clarify that dynamically typed languages are type safe in the trivial sense that they satisfy unityped type safety. What I meant is that they are not type safe by virtue of what they call types, in the sense that is used by non-unityped languages.

> All languages are typed, either with rich types, or they are unityped

Almost all languages. There is one language that can be typed without a type, the empty language.

Since the empty language contains no programs, it follows that "Untyped Programs Don't Exist".

"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.

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.

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.

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)

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.

> 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.

I'm not sure encodability can usefully be considered to define x86's type system. rax can be used in places r8 can't.

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?

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?

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.

> 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

Ada is an example of a standardized, mature language with a "natural number" (strictly positive integer) type.

But Ada doesn't restrict its division operators (div, mod and rem) to just "natural number" divisors.

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

  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

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.

> You can also think of a type as a set of valid values that a variable could hold

I would suggest avoiding this kind of thinking. Set theory and type theory are separate. Mixing them will only cause confusion and suffering.

> without changing the API

Pretty sure that loosening the return type constraints of a function or tightening the constrains of a variable that a function accepts would both change the API, is my understanding incorrect?

> This was written mostly let Option<NonZeroU32> take up the same amount of space as u32

Why not just use u32 then? These are basically the same thing after all.

> I would suggest avoiding this kind of thinking. Set theory and type theory are separate.

There are some languages - notably, Ada - where this (types as sets) is very much explicit in the language.

> Why not just use u32 then?

For u32, 0 is "just another value" - there's nothing special about it. If you pass it to some other code, there's nothing telling them that they must check for zero, and must not treat zero as actual zero value (and if they forget, it will silently give the wrong answer).

Option<NonZeroU32> requires them to pattern-match on None/Some, and if they get Some, it's guaranteed to be non-zero. That None is stored as zero is an implementation detail in that case, and doesn't leak onto the abstraction level on which code operates.

Reply on news.ycombinator.com