Original article:
Looks like some details were hidden in the publications that even the most proficient users feel ambiguous.
In section 7.7 of the definitive article:
Scala's type system unifies ML modules, object-oriented, and functional
programming. The Dependent Object Types (DOT) family of calculi has been
proposed as a new foundation for Scala and similar languages. Unfortunately, it
is not clear how DOT...
I found the following deduction:
“As the final step, we unify the separate constructs for recursion,
records, and lambda abstractions, into a single notion of object.”
I wonder if this exception is caused by such lossy merging of concepts, should this rule be explicitly defined or even generalised?
LPTK
May 9, 2023, 3:52pm
#2
I have no idea what you are talking about. Section 7.7 of what? Do you have a specific question to ask?
Just added the publication that contains section 7.7.
Sorry I just realised that DOT has several seminal publications. Hope it is clear now
sjrd
May 9, 2023, 10:06pm
#4
I don’t know about DOT, but in the Scala type system, this.type
is the target of the fundamental “as seen from” meta operation on types :
https://scala-lang.org/files/archive/spec/2.13/03-types.html#base-types-and-member-definitions
For a Scala 3 equivalent, I happened to open today a PR to update that section of the spec to Scala 3, which is already quite a bit closer to DOT:
lampepfl:main
← sjrd:spec-type-system-fundamentals
opened 04:09PM - 09 May 23 UTC
There are two fundamental differences between the type sytems of Scala 2 and 3, … which made a fundamental rewrite desirable:
- Scala 2 defines path-dependent types in terms of type projections, whereas Scala 3 is path-dependent first, and has not general type projects.
- Scala 2 has ad hod higher-kinded type parameters and polymorphic type aliases, whereas Scala 3 has first-class type lambdas and is fundamentally higher order.
We therefore rewrite the entire type system section of the spec to be higher-kinded and path-dependent first. In the process, we also revise refined types to better fit the path-dependent nature.
I (sjrd) took the liberty to add myself as a contributor in the index page of the spec, as I believe this constitutes a fundamental contribution to the language specification.
---
The rendered version of the Types chapter can be seen here:
[Types Scala 3.pdf](https://github.com/lampepfl/dotty/files/11433246/Types.Scala.3.pdf)
1 Like
In DOT, this
is just an identifier bound when we create a record. So, this.T
is a path dependent type, for any member type T
. But DOT does not have singleton types. So this.type
is not handled. It would be interesting to see an extension of DOT along these lines.
1 Like
This post was flagged by the community and is temporarily hidden.