From 7bb287c936c34aeb50b7e34665de7121c908ff61 Mon Sep 17 00:00:00 2001 From: Allan Renucci Date: Thu, 1 Mar 2018 14:37:43 +0100 Subject: [PATCH 01/23] Blog Post: Announcing Dotty 0.6.0 and 0.7.0-RC1 --- ...8-03-05-seventh-dotty-milestone-release.md | 157 ++++++++++++++++++ 1 file changed, 157 insertions(+) create mode 100644 docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md diff --git a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md new file mode 100644 index 000000000000..250083b301d3 --- /dev/null +++ b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md @@ -0,0 +1,157 @@ +--- +layout: blog-page +title: Announcing Dotty 0.6.0 and 0.7.0-RC1 +author: Allan Renucci +authorImg: /images/allan.jpg +date: 2018-03-05 +--- + +Today, we are excited to release Dotty versions 0.6.0 and 0.7.0-RC1. These releases +serve as a technology preview that demonstrates new language features and the compiler supporting them. + +If you’re not familiar with Dotty, it's a platform to try out new language concepts and compiler +technologies for Scala. The focus is mainly on simplification. We remove extraneous syntax +(e.g. no XML literals), and try to boil down Scala’s types into a smaller set of more fundamental +constructs. The theory behind these constructs is researched in +[DOT](https://infoscience.epfl.ch/record/215280), a calculus for dependent object types. +You can learn more about Dotty on our [website](http://dotty.epfl.ch). + + + +This is our seventh scheduled release according to our [6-week release schedule](/docs/usage/version-numbers.html). +The [previous technology preview](https://github.com/lampepfl/dotty/releases/tag/0.6.0-RC1) focussed +on bug fixes and stability work. + +## What’s new in the 0.7.0-RC1 technology preview? + +### Enums Simplicification [#4003](https://github.com/lampepfl/dotty/pull/4003) +The previously introduced syntax and rules for enum were arguably too complex. We can considerably +simplify them by taking away one capability: that cases can have bodies which can define members. +Arguably, if we choose an ADT decomposition of a problem, it's good style to write all methods using +pattern matching instead of overriding individual cases. So this removes an unnecessary choice. +We now treat enums unequivocally as classes. They can have methods and other statements just like +other classes can. Cases in enums are seen as a form of constructors. We do not need a +distinction between enum class and enum object anymore. Enums can have companion objects just like +normal classes can, of course. + +Let's consider how `Option` can be represented as an enum. Previously using an enum class: +```scala +enum class Option[+T] { + def isDefined: Boolean +} +object Option { + case Some[+T](x: T) { + def isDefined = true + } + case None { + def isDefined = false + } + + def apply[T(x: T): Option[T] = if (x == null) None else Some(x) +} +``` + +And now: +```scala +enum Option[+T] { + case Some(x: T) + case None + + def isDefined: Boolean = this match { + case None => false + case some => true + } +} + +object Option { + def apply[T](x: T): Option[T] = if (x == null) None else Some(x) +} +``` + +You can visit our website for more information about [enumerations](/docs/reference/enums/enums.html) +and how we can use them to model [Algebraic Data Types](/docs/reference/enums/adts.html). + +### Unused Parameters [#3342](https://github.com/lampepfl/dotty/pull/3342) +TODO + +## Trying out Dotty +### Scastie +[Scastie], the online Scala playground, supports Dotty. +This is an easy way to try Dotty without installing anything. + +### sbt +Using sbt 0.13.13 or newer, do: + +```shell +sbt new lampepfl/dotty.g8 +``` + +This will setup a new sbt project with Dotty as compiler. For more details on +using Dotty with sbt, see the +[example project](https://github.com/lampepfl/dotty-example-project). + +### IDE support +It is very easy to start using the Dotty IDE in any Dotty project by following +the [IDE guide](http://dotty.epfl.ch/docs/usage/ide-support.html). + + +### Standalone installation +Releases are available for download on the _Releases_ +section of the Dotty repository: +[https://github.com/lampepfl/dotty/releases](https://github.com/lampepfl/dotty/releases) + +We also provide a [homebrew](https://brew.sh/) package that can be installed by running: + +```shell +brew install lampepfl/brew/dotty +``` + +In case you have already installed Dotty via brew, you should instead update it: + +```shell +brew upgrade dotty +``` + +## Let us know what you think! +If you have questions or any sort of feedback, feel free to send us a message on our +[Gitter channel](https://gitter.im/lampepfl/dotty). If you encounter a bug, please +[open an issue on GitHub](https://github.com/lampepfl/dotty/issues/new). + +## Contributing +Thank you to all the contributors who made this release possible! + +According to `git shortlog -sn --no-merges 0.6.0-RC1..0.7.0-RC1` these are: + +``` +TODO +``` + +If you want to get your hands dirty and contribute to Dotty, now is a good time to get involved! +Head to our [Getting Started page for new contributors](http://dotty.epfl.ch/docs/contributing/getting-started.html), +and have a look at some of the [good first issues](https://github.com/lampepfl/dotty/issues?q=is%3Aissue+is%3Aopen+label%3Aexp%3Anovice). +They make perfect entry-points into hacking on the compiler. + +We are looking forward to having you join the team of contributors. + +## Library authors: Join our community build +Dotty now has a set of widely-used community libraries that are built against every nightly Dotty +snapshot. Currently this includes ScalaPB, algebra, scalatest, scopt and squants. +Join our [community build](https://github.com/lampepfl/dotty-community-build) +to make sure that our regression suite includes your library. + + +[Scastie]: https://scastie.scala-lang.org/?target=dotty + +[@odersky]: https://github.com/odersky +[@DarkDimius]: https://github.com/DarkDimius +[@smarter]: https://github.com/smarter +[@felixmulder]: https://github.com/felixmulder +[@nicolasstucki]: https://github.com/nicolasstucki +[@liufengyun]: https://github.com/liufengyun +[@OlivierBlanvillain]: https://github.com/OlivierBlanvillain +[@biboudis]: https://github.com/biboudis +[@allanrenucci]: https://github.com/allanrenucci +[@Blaisorblade]: https://github.com/Blaisorblade +[@Blaisorblade]: https://github.com/Blaisorblade +[@Duhemm]: https://github.com/duhemm + From bf77e84c2a4843249c5e7cc8e6d1a2ba10764451 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Thu, 1 Mar 2018 14:46:40 +0100 Subject: [PATCH 02/23] Drop dup link --- docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md | 1 - 1 file changed, 1 deletion(-) diff --git a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md index 250083b301d3..aa2e98c17de6 100644 --- a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md +++ b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md @@ -152,6 +152,5 @@ to make sure that our regression suite includes your library. [@biboudis]: https://github.com/biboudis [@allanrenucci]: https://github.com/allanrenucci [@Blaisorblade]: https://github.com/Blaisorblade -[@Blaisorblade]: https://github.com/Blaisorblade [@Duhemm]: https://github.com/duhemm From 86f24d29cc307e12dfe3d8a292573af254b97162 Mon Sep 17 00:00:00 2001 From: Nicolas Stucki Date: Thu, 1 Mar 2018 17:02:17 +0100 Subject: [PATCH 03/23] Add section on `unused` --- ...8-03-05-seventh-dotty-milestone-release.md | 25 +++++++++++++++++-- 1 file changed, 23 insertions(+), 2 deletions(-) diff --git a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md index aa2e98c17de6..31c5111f0bf7 100644 --- a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md +++ b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md @@ -71,8 +71,29 @@ object Option { You can visit our website for more information about [enumerations](/docs/reference/enums/enums.html) and how we can use them to model [Algebraic Data Types](/docs/reference/enums/adts.html). -### Unused Parameters [#3342](https://github.com/lampepfl/dotty/pull/3342) -TODO +### Unused Parameters [#3342](https://github.com/lampepfl/dotty/pull/3342) and remove Phantom types [#3410](https://github.com/lampepfl/dotty/pull/3410) +The keyword `unsued` can be placed on parameters, `val` and `def` to enforce that no reference to +those terms is ever used (recursively). As they are never used, they can safely be removed during compilation. +These have similar semantics as _phantom types_ but with the added advantage that any type can be an unused parameter. They can be used to add implicit type constraints that are only relevant at compilation time. + +```scala +// A function that requires an implicit evidence of type X =:= Y but never uses it. +// The parameter will be removed and the argument will not be evaluated. +def apply(implicit unused ev: X =:= Y) = + foo(ev) // `ev` can be an argument to foo as foo will also never use it +def foo(unused x: X =:= Y) = () +``` + +The previous code will be transformed to the following: + +```scala +def apply() = // unused parameter will be removed + foo() // foo is called without the unused parameter +def foo() = () // unused parameter will be removed +``` + +[Documentation](/docs/reference/unused-parameters.html) + ## Trying out Dotty ### Scastie From bbdd2af202c3f8b6a9388e8911fe8ec29c6a3553 Mon Sep 17 00:00:00 2001 From: Nicolas Stucki Date: Fri, 2 Mar 2018 12:01:43 +0100 Subject: [PATCH 04/23] Rename `unused` to `ghost` --- ...18-03-05-seventh-dotty-milestone-release.md | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md index 31c5111f0bf7..a7b460ca7c8d 100644 --- a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md +++ b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md @@ -71,28 +71,28 @@ object Option { You can visit our website for more information about [enumerations](/docs/reference/enums/enums.html) and how we can use them to model [Algebraic Data Types](/docs/reference/enums/adts.html). -### Unused Parameters [#3342](https://github.com/lampepfl/dotty/pull/3342) and remove Phantom types [#3410](https://github.com/lampepfl/dotty/pull/3410) -The keyword `unsued` can be placed on parameters, `val` and `def` to enforce that no reference to +### Ghost terms [#3342](https://github.com/lampepfl/dotty/pull/3342) and remove Phantom types [#3410](https://github.com/lampepfl/dotty/pull/3410) +The keyword `ghost` can be placed on parameters, `val` and `def` to enforce that no reference to those terms is ever used (recursively). As they are never used, they can safely be removed during compilation. -These have similar semantics as _phantom types_ but with the added advantage that any type can be an unused parameter. They can be used to add implicit type constraints that are only relevant at compilation time. +These have similar semantics as _phantom types_ but with the added advantage that any type can be an ghost parameter. They can be used to add implicit type constraints that are only relevant at compilation time. ```scala // A function that requires an implicit evidence of type X =:= Y but never uses it. // The parameter will be removed and the argument will not be evaluated. -def apply(implicit unused ev: X =:= Y) = +def apply(implicit ghost ev: X =:= Y) = foo(ev) // `ev` can be an argument to foo as foo will also never use it -def foo(unused x: X =:= Y) = () +def foo(ghost x: X =:= Y) = () ``` The previous code will be transformed to the following: ```scala -def apply() = // unused parameter will be removed - foo() // foo is called without the unused parameter -def foo() = () // unused parameter will be removed +def apply() = // ghost parameter will be removed + foo() // foo is called without the ghost parameter +def foo() = () // ghost parameter will be removed ``` -[Documentation](/docs/reference/unused-parameters.html) +[Documentation](/docs/reference/ghost-terms.html) ## Trying out Dotty From 3bd057feae3bb4cef88b43328ef0d80c68023b5d Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Fri, 2 Mar 2018 21:07:57 +0100 Subject: [PATCH 05/23] Small revisions --- .../blog/_posts/2018-03-05-seventh-dotty-milestone-release.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md index a7b460ca7c8d..552e95894636 100644 --- a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md +++ b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md @@ -71,10 +71,10 @@ object Option { You can visit our website for more information about [enumerations](/docs/reference/enums/enums.html) and how we can use them to model [Algebraic Data Types](/docs/reference/enums/adts.html). -### Ghost terms [#3342](https://github.com/lampepfl/dotty/pull/3342) and remove Phantom types [#3410](https://github.com/lampepfl/dotty/pull/3410) +### Ghost terms [#3342](https://github.com/lampepfl/dotty/pull/3342) and removing phantom types [#3410](https://github.com/lampepfl/dotty/pull/3410) The keyword `ghost` can be placed on parameters, `val` and `def` to enforce that no reference to those terms is ever used (recursively). As they are never used, they can safely be removed during compilation. -These have similar semantics as _phantom types_ but with the added advantage that any type can be an ghost parameter. They can be used to add implicit type constraints that are only relevant at compilation time. +These have similar semantics as _phantom types_ but with the added advantage that any type can be a ghost parameter. They can be used to add implicit type constraints that are only relevant at compilation time. ```scala // A function that requires an implicit evidence of type X =:= Y but never uses it. From dde9330641ecbdbf1e3611e3daaf98aec45cf626 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Fri, 2 Mar 2018 21:08:13 +0100 Subject: [PATCH 06/23] Emphasize phantom types are being replaced --- docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md index 552e95894636..2c8b1467286f 100644 --- a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md +++ b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md @@ -74,7 +74,7 @@ and how we can use them to model [Algebraic Data Types](/docs/reference/enums/ad ### Ghost terms [#3342](https://github.com/lampepfl/dotty/pull/3342) and removing phantom types [#3410](https://github.com/lampepfl/dotty/pull/3410) The keyword `ghost` can be placed on parameters, `val` and `def` to enforce that no reference to those terms is ever used (recursively). As they are never used, they can safely be removed during compilation. -These have similar semantics as _phantom types_ but with the added advantage that any type can be a ghost parameter. They can be used to add implicit type constraints that are only relevant at compilation time. +Ghost terms replace _phantom types_: they have similar semantics, but with the added advantage that any type can be a ghost parameter. They can be used to add implicit type constraints that are only relevant at compilation time. ```scala // A function that requires an implicit evidence of type X =:= Y but never uses it. From ffbedef4424aa9565966a60ba3b764482df0d2c6 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Fri, 2 Mar 2018 21:09:14 +0100 Subject: [PATCH 07/23] Fix typos in code snippets Technically `case some =>` works (and binds `some` to `this`) but I don't think this was intended. --- .../blog/_posts/2018-03-05-seventh-dotty-milestone-release.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md index 2c8b1467286f..d60b5d9d8794 100644 --- a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md +++ b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md @@ -47,7 +47,7 @@ object Option { def isDefined = false } - def apply[T(x: T): Option[T] = if (x == null) None else Some(x) + def apply[T](x: T): Option[T] = if (x == null) None else Some(x) } ``` @@ -59,7 +59,7 @@ enum Option[+T] { def isDefined: Boolean = this match { case None => false - case some => true + case Some(_) => true } } From dc81fd349be6ebb8b2a0b675f8697f2d6a4258d3 Mon Sep 17 00:00:00 2001 From: Allan Renucci Date: Sun, 4 Mar 2018 11:00:46 +0100 Subject: [PATCH 08/23] Update ghost section with real life example --- ...8-03-05-seventh-dotty-milestone-release.md | 45 +++++++++++-------- 1 file changed, 27 insertions(+), 18 deletions(-) diff --git a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md index d60b5d9d8794..f8f2aa52f018 100644 --- a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md +++ b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md @@ -39,6 +39,7 @@ Let's consider how `Option` can be represented as an enum. Previously using an e enum class Option[+T] { def isDefined: Boolean } + object Option { case Some[+T](x: T) { def isDefined = true @@ -68,32 +69,40 @@ object Option { } ``` -You can visit our website for more information about [enumerations](/docs/reference/enums/enums.html) -and how we can use them to model [Algebraic Data Types](/docs/reference/enums/adts.html). -### Ghost terms [#3342](https://github.com/lampepfl/dotty/pull/3342) and removing phantom types [#3410](https://github.com/lampepfl/dotty/pull/3410) -The keyword `ghost` can be placed on parameters, `val` and `def` to enforce that no reference to -those terms is ever used (recursively). As they are never used, they can safely be removed during compilation. -Ghost terms replace _phantom types_: they have similar semantics, but with the added advantage that any type can be a ghost parameter. They can be used to add implicit type constraints that are only relevant at compilation time. +For more information about [Enumerations](/docs/reference/enums/enums.html) and how to use them to +model [Algebraic Data Types](/docs/reference/enums/adts.html), visit the respective sections in our +documentation. -```scala -// A function that requires an implicit evidence of type X =:= Y but never uses it. -// The parameter will be removed and the argument will not be evaluated. -def apply(implicit ghost ev: X =:= Y) = - foo(ev) // `ev` can be an argument to foo as foo will also never use it -def foo(ghost x: X =:= Y) = () -``` +### Ghost terms [#3342](https://github.com/lampepfl/dotty/pull/3342) +The `ghost` modifier can be used on parameters, `val` and `def` to enforce that no reference to +those terms is ever used. As they are never used, they can safely be removed during compilation. -The previous code will be transformed to the following: +One particular use case is to add implicit type constraints that are only relevant at compilation +time. For example, let's consider the following implementation of `flatten`. ```scala -def apply() = // ghost parameter will be removed - foo() // foo is called without the ghost parameter -def foo() = () // ghost parameter will be removed +class List[X] { + def flatten[Y](implicit ghost ev: X <:< List[Y]): List[Y] = { + val buffer = new mutable.ListBuffer[Y] + this.foreach(e => buffer ++= e.asInstanceOf[List[Y]]) + buffer.toList + } +} + +List(List(1, 2), List(3)).flatten // List(1, 2, 3) +List(1, 2, 3).flatten // error: Cannot prove that Int <:< List[Y] ``` -[Documentation](/docs/reference/ghost-terms.html) +The implicit evidence `ev` is only used to constrain the type parameter `X` of `List` such that we +can safely cast from `X` to `List[_]`. The usage of the `ghost` modifier ensures that the evidence +is not used and can be safely removed at compilation time. + +For more information, visit the [Ghost Terms](/docs/reference/ghost-terms.html) section of our +documentation. +**Note**: Ghost terms replace _phantom types_: they have similar semantics, but with the added +advantage that any type can be a ghost parameter. See [#3410](https://github.com/lampepfl/dotty/pull/3410). ## Trying out Dotty ### Scastie From a5dcce73a6508baa9cb44f6cc66de2d0beb5ced0 Mon Sep 17 00:00:00 2001 From: Allan Renucci Date: Sun, 4 Mar 2018 11:41:44 +0100 Subject: [PATCH 09/23] Add IDE section and use absolute links (better when read on GitHub) --- ...8-03-05-seventh-dotty-milestone-release.md | 25 ++++++++++++++----- 1 file changed, 19 insertions(+), 6 deletions(-) diff --git a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md index f8f2aa52f018..9bed4a8efee9 100644 --- a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md +++ b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md @@ -18,7 +18,7 @@ You can learn more about Dotty on our [website](http://dotty.epfl.ch). -This is our seventh scheduled release according to our [6-week release schedule](/docs/usage/version-numbers.html). +This is our seventh scheduled release according to our [6-week release schedule](http://dotty.epfl.ch/docs/usage/version-numbers.html). The [previous technology preview](https://github.com/lampepfl/dotty/releases/tag/0.6.0-RC1) focussed on bug fixes and stability work. @@ -70,9 +70,10 @@ object Option { ``` -For more information about [Enumerations](/docs/reference/enums/enums.html) and how to use them to -model [Algebraic Data Types](/docs/reference/enums/adts.html), visit the respective sections in our -documentation. +For more information about [Enumerations](http://dotty.epfl.ch/docs/reference/enums/enums.html) +and how to use them to model [Algebraic Data Types](http://dotty.epfl.ch/docs/reference/enums/adts.html), +visit the respective sections in our documentation. + ### Ghost terms [#3342](https://github.com/lampepfl/dotty/pull/3342) The `ghost` modifier can be used on parameters, `val` and `def` to enforce that no reference to @@ -98,12 +99,24 @@ The implicit evidence `ev` is only used to constrain the type parameter `X` of ` can safely cast from `X` to `List[_]`. The usage of the `ghost` modifier ensures that the evidence is not used and can be safely removed at compilation time. -For more information, visit the [Ghost Terms](/docs/reference/ghost-terms.html) section of our -documentation. +For more information, visit the [Ghost Terms](http://dotty.epfl.ch/docs/reference/ghost-terms.html) +section of our documentation. **Note**: Ghost terms replace _phantom types_: they have similar semantics, but with the added advantage that any type can be a ghost parameter. See [#3410](https://github.com/lampepfl/dotty/pull/3410). + +### Improved IDE support [#3960](https://github.com/lampepfl/dotty/pull/3960) +The Dotty language server now supports context sensitive IDE completions. Completions now include +local and imported definitions. Members completions take possible implicit conversions into account. + + + +We also improved the `find references` functionality. It is more robust and much faster! + +Try it out in [Visual Studio Code](http://dotty.epfl.ch/docs/usage/ide-support.html)! + + ## Trying out Dotty ### Scastie [Scastie], the online Scala playground, supports Dotty. From ccb1dae08a61924c51fea10e475cbabf5d8300a5 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sun, 4 Mar 2018 13:02:24 +0100 Subject: [PATCH 10/23] List GADT issues fixed --- .../2018-03-05-seventh-dotty-milestone-release.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md index 9bed4a8efee9..6d02778d4399 100644 --- a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md +++ b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md @@ -116,6 +116,18 @@ We also improved the `find references` functionality. It is more robust and much Try it out in [Visual Studio Code](http://dotty.epfl.ch/docs/usage/ide-support.html)! +### Improvements in GADT type inference + +XXX add examples. +We have fixed multiple bugs about GADT type checking and exhaustiveness checking, especially for invariant GADTs, including +[#1754](https://github.com/lampepfl/dotty/issues/1754), +[#3645](https://github.com/lampepfl/dotty/issues/3645) +[#3999](https://github.com/lampepfl/dotty/issues/3999) +and improved handling of matches using repeated type variables +[#4030](https://github.com/lampepfl/dotty/issues/4030). We have also made +error messages more informative [#3990](https://github.com/lampepfl/dotty/pull/3990). +Fixes to covariant GADTs ([#3989](https://github.com/lampepfl/dotty/issues/3989)/ +[#4013](https://github.com/lampepfl/dotty/pull/4013)) have been deferred to next release. ## Trying out Dotty ### Scastie From a18f371f4b3ec92655ec4ca1eac711a2d779cd3e Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sun, 4 Mar 2018 16:34:32 +0100 Subject: [PATCH 11/23] Small example of GADTs WIP --- .../2018-03-05-seventh-dotty-milestone-release.md | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md index 6d02778d4399..3a50c286a03d 100644 --- a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md +++ b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md @@ -118,10 +118,19 @@ Try it out in [Visual Studio Code](http://dotty.epfl.ch/docs/usage/ide-support.h ### Improvements in GADT type inference -XXX add examples. +GADTs are case class hierarchies similar to this one: +```scala +sealed trait Expr[T] +case class IntExpr(i: Int) extends Expr[Int] +case class BoolExpr(b: Boolean) extends Expr[Boolean] +``` +where different constructors, such as `IntExpr` and `BoolExpr`, pass different type argument to the super trait. Hence, typechecking a pattern match on `v: Expr[T]` requires special care: for instance, if `v = IntExpr(5)` then `T` must be `Int`. + + + We have fixed multiple bugs about GADT type checking and exhaustiveness checking, especially for invariant GADTs, including [#1754](https://github.com/lampepfl/dotty/issues/1754), -[#3645](https://github.com/lampepfl/dotty/issues/3645) +[#3645](https://github.com/lampepfl/dotty/issues/3645), [#3999](https://github.com/lampepfl/dotty/issues/3999) and improved handling of matches using repeated type variables [#4030](https://github.com/lampepfl/dotty/issues/4030). We have also made From ae8e102a7dae28234497fa5b38f5306ee165cb9f Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sun, 4 Mar 2018 21:42:33 +0100 Subject: [PATCH 12/23] Add proper GADT example, adapted from #3666 The example showcases both https://github.com/lampepfl/dotty/issues/3666 and https://github.com/lampepfl/dotty/issues/1754. --- ...8-03-05-seventh-dotty-milestone-release.md | 57 ++++++++++++++++--- 1 file changed, 48 insertions(+), 9 deletions(-) diff --git a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md index 3a50c286a03d..43022ffa13fc 100644 --- a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md +++ b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md @@ -118,23 +118,62 @@ Try it out in [Visual Studio Code](http://dotty.epfl.ch/docs/usage/ide-support.h ### Improvements in GADT type inference -GADTs are case class hierarchies similar to this one: +GADT typechecking is an advanced feature that got significantly improved in this +release. GADTs are case class hierarchies similar to this one: + ```scala -sealed trait Expr[T] -case class IntExpr(i: Int) extends Expr[Int] -case class BoolExpr(b: Boolean) extends Expr[Boolean] +sealed trait Exp[T] +case class IntLit(n: Int) extends Exp[Int] +case class BooleanLit(b: Boolean) extends Exp[Boolean] + +case class GenLit[T](t: T) extends Exp[T] +case class Plus(e1: Exp[Int], e2: Exp[Int]) extends Exp[Int] +case class Fun[S, T](f: Exp[S] => Exp[T]) extends Exp[S => T] +case class App[T, U](f: Exp[T => U], e: Exp[T]) extends Exp[U] ``` -where different constructors, such as `IntExpr` and `BoolExpr`, pass different type argument to the super trait. Hence, typechecking a pattern match on `v: Expr[T]` requires special care: for instance, if `v = IntExpr(5)` then `T` must be `Int`. - +where different constructors, such as `IntLit` and `BooleanLit`, pass different type argument to the super trait. Hence, typechecking a pattern match on `v: Exp[T]` requires special care: for instance, if `v = IntLit(5)` then `T` must be `Int`. This enables writing a typed interpreter `eval[T](e: Exp[T]): T`. In each pattern matching branch + +```scala +object Interpreter { + def eval[T](e: Exp[T]): T = e match { + case IntLit(n) => // Here T = Int and n: Int + n + case BooleanLit(b) => // Similarly, here T = Boolean and b: Boolean + b + + case GenLit(t) => //Here t: T + + // the next line is an error, but was allowed before the fix to https://github.com/lampepfl/dotty/issues/1754: + //val w: GenLit[Nothing] = w + + t + + case Plus(e1, e2) => + // Here T = Int and e1, e2: Exp[Int] + eval(e1) + eval(e2) + + // The next cases triggered warnings before the fix to + // https://github.com/lampepfl/dotty/issues/3666 + + case f: Fun[s, t] => // Here T = s => t + (v: s) => eval(f.f(GenLit(v))) + + case App(f, e) => // Here f: Exp[s, T] and e: Exp[s] + eval(f)(eval(e)) + } +} +``` +Earlier Dotty releases had issues typechecking such interpreters. We have fixed multiple bugs about GADT type checking and exhaustiveness checking, especially for invariant GADTs, including +[#3666](https://github.com/lampepfl/dotty/issues/3666), [#1754](https://github.com/lampepfl/dotty/issues/1754), [#3645](https://github.com/lampepfl/dotty/issues/3645), -[#3999](https://github.com/lampepfl/dotty/issues/3999) and improved handling of matches using repeated type variables -[#4030](https://github.com/lampepfl/dotty/issues/4030). We have also made -error messages more informative [#3990](https://github.com/lampepfl/dotty/pull/3990). +[#4030](https://github.com/lampepfl/dotty/issues/4030). +More test cases appear in [#3999](https://github.com/lampepfl/dotty/pull/3999). +We have also made error messages more informative [#3990](https://github.com/lampepfl/dotty/pull/3990). Fixes to covariant GADTs ([#3989](https://github.com/lampepfl/dotty/issues/3989)/ [#4013](https://github.com/lampepfl/dotty/pull/4013)) have been deferred to next release. From 2fdb46d83805b1f168b55961f36dedf2bd597008 Mon Sep 17 00:00:00 2001 From: Allan Renucci Date: Mon, 5 Mar 2018 14:12:12 +0100 Subject: [PATCH 13/23] Rename ghost parameter to erased --- ...2018-03-05-seventh-dotty-milestone-release.md | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md index 43022ffa13fc..bb8bd93e8ca2 100644 --- a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md +++ b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md @@ -24,7 +24,7 @@ on bug fixes and stability work. ## What’s new in the 0.7.0-RC1 technology preview? -### Enums Simplicification [#4003](https://github.com/lampepfl/dotty/pull/4003) +### Enum Simplification [#4003](https://github.com/lampepfl/dotty/pull/4003) The previously introduced syntax and rules for enum were arguably too complex. We can considerably simplify them by taking away one capability: that cases can have bodies which can define members. Arguably, if we choose an ADT decomposition of a problem, it's good style to write all methods using @@ -75,8 +75,8 @@ and how to use them to model [Algebraic Data Types](http://dotty.epfl.ch/docs/re visit the respective sections in our documentation. -### Ghost terms [#3342](https://github.com/lampepfl/dotty/pull/3342) -The `ghost` modifier can be used on parameters, `val` and `def` to enforce that no reference to +### Erased terms [#3342](https://github.com/lampepfl/dotty/pull/3342) +The `erased` modifier can be used on parameters, `val` and `def` to enforce that no reference to those terms is ever used. As they are never used, they can safely be removed during compilation. One particular use case is to add implicit type constraints that are only relevant at compilation @@ -84,7 +84,7 @@ time. For example, let's consider the following implementation of `flatten`. ```scala class List[X] { - def flatten[Y](implicit ghost ev: X <:< List[Y]): List[Y] = { + def flatten[Y](implicit erased ev: X <:< List[Y]): List[Y] = { val buffer = new mutable.ListBuffer[Y] this.foreach(e => buffer ++= e.asInstanceOf[List[Y]]) buffer.toList @@ -96,14 +96,14 @@ List(1, 2, 3).flatten // error: Cannot prove that Int <:< List[Y] ``` The implicit evidence `ev` is only used to constrain the type parameter `X` of `List` such that we -can safely cast from `X` to `List[_]`. The usage of the `ghost` modifier ensures that the evidence +can safely cast from `X` to `List[_]`. The usage of the `erased` modifier ensures that the evidence is not used and can be safely removed at compilation time. -For more information, visit the [Ghost Terms](http://dotty.epfl.ch/docs/reference/ghost-terms.html) +For more information, visit the [Erased Terms](http://dotty.epfl.ch/docs/reference/erased-terms.html) section of our documentation. -**Note**: Ghost terms replace _phantom types_: they have similar semantics, but with the added -advantage that any type can be a ghost parameter. See [#3410](https://github.com/lampepfl/dotty/pull/3410). +**Note**: Erased terms replace _phantom types_: they have similar semantics, but with the added +advantage that any type can be an erased parameter. See [#3410](https://github.com/lampepfl/dotty/pull/3410). ### Improved IDE support [#3960](https://github.com/lampepfl/dotty/pull/3960) From 5c4fac2ac722467cddadfd87bd57b5d9205a6267 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Mon, 5 Mar 2018 14:51:42 +0100 Subject: [PATCH 14/23] Fix code snippet, thanks to Allan for pointing it out --- .../_posts/2018-03-05-seventh-dotty-milestone-release.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md index bb8bd93e8ca2..35ea2b998730 100644 --- a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md +++ b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md @@ -142,12 +142,12 @@ object Interpreter { case BooleanLit(b) => // Similarly, here T = Boolean and b: Boolean b - case GenLit(t) => //Here t: T + case gl: GenLit[_] => // Here in fact gl: GenLit[T] - // the next line is an error, but was allowed before the fix to https://github.com/lampepfl/dotty/issues/1754: - //val w: GenLit[Nothing] = w + // the next line was incorrectly allowed before the fix to https://github.com/lampepfl/dotty/issues/1754: + //val gl1: GenLit[Nothing] = gl - t + gl.t case Plus(e1, e2) => // Here T = Int and e1, e2: Exp[Int] From 88e97bd2c9d123c48285bc4a28fbd1568338aabd Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Mon, 5 Mar 2018 15:07:09 +0100 Subject: [PATCH 15/23] Drop BooleanLit --- .../_posts/2018-03-05-seventh-dotty-milestone-release.md | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md index 35ea2b998730..f7777e001e40 100644 --- a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md +++ b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md @@ -124,7 +124,6 @@ release. GADTs are case class hierarchies similar to this one: ```scala sealed trait Exp[T] case class IntLit(n: Int) extends Exp[Int] -case class BooleanLit(b: Boolean) extends Exp[Boolean] case class GenLit[T](t: T) extends Exp[T] case class Plus(e1: Exp[Int], e2: Exp[Int]) extends Exp[Int] @@ -132,15 +131,13 @@ case class Fun[S, T](f: Exp[S] => Exp[T]) extends Exp[S => T] case class App[T, U](f: Exp[T => U], e: Exp[T]) extends Exp[U] ``` -where different constructors, such as `IntLit` and `BooleanLit`, pass different type argument to the super trait. Hence, typechecking a pattern match on `v: Exp[T]` requires special care: for instance, if `v = IntLit(5)` then `T` must be `Int`. This enables writing a typed interpreter `eval[T](e: Exp[T]): T`. In each pattern matching branch +where different constructors, such as `IntLit` and `Fun`, pass different type argument to the super trait. Hence, typechecking a pattern match on `v: Exp[T]` requires special care: for instance, if `v = IntLit(5)` then `T` must be `Int`. This enables writing a typed interpreter `eval[T](e: Exp[T]): T`. In each pattern matching branch ```scala object Interpreter { def eval[T](e: Exp[T]): T = e match { case IntLit(n) => // Here T = Int and n: Int n - case BooleanLit(b) => // Similarly, here T = Boolean and b: Boolean - b case gl: GenLit[_] => // Here in fact gl: GenLit[T] From 5d9440abfbea94401df1f43eaff954c95ca56f17 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Mon, 5 Mar 2018 15:10:35 +0100 Subject: [PATCH 16/23] Revise GADT text --- docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md index f7777e001e40..a3e14a8de5b6 100644 --- a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md +++ b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md @@ -131,7 +131,7 @@ case class Fun[S, T](f: Exp[S] => Exp[T]) extends Exp[S => T] case class App[T, U](f: Exp[T => U], e: Exp[T]) extends Exp[U] ``` -where different constructors, such as `IntLit` and `Fun`, pass different type argument to the super trait. Hence, typechecking a pattern match on `v: Exp[T]` requires special care: for instance, if `v = IntLit(5)` then `T` must be `Int`. This enables writing a typed interpreter `eval[T](e: Exp[T]): T`. In each pattern matching branch +where different constructors, such as `IntLit` and `Fun`, pass different type argument to the super trait. Hence, typechecking a pattern match on `v: Exp[T]` requires special care: for instance, if `v = IntLit(5)` then the typechecker must realize that `T` must be `Int`. This enables writing a typed interpreter `eval[T](e: Exp[T]): T`, where say the `IntLit` branch can return an `Int`: ```scala object Interpreter { @@ -169,7 +169,6 @@ We have fixed multiple bugs about GADT type checking and exhaustiveness checking [#3645](https://github.com/lampepfl/dotty/issues/3645), and improved handling of matches using repeated type variables [#4030](https://github.com/lampepfl/dotty/issues/4030). -More test cases appear in [#3999](https://github.com/lampepfl/dotty/pull/3999). We have also made error messages more informative [#3990](https://github.com/lampepfl/dotty/pull/3990). Fixes to covariant GADTs ([#3989](https://github.com/lampepfl/dotty/issues/3989)/ [#4013](https://github.com/lampepfl/dotty/pull/4013)) have been deferred to next release. From 60066500fd66ef9dd322effe23c12e2ec6eda3a7 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Mon, 5 Mar 2018 15:14:10 +0100 Subject: [PATCH 17/23] Address review, point out Scalac had issues --- docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md index a3e14a8de5b6..8115fa83b12e 100644 --- a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md +++ b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md @@ -162,7 +162,7 @@ object Interpreter { } ``` -Earlier Dotty releases had issues typechecking such interpreters. +Earlier Scalac and Dotty releases had issues typechecking such interpreters. We have fixed multiple bugs about GADT type checking and exhaustiveness checking, especially for invariant GADTs, including [#3666](https://github.com/lampepfl/dotty/issues/3666), [#1754](https://github.com/lampepfl/dotty/issues/1754), From cf9db16fd34f0f073413db4bc41f33ec0e3a8d0c Mon Sep 17 00:00:00 2001 From: Allan Renucci Date: Tue, 6 Mar 2018 11:26:24 +0100 Subject: [PATCH 18/23] Polishing --- ...8-03-05-seventh-dotty-milestone-release.md | 23 ++++++++----------- 1 file changed, 10 insertions(+), 13 deletions(-) diff --git a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md index 8115fa83b12e..29f04e3f52cc 100644 --- a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md +++ b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md @@ -126,12 +126,14 @@ sealed trait Exp[T] case class IntLit(n: Int) extends Exp[Int] case class GenLit[T](t: T) extends Exp[T] -case class Plus(e1: Exp[Int], e2: Exp[Int]) extends Exp[Int] case class Fun[S, T](f: Exp[S] => Exp[T]) extends Exp[S => T] case class App[T, U](f: Exp[T => U], e: Exp[T]) extends Exp[U] ``` -where different constructors, such as `IntLit` and `Fun`, pass different type argument to the super trait. Hence, typechecking a pattern match on `v: Exp[T]` requires special care: for instance, if `v = IntLit(5)` then the typechecker must realize that `T` must be `Int`. This enables writing a typed interpreter `eval[T](e: Exp[T]): T`, where say the `IntLit` branch can return an `Int`: +where different constructors, such as `IntLit` and `Fun`, pass different type argument to the super +trait. Hence, typechecking a pattern match on `v: Exp[T]` requires special care. For instance, if +`v = IntLit(5)` then the typechecker must realize that `T` must be `Int`. This enables writing a +typed interpreter `eval[T](e: Exp[T]): T`, where say the `IntLit` branch can return an `Int`: ```scala object Interpreter { @@ -140,17 +142,12 @@ object Interpreter { n case gl: GenLit[_] => // Here in fact gl: GenLit[T] - - // the next line was incorrectly allowed before the fix to https://github.com/lampepfl/dotty/issues/1754: - //val gl1: GenLit[Nothing] = gl + // the next line was incorrectly allowed before the fix to https://github.com/lampepfl/dotty/issues/1754 + // val gl1: GenLit[Nothing] = gl gl.t - case Plus(e1, e2) => - // Here T = Int and e1, e2: Exp[Int] - eval(e1) + eval(e2) - - // The next cases triggered warnings before the fix to + // The next cases triggered spurious warnings before the fix to // https://github.com/lampepfl/dotty/issues/3666 case f: Fun[s, t] => // Here T = s => t @@ -163,13 +160,13 @@ object Interpreter { ``` Earlier Scalac and Dotty releases had issues typechecking such interpreters. -We have fixed multiple bugs about GADT type checking and exhaustiveness checking, especially for invariant GADTs, including +We fixed multiple bugs about GADT type checking and exhaustiveness checking, including [#3666](https://github.com/lampepfl/dotty/issues/3666), [#1754](https://github.com/lampepfl/dotty/issues/1754), [#3645](https://github.com/lampepfl/dotty/issues/3645), -and improved handling of matches using repeated type variables [#4030](https://github.com/lampepfl/dotty/issues/4030). -We have also made error messages more informative [#3990](https://github.com/lampepfl/dotty/pull/3990). +Error messages are now more informative [#3990](https://github.com/lampepfl/dotty/pull/3990). + Fixes to covariant GADTs ([#3989](https://github.com/lampepfl/dotty/issues/3989)/ [#4013](https://github.com/lampepfl/dotty/pull/4013)) have been deferred to next release. From 8e29d895a959df115086e04a46f3c213ddb64c67 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Tue, 6 Mar 2018 11:53:50 +0100 Subject: [PATCH 19/23] Address review comment --- .../blog/_posts/2018-03-05-seventh-dotty-milestone-release.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md index 29f04e3f52cc..81e4d224fe42 100644 --- a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md +++ b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md @@ -159,8 +159,8 @@ object Interpreter { } ``` -Earlier Scalac and Dotty releases had issues typechecking such interpreters. -We fixed multiple bugs about GADT type checking and exhaustiveness checking, including +Scala 2 and Dotty have issues typechecking such interpreters. +In this release we fixed multiple bugs about GADT type checking and exhaustiveness checking, including [#3666](https://github.com/lampepfl/dotty/issues/3666), [#1754](https://github.com/lampepfl/dotty/issues/1754), [#3645](https://github.com/lampepfl/dotty/issues/3645), From 61e7829ada759256dd253b5fc8746fc4e5369ad1 Mon Sep 17 00:00:00 2001 From: Allan Renucci Date: Tue, 6 Mar 2018 11:57:26 +0100 Subject: [PATCH 20/23] Add contributors --- ...8-03-05-seventh-dotty-milestone-release.md | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md index 81e4d224fe42..3d8f60a51a7e 100644 --- a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md +++ b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md @@ -216,10 +216,25 @@ If you have questions or any sort of feedback, feel free to send us a message on ## Contributing Thank you to all the contributors who made this release possible! -According to `git shortlog -sn --no-merges 0.6.0-RC1..0.7.0-RC1` these are: +According to `git shortlog -sn --no-merges 0.6.0..0.7.0-RC1` these are: ``` -TODO + 182 Martin Odersky + 94 Nicolas Stucki + 48 Olivier Blanvillain + 38 liu fengyun + 16 Allan Renucci + 15 Guillaume Martres + 11 Aggelos Biboudis + 5 Abel Nieto + 5 Paolo G. Giarrusso + 4 Fengyun Liu + 2 Georg Schmid + 1 Jonathan Skowera + 1 Fedor Shiriaev + 1 Alexander Slesarenko + 1 benkobalog + 1 Jimin Hsieh ``` If you want to get your hands dirty and contribute to Dotty, now is a good time to get involved! From b636b849d4f6f757d2282f132149d580b97dd203 Mon Sep 17 00:00:00 2001 From: Guillaume Martres Date: Tue, 6 Mar 2018 13:01:49 +0100 Subject: [PATCH 21/23] Rewritten GADT section --- ...8-03-05-seventh-dotty-milestone-release.md | 99 +++++++++++-------- 1 file changed, 56 insertions(+), 43 deletions(-) diff --git a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md index 3d8f60a51a7e..fb08adea3003 100644 --- a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md +++ b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md @@ -116,59 +116,72 @@ We also improved the `find references` functionality. It is more robust and much Try it out in [Visual Studio Code](http://dotty.epfl.ch/docs/usage/ide-support.html)! -### Improvements in GADT type inference - -GADT typechecking is an advanced feature that got significantly improved in this -release. GADTs are case class hierarchies similar to this one: +### Better and safer types in pattern matching (improved GADT support) +Consider the following implementation of an evaluator for a very simple +language containing only integer literals (`Lit`) and pairs (`Pair`): ```scala -sealed trait Exp[T] -case class IntLit(n: Int) extends Exp[Int] - -case class GenLit[T](t: T) extends Exp[T] -case class Fun[S, T](f: Exp[S] => Exp[T]) extends Exp[S => T] -case class App[T, U](f: Exp[T => U], e: Exp[T]) extends Exp[U] +sealed trait Exp +case class Lit(value: Int) extends Exp +case class Pair(fst: Exp, snd: Exp) extends Exp + +object Evaluator { + def eval(e: Exp): Any = e match { + case Lit(x) => + x + case Pair(a, b) => + (eval(a), eval(b)) + } + def main(args: Array[String]): Unit = { + println(eval(Lit(1))) // 1 + println(eval(Pair(Pair(Lit(1), Lit(2)), Lit(3)))) // ((1,2),3) + } +} ``` -where different constructors, such as `IntLit` and `Fun`, pass different type argument to the super -trait. Hence, typechecking a pattern match on `v: Exp[T]` requires special care. For instance, if -`v = IntLit(5)` then the typechecker must realize that `T` must be `Int`. This enables writing a -typed interpreter `eval[T](e: Exp[T]): T`, where say the `IntLit` branch can return an `Int`: +This code is correct but it's not very type-safe since `eval` returns a value +of type `Any`, we can do better by adding a type parameter to `Exp` that +represents the result type of evaluating expression: ```scala -object Interpreter { - def eval[T](e: Exp[T]): T = e match { - case IntLit(n) => // Here T = Int and n: Int - n - - case gl: GenLit[_] => // Here in fact gl: GenLit[T] - // the next line was incorrectly allowed before the fix to https://github.com/lampepfl/dotty/issues/1754 - // val gl1: GenLit[Nothing] = gl - - gl.t - - // The next cases triggered spurious warnings before the fix to - // https://github.com/lampepfl/dotty/issues/3666 - - case f: Fun[s, t] => // Here T = s => t - (v: s) => eval(f.f(GenLit(v))) +sealed trait Exp[T] +case class Lit(value: Int) extends Exp[Int] +case class Pair[A, B](fst: Exp[A], snd: Exp[B]) extends Exp[(A, B)] - case App(f, e) => // Here f: Exp[s, T] and e: Exp[s] - eval(f)(eval(e)) - } +object Evaluator { + def eval[T](e: Exp[T]): T = e match { + case Lit(x) => + // In this case, T = Int + x + case Pair(a, b) => + // In this case, T = (A, B) where A is the type of a and B is the type of b + (eval(a), eval(b)) } ``` -Scala 2 and Dotty have issues typechecking such interpreters. -In this release we fixed multiple bugs about GADT type checking and exhaustiveness checking, including -[#3666](https://github.com/lampepfl/dotty/issues/3666), -[#1754](https://github.com/lampepfl/dotty/issues/1754), -[#3645](https://github.com/lampepfl/dotty/issues/3645), -[#4030](https://github.com/lampepfl/dotty/issues/4030). -Error messages are now more informative [#3990](https://github.com/lampepfl/dotty/pull/3990). - -Fixes to covariant GADTs ([#3989](https://github.com/lampepfl/dotty/issues/3989)/ -[#4013](https://github.com/lampepfl/dotty/pull/4013)) have been deferred to next release. +Now the expression `Pair(Pair(Lit(1), Lit(2)), Lit(3)))` has type `Exp[((Int, +Int), Int)]` and calling `eval` on it will return a value of type `((Int, +Int), Int)` instead of `Any`. + +Something subtle is going on in the definition of `eval` here: its result type +is `T` which is a type parameter that could be instantiated to anything, and +yet in the `Lit` case we are able to return a value of type `Int`, and in the +`Pair` case a value of a tuple type. In each case the typechecker has been able +to constrain the type of `T` through unification (e.g. if `e` matches `Lit(x)` +then `Lit` is a subtype of `Exp[T]`, so `T` must be equal to `Int`). This is +usually referred to as **GADT support** in Scala since it closely mirrors the +behavior of [Generalized Algebraic Data +Types](https://en.wikipedia.org/wiki/Generalized_algebraic_data_type) in +Haskell and other languages. + +GADTs have been a part of Scala for a long time, but in Dotty 0.7.0-RC1 we +significantly improved their implementation to catch more issues at +compile-time. For example, writing `(eval(a), eval(a))` instead of `(eval(a), +(eval(b)))` in the example above should be an error, but it was not caught by +Scala 2 or previous versions of Dotty, whereas we now get a type mismatch error +as expected. More work remains to be done to fix the remaining [GADT-related +issues](https://github.com/lampepfl/dotty/issues?utf8=%E2%9C%93&q=is%3Aissue+is%3Aopen+gadt), +but so far no show-stopper has been found. ## Trying out Dotty ### Scastie From 022669325fe11b1e6be0ce3e3e5b7fdc0f44009e Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Tue, 6 Mar 2018 14:07:36 +0100 Subject: [PATCH 22/23] Fix typos --- .../_posts/2018-03-05-seventh-dotty-milestone-release.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md index fb08adea3003..340b8a134dbd 100644 --- a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md +++ b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md @@ -141,7 +141,7 @@ object Evaluator { This code is correct but it's not very type-safe since `eval` returns a value of type `Any`, we can do better by adding a type parameter to `Exp` that -represents the result type of evaluating expression: +represents the result type of evaluating the expression: ```scala sealed trait Exp[T] @@ -156,6 +156,7 @@ object Evaluator { case Pair(a, b) => // In this case, T = (A, B) where A is the type of a and B is the type of b (eval(a), eval(b)) + } } ``` @@ -177,7 +178,7 @@ Haskell and other languages. GADTs have been a part of Scala for a long time, but in Dotty 0.7.0-RC1 we significantly improved their implementation to catch more issues at compile-time. For example, writing `(eval(a), eval(a))` instead of `(eval(a), -(eval(b)))` in the example above should be an error, but it was not caught by +eval(b))` in the example above should be an error, but it was not caught by Scala 2 or previous versions of Dotty, whereas we now get a type mismatch error as expected. More work remains to be done to fix the remaining [GADT-related issues](https://github.com/lampepfl/dotty/issues?utf8=%E2%9C%93&q=is%3Aissue+is%3Aopen+gadt), From 5dcf78927ca332c00ceb4bba434460d1004a1a3a Mon Sep 17 00:00:00 2001 From: Allan Renucci Date: Tue, 6 Mar 2018 14:17:02 +0100 Subject: [PATCH 23/23] Polishing --- .../2018-03-05-seventh-dotty-milestone-release.md | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md index 340b8a134dbd..0b43d4d3b22f 100644 --- a/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md +++ b/docs/blog/_posts/2018-03-05-seventh-dotty-milestone-release.md @@ -132,10 +132,9 @@ object Evaluator { case Pair(a, b) => (eval(a), eval(b)) } - def main(args: Array[String]): Unit = { - println(eval(Lit(1))) // 1 - println(eval(Pair(Pair(Lit(1), Lit(2)), Lit(3)))) // ((1,2),3) - } + + eval(Lit(1)) // 1: Any + eval(Pair(Pair(Lit(1), Lit(2)), Lit(3))) // ((1, 2), 3) : Any } ``` @@ -157,6 +156,9 @@ object Evaluator { // In this case, T = (A, B) where A is the type of a and B is the type of b (eval(a), eval(b)) } + + eval(Lit(1)) // 1: Int + eval(Pair(Pair(Lit(1), Lit(2)), Lit(3))) // ((1, 2), 3) : ((Int, Int), Int) } ```