はじめに
昨日、 ScalaMatsuri 参加者の一人から、タイトルの用語について、どういう使い分けをされているのかがわからない、といった質問があったので、処理系と言語の区別という観点も踏まえてちょっと整理しておきます。Eugene Yokotaさんから聞いた話としては、Scala 3という用語についてちょっと違う意味合いもあるようなのですが、その辺はツッコミ入れてくださるのではないかと期待しています。
Scala
2019年6月30日現在、普通にScalaといったらプロダクションで普通に使われているScalaの処理系（scalacなど）を指す場合と、その処理系が対象とする言語そのものを指す場合の用法の大まかに二通りがあります。この辺の使い分けは話の文脈に多分に依存していて、たとえば、「Scalaはコンパイルが遅い」「Scala 2.12でコンパイル速度が15%（詳細な数値は忘れました）向上」といったとき、意識していなくても、処理系の方を指していることになります。なぜなら、このとき、Scala「言語」の変化について言っているわけではないですから。一方、「Scala 2.12でSAM type conversionが入った」という話をするとき、主に、言語そのものを指していることになります。標準ライブラリの変化については扱いが難しいですが、どちらかというと言語自体に近いコンテキストになるのではないかと。
Scala 2
これは、1～2年後にリリース予定（要出展）のScala 3と区別する文脈で用いられることが多いです。このときも、「Scala 3ではコンパイルがかなり早くなる」といったときは処理系の話をしていますし、「Scala 3でenumが」とか「implicitについて書き方が変わった（改善された）」というとき、Scala 3（予定）の言語（仕様）について言及しています。
Dotty
これについては若干扱いに困るのですが、基本的には、
で開発されている、Scala 3（予定）の処理系の現在の実装であるものを指すことがほとんどです（Dottyでコンパイルが大幅に早くなった、Dottyでは将来的にTASTYが入る、など）。ただ、「Dottyでenumが入った」「Dottyでimplicit function typeが入った」「Dottyでhogehoge機能が削られた」という話をしているときは、主に言語の話をしているわけです。ちょっとややこしいのは、DottyはScala 3の処理系になることが既に確定していて、おそらくリポジトリ名なども変更されるかと思います。DottyはまだScala 3になっていないので、「Scala 3でenumが入った」というと未来の仕様の話について過去形で話すというおかしなことになってしまいます。「enumが入った」という過去形で言うならDottyというキーワードを使う方が伝わりやすいのかな、という気がします。
DOT calculus
これについては、上記のよりもだいぶわかりやすいです。元々、Odersky先生（および共同研究をしている人たち、あるいは、研究室の大学院生、そこ出身の研究者）は設計の初期段階から、core calculusの研究を同時に進めていました。発表で話したのですが、
- vObj calculus: 2003
- Featherweight Scala: 2006
- DOT calculus 2012-
といった感じです。そして、DOT calculusについては、各論文において、という形ではありますが、明確に定義されているので、それほどややこしいことはありません。ただ、DOTというcore calculusが開発されはじめて、もう10年近くになるわけですが、その間に、望ましい性質を証明できるように細かい部分に手を加えたり、ということがあり、DOTには複数のバージョンがあります（OOPSLA'16におけるDOT、ECOOP'17におけるDOTみたいな表現が妥当かなと思います）。ただ、基本的にはDOTそのものでプロダクションコード開発するわけではないので、最新のDOTに関する論文を追っかけておけばいいです。私は、説明するときには、どの時点でのDOTの話をするのか明記しましたが。
さらに脇道にそれると、本来のDOTより強い性質を証明したいとか色々な動機によって、μDOTとか、kDOTとか。興味があったら調べてみてください。ところで、全然関係ないのですが、ECOOP'17の論文では、Strong Normalizationについて証明されていたのですね（やはりCoqで証明が書かれている模様）。ただ、これはDOTのvariantであるD<:>についてであって、再帰関数や再帰型（など？）を取り除いたもののようです。
さらにさらに脇道にそれると、Scalaのcore calculusについては変遷があったものの、ようやくDOTが決定版になって（性質を証明するための基盤になったというか）、それのvariantで色々証明するということが行われているようです（この辺はもう全然追えていないですが、DOT関連の論文、プログラミング言語系の国際会議に査読通ってるものも少なからずあるので（OOPSLA、ECOOP、POPL、その他？）、その辺によく出席する研究者の方々の方が詳しいのではないかと思ったり）。
というわけで、ざっくりとその辺について説明してみましたが、参考になれば幸いです。
