DEV Community

stereobooster
stereobooster

Posted on • Originally published at stereobooster.com on

2 1

Are Dart and Java type systems sound?

From Dart docs:

Soundness is about ensuring your program can’t get into certain invalid states. A sound type system means you can never get into a state where an expression evaluates to a value that doesn’t match the expression’s static type. For example, if an expression’s static type is String, at runtime you are guaranteed to only get a string when you evaluate it.

Dart’s type system, like the type systems in Java and C#, is sound. It enforces that soundness using a combination of static checking (compile-time errors) and runtime checks. For example, assigning a String to int is a compile-time error. Casting an Object to a string using as String fails with a runtime error if the object isn’t a string.

This is an interesting point of view - yes type system is sound (based on the provided definition), but at the same time it means that the application can crash due to type error 🤔.

For example, if I would write:

public class HelloWorld{
    public static void main(String []args){
        String[] strs = { 1 };
    }
}
Enter fullscreen mode Exit fullscreen mode

It will not compile:

$javac HelloWorld.java
HelloWorld.java:4: error: incompatible types: int cannot be converted to String
        String[] strs = { 1 };
                          ^
1 error
Enter fullscreen mode Exit fullscreen mode

But this will compile:

public class HelloWorld{
    public static void main(String []args){
        String[] strs = { "1" };
        Object[] objs = strs;
        objs[0] = 1;
        String one = strs[0];
        System.out.println("Hello World");
    }
}
Enter fullscreen mode Exit fullscreen mode

and fail:

$javac HelloWorld.java
$java -Xmx128M -Xms16M HelloWorld
Exception in thread "main" java.lang.ArrayStoreException: java.lang.Integer
    at HelloWorld.main(HelloWorld.java:6)

Enter fullscreen mode Exit fullscreen mode

I feel like something is twisted here.

Can we say that type system is sound, but static analyzer isn't?

Or the other way around - if we can say that relying on dynamic type checks is enough to have a sound type system, can we say that Ruby is sound?

1 + "0"
// TypeError: String can't be coerce into Numeric
Enter fullscreen mode Exit fullscreen mode

See also: Java is Unsound: The Industry Perspective

Top comments (0)

Great read:

Is it Time to go Back to the Monolith?

History repeats itself. Everything old is new again and I’ve been around long enough to see ideas discarded, rediscovered and return triumphantly to overtake the fad. In recent years SQL has made a tremendous comeback from the dead. We love relational databases all over again. I think the Monolith will have its space odyssey moment again. Microservices and serverless are trends pushed by the cloud vendors, designed to sell us more cloud computing resources.

Microservices make very little sense financially for most use cases. Yes, they can ramp down. But when they scale up, they pay the costs in dividends. The increased observability costs alone line the pockets of the “big cloud” vendors.

👋 Kindness is contagious

Please leave a ❤️ or a friendly comment on this post if you found it helpful!

Okay