[freyrs3]

> When is a language untyped

There's the formal definition of type and there's the colloquial definition of type. A type in the context of the article means a formal type, it is an syntactic classifier that is part of the static semantics of the language. The properties you describe ( string/number exceptions ) are part of the dynamics of the language, which is a separate concept. Dynamically typed languages quite often use boxed values with an attached runtime tags which are colloquially referred to as "types" even though they have nothing to do with static types.

If you read the article in the context of "type" meaning "static type" it will make more sense.

[kazinator]

Does that mean I can search and replace every occurrence of "type" in the article with "static type"?

Are you sure dynamic types have nothing to do with static types? What about compilers for dynamic languages which reason about type, like that if the program calls (symbol-name x), it is inferred that x must hold a string, so that a subsequent (cos x) is inconsistent? Is such a compiler is reasoning about something which has nothing to do with static type?

[chriswarbo]

> What about compilers for dynamic languages which reason about type, like that if the program calls (symbol-name x), it is inferred that x must hold a string, so that a subsequent (cos x) is inconsistent?

That's irrelevant; if the program containing (symbol-name x) and (cos x) works in an interpreter but not in the compiler then the compiler is broken. Note that throwing-exceptions/triggering-errors/etc. is "working", since it's a valid form of control flow which the program could intercept and carry on. Aborting immediately (like a segfault) isn't "working". Triggering undefined behaviour also isn't "working", but since most of these languages lack any real defined behaviour, it's assumed that "whatever the official interpreter does" is correct.

Usually, these compilers completely acknowledge that their behaviour is incorrect WRT the interpreter. They embrace this and define a new, static language which just-so-happens to share a lot of syntax and semantics with that dynamic language. For example, HipHop for PHP could not compile PHP; it could only compile a static language which looks like PHP. Likewise for ShedSkin and Python. PyPy even gives its static language a name: RPython.

Hence, these compilers don't show that runtime tags and static types are the same/similar. Instead, they show that sometimes programmers without static types will use tags to do some things that static types are often used for.

[kd0amg]

Are you sure dynamic types have nothing to do with static types?

"Static type" does not really mean "class of values." That is a common use of static types, but they can also be used for things like tracking what resources are available/released or describing what exceptions a function might raise.

[gsg]

Types are usually understood as proofs: in this case, a proof about whether the tag of x is suitable for passing to cos without causing an error. (If you like, read "dynamic type" for "tag".)

So the proof and the tag are related in that one is about the other, but that does not mean they are the same thing.

[freyrs3]

Quite sure, in a dynamically typed language there is only a single static type inhabited by all values. If the compiler is reasoning about classes of values at runtime then it does indeed have nothing to do with static typing.

[chongli]

If the compiler is applying reasoning before the program is run then it is by definition performing static type checking.