Add posts from dotty-website

Author: felixmulder

docs/blog/2015-10-23-dotty-compiler-bootstraps.md

@@ -1,11 +1,10 @@
 ---
-layout: blog
-post-type: blog
-by: Martin Odersky and Dmitry Petrashko
-title: We Got LiftOff! The Dotty Compiler for Scala Bootstraps.
+author: Martin Odersky and Dmitry Petrashko
+title: "We got liftoff!"
+subTitle: The Dotty compiler for Scala bootstraps.
 ---
 
-## We Got Liftoff!
+## We got liftoff!
 
 The [Dotty project](https://github.com/lampepfl/dotty)
 is a platform to develop new technology for Scala
@@ -14,7 +13,7 @@ Its compiler is a new design intended to reflect the
 lessons we learned from work with the Scala compiler. A clean redesign
 today will let us iterate faster with new ideas in the future.
 
-Today we reached an important milestone: The Dotty compiler can
+Today we reached an important milestone: the Dotty compiler can
 compile itself, and the compiled compiler can act as a drop-in for the
 original one. This is what one calls a *bootstrap*.
 
@@ -35,29 +34,36 @@ go unnoticed, precisely because every part of a compiler feeds into
 other parts and all together are necessary to produce a correct
 translation.
 
-## Are We Done Yet?
+## Are we done yet?
 
 Far from it! The compiler is still very rough. A lot more work is
 needed to
 
  - make it more robust, in particular when analyzing incorrect programs,
  - improve error messages and warnings,
  - improve the efficiency of some of the generated code,
+ - improve compilation speed,
  - embed it in external tools such as sbt, REPL, IDEs,
  - remove restrictions on what Scala code can be compiled,
  - help in migrating Scala code that will have to be changed.
 
-## What Are the Next Steps?
+## What are the next steps?
 
 Over the coming weeks and months, we plan to work on the following topics:
 
  - Make snapshot releases.
- - Get the Scala standard library to compile.
  - Work on SBT integration of the compiler.
  - Work on IDE support.
  - Investigate the best way to obtaining a REPL.
  - Work on the build infrastructure.
 
-If you want to get your hands dirty with any of this, now is a good moment to get involved!
-To get started: <https://github.com/lampepfl/dotty>.
+If you want to get your hands dirty with any of this, now is a good
+moment to get involved! Join the team of contributors, including
+Dmitry Petrashko ([@DarkDimius](https://github.com/DarkDimius)),
+Guillaume Martres ([@smarter](https://github.com/smarter)),
+Ondrey Lhotak ([@olhotak](https://github.com/olhotak)),
+Samuel Gruetter ([@samuelgruetter](https://github.com/samuelgruetter)),
+Vera Salvis ([@vsalvis](https://github.com/vsalvis)),
+and Jason Zaugg ([@retronym](https://github.com/retronym)).
 
+To get started: <https://github.com/lampepfl/dotty>.

docs/blog/2016-01-02-new-year-resolutions.md

@@ -0,0 +1,64 @@
+---
+title: New Year Resolutions
+author: Martin Odersky
+authorImg: /images/martin.jpg
+---
+
+For most of us, the change of the year is an occasion for thinking
+about what we missed doing last year and where we want to improve. I decided
+there are a couple of things where I would like to do better in 2016
+than in 2015. The first is that I would like to do more blogging and
+writing in general. I have been pretty silent for most of the last
+year. This was mostly caused by the fact that I had been heads down to
+work on DOT, Scala's foundations, and _dotty_, the new Scala compiler
+platform we are working on. It's been a lot of work, but we are finally
+getting good results. DOT now has a mechanized proof of type soundness
+and the dotty compiler [can now compile
+itself](http://www.scala-lang.org/blog/2015/10/23/dotty-compiler-bootstraps.html)
+as well as large parts of Scala's standard library.
+
+The dotty compiler has a completely new and quite unusual
+architecture, which makes it resemble a functional database or a
+functional reactive program. My [talk at the JVM language
+summit](https://www.youtube.com/watch?v=WxyyJyB_Ssc) gives an
+overview. In the coming months I want to write together with my
+collaborators a series of blog posts
+ that explain details of the code base. The
+aim of these posts will be to present the new architectural patterns
+to a larger audience and also to help existing and potential
+contributors get familiar with the code base.
+
+My second resolution is to take a larger effort to promote simplicity
+in Scala. I believe the recent [blog post by Jim
+Plush](http://jimplush.com/talk/2015/12/19/moving-a-team-from-scala-to-golang/) should be a wakeup call for our
+community. Scala is a very powerful and un-opinionated language.  This
+means we have a large spectrum of choice how to write a Scala
+application or library. It's very important for all of us to use this
+power wisely, and to promote simplicity of usage wherever possible.
+Unfortunately, most of us fall all too easily into the complexity
+trap, as Alex Payne's tweet sums it up very nicely.
+
+<blockquote class="twitter-tweet" lang="en"><p lang="en" dir="ltr">“Complexity is like a bug light for smart people. We can&#39;t resist it, even though we know it&#39;s bad for us.” <a href="https://t.co/V9Izi573CF">https://t.co/V9Izi573CF</a></p>&mdash; Alex Payne (@al3x) <a href="https://twitter.com/al3x/status/683036775942496256">January 1, 2016</a></blockquote>
+<script async src="//platform.twitter.com/widgets.js" charset="utf-8"></script>
+
+I have been as guilty of complication as everybody else. Is
+`CanBuildFrom` the most appropriate solution to deal with the
+constraints of embedding special types such as arrays and strings in a
+collection library? It achieves its purpose of providing a uniform
+user-level API on disparate datatypes. But I now think with more
+effort we might be able come up with a solution that works as well and
+is simpler. Another example, where I have doubts if not regrets are
+the `/:` and `:\` operators in scala.collections.  They are cute
+synonyms for folds, and I am still fond of the analogy with falling
+dominoes they evoke. But in retrospect I think maybe they did give a
+bad example for others to go overboard with symbolic operators.
+
+So my main agenda for the coming year is to work on making Scala
+simpler: The language, its foundations, its libraries. I hope you
+will join me in that venture.
+
+With that thought, I wish you a happy new year 2016.
+
+
+
+

docs/blog/2016-02-03-essence-of-scala.md

@@ -0,0 +1,144 @@
+---
+title: The Essence of Scala
+author: Martin Odersky
+authorImg: /images/martin.jpg
+---
+
+What do you get if you boil Scala on a slow flame and wait until all
+incidental features evaporate and only the most concentrated essence
+remains? After doing this for 8 years we believe we have the answer:
+it's DOT, the calculus of dependent object types, that underlies Scala.
+
+A [paper on DOT](http://infoscience.epfl.ch/record/215280) will be
+presented in April at [Wadlerfest](http://events.inf.ed.ac.uk/wf2016),
+an event celebrating Phil Wadler's 60th birthday. There's also a prior
+technical report ([From F to DOT](http://arxiv.org/abs/1510.05216))
+by Tiark Rompf and Nada Amin describing a slightly different version
+of the calculus. Each paper describes a proof of type soundness that
+has been machine-checked for correctness.
+
+## The DOT calculus
+
+A calculus is a kind of mini-language that is small enough to be
+studied formally. Translated to Scala notation, the language covered
+by DOT is described by the following abstract grammar:
+
+    Value       v  =  (x: T) => t            Function
+                      new { x: T => ds }     Object
+
+    Definition  d  =  def a = t              Method definition
+                      type A = T             Type
+
+    Term        t  =  v                      Value
+                      x                      Variable
+                      t1(t2)                 Application
+                      t.a                    Selection
+                      { val x = t1; t2 }     Local definition
+
+    Type        T  =  Any                    Top type
+                      Nothing                Bottom type
+                      x.A                    Selection
+                      (x: T1) => T2          Function
+                      { def a: T }           Method declaration
+                      { type T >: T1 <: T2 } Type declaration
+                      T1 & T2                Intersection
+                      { x => T }             Recursion
+
+The grammar uses several kinds of names:
+
+    x      for (immutable) variables
+    a      for (parameterless) methods
+    A      for types
+
+The full calculus adds to this syntax formal _typing rules_ that
+assign types `T` to terms `t` and formal _evaluation rules_ that
+describe how a program is evaluated. The following _type soundness_
+property was shown with a mechanized, (i.e. machine-checked) proof:
+
+> If a term `t` has type `T`, and the evaluation of `t` terminates, then
+  the result of the evaluation will be a value `v` of type `T`.
+
+## Difficulties
+
+Formulating the precise soundness theorem and proving it was unexpectedly hard,
+because it uncovered some technical challenges that had not been
+studied in depth before. In DOT - as well as in many programming languages -
+you can have conflicting definitions. For instance you might have an abstract
+type declaration in a base class with two conflicting aliases in subclasses:
+
+     trait Base { type A }
+     trait Sub1 extends Base { type A = String }
+     trait Sub2 extends Base { type A = Int }
+     trait Bad extends Sub1 with Sub2
+
+Now, if you combine `Sub1` and `Sub2` in trait `Bad` you get a conflict,
+since the type `A` is supposed to be equal to both `String` and `Int`. If you do
+not detect the conflict and assume the equalities at face value you
+get `String = A = Int`, hence by transitivity `String = Int`! Once you
+are that far, you can of course engineer all sorts of situations where
+a program will typecheck but cause a wrong execution at runtime. In
+other words, type soundness is violated.
+
+Now, the problem is that one cannot always detect these
+inconsistencies, at least not by a local analysis that does not need
+to look at the whole program. What's worse, once you have an
+inconsistent set of definitions you can use these definitions to
+"prove" their own consistency - much like a mathematical theory that
+assumes `true = false` can "prove" every proposition including its own
+correctness.
+
+The crucial reason why type soundness still holds is this: If one
+compares `T` with an alias, one does so always relative to some _path_
+`x` that refers to the object containing `T`.  So it's really `x.T =
+Int`. Now, we can show that during evaluation every such path refers
+to some object that was created with a `new`, and that, furthermore,
+every such object has consistent type definitions. The tricky bit is
+to carefully distinguish between the full typing rules, which allow
+inconsistencies, and the typing rules arising from runtime values,
+which do not.
+
+## Why is This Important?
+
+There are at least four reasons why insights obtained in the DOT
+project are important.
+
+ 1. They give us a well-founded explanation of _nominal typing_.
+    Nominal typing means that a type is distinguished from others
+    simply by having a different name.
+    For instance, given two trait definitions
+
+          trait A extends AnyRef { def f: Int }
+          trait B extends AnyRef { def f: Int }
+
+    we consider `A` and `B` to be different types, even though both
+    traits have the same parents and both define the same members.
+    The opposite of
+    nominal typing is structural typing, which treats types
+    that have the same structure as being the same. Most programming
+    languages are at least in part nominal whereas most formal type systems,
+    including DOT, are structural. But the abstract types in DOT
+    provide a way to express nominal types such as classes and traits.
+    The Wadlerfest paper contains examples that show how
+    one can express classes for standard types such as `Boolean` and `List` in DOT.
+
+ 2. They give us a stable basis on which we can study richer languages
+    that resemble Scala more closely. For instance, we can encode
+    type parameters as type members of objects in DOT. This encoding
+    can give us a better understanding of the interactions of
+    subtyping and generics. It can explain why variance rules
+    are the way they are and what the precise typing rules for
+    wildcard parameters `[_ <: T]`, `[_ >: T]` should be.
+
+ 3. DOT also provides a blueprint for Scala compilation. The new Scala
+    compiler _dotty_ has internal data structures that closely resemble DOT.
+    In particular, type parameters are immediately mapped to type members,
+    in the way we propose to encode them also in the calculus.
+
+ 4. Finally, the proof principles explored in the DOT work give us guidelines
+    to assess and treat other possible soundness issues. We now know much
+    better what conditions must be fulfilled to ensure type soundness.
+    This lets us put other constructs of the Scala language to the test,
+    either to increase our confidence that they are indeed sound, or
+    to show that they are unsound. In my next blog I will
+    present some of the issues we have discovered through that exercise.
+