4

First let me explain what is my understanding of the terms statically typed language and type safety:

Statically typed language: a language that does not allow you to change the type of a variable at run-time.

Type safety: type safety means that you are not allowed to mix incompatible data types. For example, you cannot assign a float to an int, and you cannot assign an int to a function pointer, and you cannot add a user-defined object to an int (unless you use operator overloading), etc.


Back to my question, let's say that there is an interpreted statically typed language, in such a language I can write code that assigns a float to an int, but when this code is executed, a (run-time) type error will occur.

Is such a language considered to be type safe, or are type safe languages can only be statically typed and compiled, and so type errors must be caught at the compilation stage?

  • Whatever the technical answer; it seems far less useful – Richard Tingle Sep 27 '16 at 20:18
  • 2
    I'm not sure what you mean. Are you saying Haskell would be more useful if Hugs didn't exist? That seems almost contradictory: how could a language become more useful by allowing less ways to use it? – Jörg W Mittag Sep 27 '16 at 21:36
12

Statically typed language: a language that does not allow you to change the type of a variable at run-time.

That's not the definition of statically typed. Statically typed means that type checking (and type inference) happens before runtime. The opposite is dynamic typing, where type checking happens at runtime.

It is perfectly possible to design a statically typed language in which either identifiers can change types or types can change.

Type safety: type safety means that you are not allowed to mix incompatible data types. For example, you cannot assign a float to an int, and you cannot assign an int to a function pointer, and you cannot add a user-defined object to an int (unless you use operator overloading), etc.

There is no universally accepted definition of type safety. Yours is a very sensible one.

Back to my question, let's say that there is an interpreted statically typed language,

There is no such thing as an interpreted statically typed language, simply because there is no such thing as an interpreted language, period. Interpretation and compilation are traits of the, well, interpreter or compiler (duh!), i.e. the implementation, not the language. Every language can be implemented with an interpreter and every language can be implemented with a compiler. In fact, many languages have both interpreted and compiled implementations. For example, Haskell has several compiled implementations (Ghc, Jhc, Yhc, Lhv) and an interpreted implementation (Hugs). ECMAScript has pure compiled implementations (V8), and hybrid mixed-mode implementations (e.g. SpiderMonkey AOT-compiles ECMAScript to SpiderMonkey bytecode, then both compiles and interprets this bytecode)

Saying that a language is an "interpreted language" is not just wrong, it is even more than wrong, it is simply non-sensical. The idea of "language" and the idea of "interpretation" live on two different levels of abstraction. If English were a typed language, "interpreted language" would be a type error.

in such a language I can write code that assigns a float to an int, but when this code is executed, a (run-time) type error will occur.

You are inconsistent with yourself here.

You say "statically typed" means "does not allow to change the type of a variable", which means you can not write such code. But now you say that you can write such code in a statically typed language.

But if you can write such code, then by your own definition, it is not statically typed. And if it is statically typed, then by your own definition, you cannot write such code.

So, it's not surprising that you get a contradiction, because you are contradicting yourself.

Is such a language considered to be type safe, or are type safe languages can only be statically typed and compiled, and so type errors must be caught at the compilation stage?

Whether or not type safe languages can only be statically typed or not really only depends on how you define "type safe". Another common definition of "type safe" is that you cannot subvert the type system. Ruby is dynamically typed, but it is usually described as type safe. On the other hand, C is statically typed but nobody would describe it as type safe.

As for whether a type safe language can only be compiled, I already explained above that compilation is an implementation detail, it is not a property of the language itself.

  • "in such a language I can write code that assigns a float to an int, but when this code is executed, a (run-time) type error will occur." I should have said: in such a language if I wrote code that assigns a float to an int, when this code is executed, a (run-time) type error will occur. – user247763 Sep 27 '16 at 21:11
  • 5
    No, it won't. The type error will occur before runtime, otherwise it wouldn't be a statically typed language. And the code won't be executed in the first place. – Jörg W Mittag Sep 27 '16 at 21:13
  • So if C is compiled it is called static typing (because type checking happens before run-time), but if it is interpreted, then it is called dynamic typing (because type checking is done during run-time)? – user247763 Sep 27 '16 at 22:10
  • 1
    No. Compilation and interpretation are a property of the language implementation, not the language. Period. C is still the same language regardless of whether it is compiled, interpreted, both, or even not implemented at all. C is statically typed. That's a property of the language. This property does not change. – Jörg W Mittag Sep 27 '16 at 22:13
  • 2
    @user247763, Interpreters necessarily have a notion of syntactic and semantic error checking that happens on text or bytecode input before execution of any lines of code they processes even if you call interpretation happening entirely at runtime. Which is to say just because it is an interpreter doesn't mean it can't check anything in advance of actual execution. – Erik Eidt Sep 27 '16 at 22:29
2

Instead of answering you're question, I'm going to poke a bit at your definitions. This is because I have a feeling that this question mostly arises from comparing different ideas of "type" and "type safety" as if they were identical.

First, a statically typed language doesn't allow you to change the type of an assignable at runtime isn't quite true: in fact there's a well-studied class of languages with a feature termed "strong updates" that do just this. Moreover, a common view of dynamically typed languages is that they only have one particular "type" in the sense of the word used by statically typed systems. A dynamic language means "type" in the sense of a tag or some piece of data persisted at runtime giving information about the sort of value it's paired with. In a static language, types are a separation of programs into different classes based on their behavior or some other metric. In particular, if we think of the "type of things tagged with a tag at runtime" we arrive precisely at the sort of data we encounter in a dynamic language.

Moreover, static types or languages in general have nothing to do with their implementation. If I write an interpreter for C, it's still C. If I write a compiler for Python, it's still Python. Therefore, the question a language can be type-safe and not compiled must be yes if we accept that there are any type safe languages since whatever languages I can compile I can interpret and vice versa.

Now as far as notions of type-safety go, I would say that this is not the definition you want either. Every single language folks use for software has some provision for exiting with an exception, throwing an error, or generally just complaining in some way. The usual definition of type safety is that if we accept a program as well-formed then that program will run to a value or terminate in some well-defined way, like by throwing an exception. It may not, for example, segfault, get stuck somehow, or just do whatever it wants. With this in mind, lots of dynamic languages are type-safe simply because they ensure that if a program is well-formed, then it has well-defined behavior. Statically typed languages may be type-unsafe though: consider C. Not every C program has defined behavior, plain and simple.

TLDR: the answer to your question is no, whether you interpret the words as you have done or as I would prefer to.

  • Do you consider JavaScript to be a type safe language? – user247763 Sep 27 '16 at 20:36
  • @jozefg Good answer. I will point out though that you left out a case: a well-typed program in a type-safe language may never halt. This is in particular true if the language is turing-complete. Also, what are "strong updates"? I don't think it's possible for the type of a variable to change at runtime, namely because types don't exist at runtime. – gardenhead Sep 27 '16 at 21:05
  • @gardenhead: "Strong update" means overwriting completely the value of a variable with a different value of possibly different type. Making that type safe and supported in the type system is tricky, but there are languages which can do it. Hoare Type Theory is one that supports it. – Jörg W Mittag Sep 27 '16 at 21:08
  • 1
    That sounds suspicious to me. I'm not saying you're incorrect, I would just have to see it to believe it. Actually, isn't that just shadowing? If you have let x: int = 5 in let x: sting = "hi", that would type-check in most languages. It's not updating a variable; it's creating a new variable which just happens to have the same name – gardenhead Sep 27 '16 at 21:14
  • @gardenhead: well, you can do it in C. It's just not type-safe, and thus will (probably) crash. But in HTT, for example, it is. – Jörg W Mittag Sep 27 '16 at 21:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.