Hacker News Reader

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?)

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.

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