What is the pros and cons of Dependent Object Types over the other type system?

Hi everyone :grin:. I like the concept of Scala that fuse together math and coding (I love both of it!). I found out that DOT (Dependent Object Type) is the foundation of Scala 3 and research on this topic by reading:

The Essence of Dependent Object Types from EPFL

and

A Simple Soundness Proof for Dependent Object Types

However it is too hard for me to fully understand all of it . Can anyone please explain the pros and cons of the DOT over the other type system of the other programming language?

Welcome to Scala!

Your question opens a very big space to try and cover. Like such a big space, the answer might not be useful to you.

So, can you narrow down the area a bit by saying why you want to know this? And perhaps identify a language or two with which you are familiar upon which one could base the contrast and comparison? That would help make generating an answer much more tractable and concrete which likely would be far more useful to you and to others who end up reading this thread.

Definitely!

At first, from many resources such as dotty fact, essence of scala or stack overflow depict that DOT is heavily researched in the past several years in order to create and improve new scala. (I love this kind of things like how rust has invented Ownerships and Borrowing rules to discard the garbage collector :+1:).

From the resources and papers, my curious is boiled down to 2 main questions.

  • How is DOT related to calculus at all?
  • What is the improvement of the DOT over previous version Scala’s type system ? Like does the performance improving? or Does it solve any persist issues of the previous version?

Given the resources you have already listed, I’m not sure there’s much to add.

For your first bullet, the article, “Essence of Scala”, starts with the “DOT Calculus”. I don’t know where you could find a discussion about how that’s related to the more Math’s general notion of “calculus”. Perhaps someone who was involved in the DOT proofs could show an explicit connection.

For your second bullet, it appears all three articles you cited provide first approximation answers to your questions.

For example, Odersky outlines the elevated expectations of performance improvements because of the resulting simplification of internals. Whether that is from improved type soundness, or the many other Scala 3 adaptations and improvements over Scala 2, or both, it’s not clear. And what benefit would there be from seeking clarification?

Were you intending to use Scala 3? Or are you researching it to consider as an option against other alternatives like TypeScript, Haskell, etc.? Or are you just a compiler theory enthusiast just kicking the Scala compiler tires as opposed to seeking to actually utilize it? Just trying to continue to narrow down what you’re actually seeking as your questions still left a very large abstract surface area.

1 Like

Thanks for the answering :grin:.

It is not for comparison to choose the language for my profession or anything. I love many languages (mostly python, rust and scala!), it has its unique features and capabilities.

Most of the question just comes from my curiosity, it is just interesting (like how Rust introduce new concept!). It is as you said that the resource does point out the benefit, but not in the plain English :sweat_smile:, and that’s why I am trying to seek the answer from the Scala developer or the contributor here.

1 Like

On thing to clarify (in case this was not clear): this is not “Calculus” in the sense of “Differential and Integral Calculus” (i.e., the contents of a “Calculus” course), but in the sense of formal rules for calculating. So DOT Calculus is similar to (indeed perhaps a generalization of) Lambda Calculus in logic.

regards,
Siddhartha

3 Likes

If you mean “calculus” as in the common math class with differentials and integrals, it’s not. “Calculus” is a word with a broader meaning: “a method of computation or calculation in a special notation”. The calculus you’re probably familiar with is “infinitesimal calculus”, but there are many other kinds of calculi, including DOT.

The main improvement from DOT is soundness. For a somewhat hand-wavy intuition, when a type system is sound that means you cannot represent an invalid program within the type system; if it passes the type checker, then it is correct in some sense. It might not be logically correct where it does what you intended, but it is type-correct in that things are what they say they are, and you won’t have an integer when you expected to have a string. In an unsound type system you can have code that passes the type checker but fails at runtime.

2 Likes

Thanks everyone, I get a glimpse of it now.

So, with the new DOT foundation, it is basically safer to code while maintain rich features of the Scala.

3 Likes