Type Safety and Type Soundness

Type safety and type soundness refer to the extent to which a programming language discourages or prevents type errors.

Type safety là mức độ mà một ngôn ngữ lập trình không khuyến khích/không cho phép các lỗi kiểu dữ liệu.

Examples of Type Safety

          int number = 5;
          String text = "hello";
          //Error
        

          let result = "5" + 2; //Result = 52
          let sum = "5" - 2; //Result = 3
        

Type safety is not the same as static/dynamic typing or strong/weak typing.

Static vs Dynamic typing

Type safety means that if a data item has type X and X doesn't support operation y, then a type-safe language can't perform y(X). This can be checked in different ways:

• If the rule is checked at compile time, then it is a static typing language (static typing is equivalent to type safety at compile time).
• If the rule is checked at runtime, then it is a dynamic typing language (dynamic typing is equivalent to type safety at runtime).
• Some languages check the rule at both compile time and runtime.

Example of Type Safety Issue

Consider the following Java code, which can compile but may result in a type error at runtime:

        Object obj = "I am a string";
        Consumer<String> consumer = (Consumer<String>) obj;
      

In this example:

• The compiler doesn't know that obj is actually a String; it only knows that an Object can be cast to any type (in this case, Object is cast to Consumer<String>).
• At runtime, the Java Virtual Machine recognizes that obj is a String and attempts to cast String to Consumer<String>, resulting in a type error.

Strong vs Weak Typing

Strong Typing

A strongly typed language does not allow implicit changes to data types. To change a data type, explicit casting or functions are required (e.g., str() in Python).

Note: Python is considered a strongly typed language if we don't strictly define strong typing, because Python allows operations like double + int = double (e.g., 1.0 + 2 = 3.0).

Weak Typing

A weakly typed language allows implicit changes between data types.

For example, JavaScript is a weakly typed language.

Data Casting

Suppose a char variable have 1 byte and a int variable have 4 byte. I want to cast int to char in programming language C.

          int number = 300; // In binary: 00000000 00000000 00000001 00101100
          char character = (char) number; // Only last byte is keep, 00101100 = 44 = "," in ASCII
          printf("%c\n", character); // ","
          printf("%d\n", character); // 44