Scala 3’s type system is based on something called dependent object types / DOT or path dependent types. This isn’t true dependent type theory afaict. The documentation example is:
trait Entry { type Key; val key: Key }
def extractKey(e: Entry): e.Key = e.key // a dependent method
val extractor: (e: Entry) => e.Key = extractKey // a dependent function value
// ^^^^^^^^^^^^^^^^^^^
// a dependent function type
Compare
module type Entry = sig
type key
val x : key
end
let extractor (module E : Entry) : E.key = E.x
Is there any direct comparison of module-dependent functions with Scala 3’s type system?
Scala objects correspond to ML modules, classes to
functors, and interfaces to signatures.
So Scala is kinda like writing programs entirely in OCaml’s module system (except they don’t need wrapper modules for regular values, since they are objects already.) With module-dependent functions in OCaml 5.5, you could instead replace OCaml records with first-class modules entirely to approach the Scala calculus.
As @hyphenrf said, 1ML has been influential on both. DOT however has a focus on allowing recursive references and mixins, to match the OOP and JVM style of programming.
My current best guess is that both these features can be used in similar-ish situations, but that path-dependent types are in general more expressive than module-dependent functions. I’m not fully sure how to pinpoint the difference on concrete examples (and it’s a bit embarrassing given that I’ve helped from the sidelines the work on module-dependent functions), but I have a meta-level argument (warning: type-theory jargon):
The Scala people have a lot of trouble showing that the DOT calculus (the essence of path-dependent types) is actually sound. This was a major research topic about 10 years ago, when people spent a few years looking for a soundness proof. And it was in a restricted case, the full case was still being worked on maybe 5 years ago.
On the other hand, there is an encoding of module-dependent functions into the rest of the OCaml module system. (Basically, every module-dependent function can be turned into a functor.) This was proposed already in the first version of modular implicits years ago (2015?), see section 1.5 of this more recent paper as well.
At this point I would conclude the argument by saying “… and the combination of standard ML functors and first-class modules is well-known to be sound, and to be at the expressivity level of F-omega, so it is easier than path-dependent types”. In fact, yeah, it’s a bit more muddy than that, because OCaml tends to support more things than academic module systems with a soundness proof. But I do believe that the fragment targeted by the translation of module-dependent functions does reasonably fit within F-omega as using in Rossberg’s F-ing module approach, maybe with a few extra bits of formalization on first-class modules (I don’t remember how Russo formalized them, and/or if the more recent work of Clément Blaudeau covers them as well).
To summarize: type soundness of path-dependent types is widely known to be hard. Type soundness of module-dependent functions is believed to be a folklore result. So the first (harder) one is probably more expressive than the second.
(Note: it is actually possible that the ML people are wrong in believing that functors + first-class modules is in F-omega, or that Scala people are wrong in the sense that people with ML-module-system-soundness expertise could think of a nice translation of the dot-calculus into F-omega, so maybe the problem is not as hard as believed. But this would be surprising.)