Merge branch 'dev'

doc/koka.css

@@ -275,7 +275,7 @@ a.pp:hover .pc, .tooltip {
   left:2ex;
   padding: 0.2ex 0.75ex 0.2ex 0.5ex;
   border:1px solid black;
-  background: #FFFFE8;   
+  background: #fffdf0;   
   white-space: pre;
 }
 

doc/spec/manual.kk.md → doc/spec/book.kk.md

@@ -1,17 +1,18 @@
-Title         : The Koka Manual
-Title Note    : [(&date;)]{font-size:75%}
+Title         : The &koka; Programming Language
+Title Note    : [(Daan Leijen, &date;)]{font-size:75%}
 Heading Base  : 1
 Heading Depth : 3
 Toc Depth     : 3
 Css           : styles/koka.css
-Css           : styles/manual.css
+Css           : styles/book.css
 Css           : https://maxcdn.bootstrapcdn.com/font-awesome/4.4.0/css/font-awesome.min.css
-Script        : scripts/manual.js
+Script        : scripts/book.js
 Colorizer     : unchecked.json
 Colorizer     : koka.json
 Bibliography  : koka.bib
 Description   : Koka Language Specification
 Mapsto        : [$\rightsquigarrow$]{.mapsto}
+Koka          : Koka
 
 [INCLUDE=book]
 [INCLUDE=styles/webanchors]
@@ -51,7 +52,6 @@ toc.toc-contents {
   .button;
 }
 
-
 @if preview {
   .code1 {
     border-bottom: 1px solid green;
@@ -78,10 +78,41 @@ li {
   margin-bottom: 1ex;
 }
 
+.note {
+  font-style: italic;
+}
+
+.advanced {
+  .boxed;
+  before: "[advanced]{.boxed-label}";
+}
+
+.translate {
+  .boxed;
+  replace: "[translation]{.boxed-label}&nl;~begin translate-row&nl;&source;&nl;~end translate-row&nl;";
+}
+
+.boxed {
+  border: 1px solid #AAA;
+  padding: 0em 1em;  
+}
+
+.boxed-label {
+  display: block;
+  float: left;
+  margin: -1.5em 0em -1em -1em;
+  font-size: 70%;
+  color: #999;
+}
+
 [koka-logo]: images/koka-logo.png { max-height: 120px; padding:1rem 1rem 1rem 1.5rem; }
 
+~ Begin MainHeader
+
 [TITLE]
 
+~ End MainHeader
+
 ~ Begin FlexBody
 
 ~ Begin SidePanel
@@ -98,7 +129,7 @@ li {
 
 [INCLUDE=getstarted.kk.md]
 
-[INCLUDE=overview.kk.md]
+[INCLUDE=why.kk.md]
 
 [INCLUDE=tour.kk.md]
 

doc/spec/getstarted.kk.md

@@ -1,15 +1,17 @@
+
 [<img align="right" src="https://badges.gitter.im/koka-lang/koka.svg"/>](https://gitter.im/koka-lang/koka?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge&utm_content=badge)
 
+
 # Getting started
 
-Welcome to Koka -- a functional-style language with effect types and handlers.
+Welcome to &koka; -- a functional-style language with effect types and handlers.
 
-[Why Koka?][#why]{.learn}
-[Install Koka][#install]{.learn}
-[Browse the Github repo][kokarepo]{.learn}
-[Browse the Library documentation][libraries]{.learn}
+[Why &koka;?][#why]{.learn}
+[Install &koka;][#install]{.learn}
+[The Github repo][kokarepo]{.learn}
+[Browse the Libraries][libraries]{.learn}
 
-Note: Koka v2 is a research language that is currently under heavy development. 
+Note: &koka; v2 is a research language that is currently under heavy development. 
 Nevertheless, the language is stable and the compiler
 implements the full specification. The main things lacking at the moment are 
 libraries and IDE integration. 
@@ -33,12 +35,12 @@ libraries and IDE integration.
 
 ## Installing the compiler { #install }
 
-For Linux and macOS on x86 64-bit, you can install Koka using:
+For Linux and macOS on x86 64-bit, you can install &koka; using:
 
     \(> **curl -sSL https://github.com/koka-lang/koka/releases/latest/download/install.sh &bar; sh**\)
 
 This also installs syntax highlighting for the VS Code and Atom editors.
-After installation, verify if Koka installed correctly:
+After installation, verify if &koka; installed correctly:
 
     > koka
      _          _           ____
@@ -60,7 +62,7 @@ It is also straightforward to build the compiler [from source][build].
 
 ## Running the compiler
 
-You can compile a Koka source using `-c` (note that all [`samples`][samples] are pre-installed):
+You can compile a &koka; source using `-c` (note that all [`samples`][samples] are pre-installed):
 
     > koka -c samples/basic/caesar.kk
     compile: samples/basic/caesar.kk
@@ -98,7 +100,7 @@ We can compare this against an in-place updating C++ implementation using ``stl:
 ([``rbtree.cpp``](https://github.com/koka-lang/koka/tree/master/samples/basic/rbtree.cpp)) (which also uses a
 [red-black tree](https://code.woboq.org/gcc/libstdc++-v3/src/c++98/tree.cc.html) internally):
 
-    > clang++ --std=c++17 -o cpp-rbtree -O3 samples/basic/rbtree.cpp
+    > clang++ --std=c++17 -o cpp-rbtree -O3 /usr/local/share/koka/v2.0.12/samples/basic/rbtree.cpp
     > time ./cpp-rbtree
     420000
     real    0m0.864s
@@ -170,7 +172,7 @@ And quit the interpreter:
 
 The [``samples/syntax``](https://github.com/koka-lang/koka/tree/master/samples/syntax)
 and [``samples/basic``](https://github.com/koka-lang/koka/tree/master/samples/basic) 
-directories contain various basic Koka examples to start with. If you type:
+directories contain various basic &koka; examples to start with. If you type:
 
     > :l samples/
 
@@ -201,15 +203,15 @@ you can type ``:e`` in the interactive prompt to edit your program further. For
 
 What next?
 
-[Why Koka?][#why]{.learn}
-[Basic Koka syntax][#sec-basics]{.learn}
+[Why &koka;?][#why]{.learn}
+[Basic &koka; syntax][#sec-basics]{.learn}
 [Browse the Library documentation][libraries]{.learn}
 
 
 <!--
 ## Algebraic effect handlers
 
-A novel feature of Koka is a compiled and typed implementation of algebraic
+A novel feature of &koka; is a compiled and typed implementation of algebraic
 effect handlers (described in detail in [[3]](#references)).
 In the interactive environment, you can load various demo files with algebraic
 effects which are located in the [``samples/handlers``](https://github.com/koka-lang/koka/tree/master/samples/handlers) directory.

doc/spec/koka.bib

@@ -168,3 +168,80 @@ @book{Okasaki:purefun
   year  = 1999,
   month = Jun
 }
+
+@inproceedings{Pretnar:handlers,
+  author    = {Plotkin, Gordon D. and Pretnar, Matija},
+  title     = {Handlers of Algebraic Effects},
+  booktitle = {18th European Symposium on Programming Languages and Systems},
+  series    = {ESOP'09},
+  location  = {York, UK},
+  month     = Mar,
+  pages     = {80--94},
+  year      = 2009,
+  doi       = {10.1007/978-3-642-00590-9_7}
+}
+
+@inproceedings{Leijen:algeff,
+  author  = "Daan Leijen",
+  title   = {Type Directed Compilation of Row-typed Algebraic Effects},
+  booktitle = {Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'17)},
+  month   = Jan,
+  year    = 2017,
+  isbn    = {978-1-4503-4660-3},
+  location= {Paris, France},
+  pages   = {486--499},
+  numpages= {14},
+  doi     = {10.1145/3009837.3009872}
+}
+
+@inproceedings{Gunter:mprompt,
+  author = {Gunter, Carl A. and R\'{e}my, Didier and Riecke, Jon G.},
+  title = {A Generalization of Exceptions and Control in ML-like Languages},
+  year = {1995},
+  isbn = {0897917197},
+  publisher = {ACM},
+  doi = {10.1145/224164.224173},
+  booktitle = {Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture},
+  pages = {12–23},
+  numpages = {12},
+  location = {La Jolla, California, USA},
+  series = {FPCA ’95}
+}
+
+@INPROCEEDINGS{Leijen:scopedlabels,
+  author    = {Daan Leijen},
+  title     = {Extensible records with scoped labels},
+  booktitle = {Proceedings of the 2005 Symposium on Trends in Functional Programming},
+  year      = {2005},
+  pages     = {297--312}
+}
+
+@ARTICLE{Biernacki:care,
+ author = {Biernacki, Dariusz and Pir\'{o}g, Maciej and Polesiuk, Piotr and Sieczkowski, Filip},
+ title = {Handle with Care: Relational Interpretation of Algebraic Effects and Handlers},
+ journal = {Proc. ACM Program. Lang.},
+ issue_date = {January 2018},
+ volume = {2},
+ number = {POPL'17 issue},
+ month = dec,
+ year = {2017},
+ issn = {2475-1421},
+ pages = {8:1--8:30},
+ articleno = {8},
+ numpages = {30},
+ doi = {10.1145/3158096},
+ keywords = {algebraic effect, logical relation, row polymorphism}
+}
+
+@inproceedings{Lindley:liberate,
+  author  = "Hillerström, Daniel and Lindley, Sam",
+  title   = "Liberating Effects with Rows and Handlers",
+  booktitle = {Proceedings of the 1st International Workshop on Type-Driven Development},
+  series = {{TyDe} 2016},
+  year = {2016},
+  location = {Nara, Japan},
+  pages = {15--27},
+  numpages = {13},
+  doi = {10.1145/2976022.2976033},
+}
+

doc/spec/spec.kk.md

@@ -1,7 +1,7 @@
 
-# Koka language specification
+# &koka; language specification
 
-This is the draft language specification of the Koka language, version v&kokaversion;\
+This is the draft language specification of the &koka; language, version v&kokaversion;\
 Currently only the lexical and context-free grammar are specified.
 The [standard libraries][stdlib] are documented separately.
 
@@ -269,7 +269,7 @@ of [JavaScript][ljavascript] and [Haskell][lhaskell] (I am sad to admit)
 the precise behavior is bizarrely complex where semicolon insertion
 depends on the interaction between the lexer and parser.
 
-In Koka, the grammar is carefully constructed to not need any statement
+In &koka;, the grammar is carefully constructed to not need any statement
 separator at all and semicolons are never required by the grammar.
 They are still allowed in the grammar but strictly to help new programmers
 that are used to putting semicolons at the end of statements.
@@ -278,17 +278,17 @@ The construction of a grammar that does not need statement separators is
 also good from a human perspective. The reason semicolons are required is
 to resolve ambiguities in the syntax. When such ambiguities do not occur
 in the first place, that also removes a cognitive burden from the
-programmer. In particular, Koka statements often start with a keyword,
+programmer. In particular, &koka; statements often start with a keyword,
 like `val` or `match`, signifying intention to both programmer and parser.
 
 In other cases, we restrict the expression grammar. For example, one
 reason why C requires semicolons is due to prefix- and postfix operators.
 If we write ``p ++ q`` the C parser needs a semicolon in order to know if
-we meant ``p++; q`` or ``p; ++q``. Such ambiguity is resolved in Koka by
+we meant ``p++; q`` or ``p; ++q``. Such ambiguity is resolved in &koka; by
 not having postfix operators and restricting prefix operators to ``!``
 and ``~``.
 
-One other reason that Koka can do without a statement separator is the
+One other reason that &koka; can do without a statement separator is the
 effect inference system: without such effect inference subtle bugs may
 occur if we leave out semicolons. For example, consider the following
 function:
@@ -304,9 +304,9 @@ fun square-wrong( x : int ) {
   x x
 }
 ```
-The Koka grammar sees this as 2 separate statements now, &ie; as ``x; x``
+The &koka; grammar sees this as 2 separate statements now, &ie; as ``x; x``
 returning ``x`` instead. In a language without effect inference it is hard
-to detect such errors, but the Koka type system rejects this program:
+to detect such errors, but the &koka; type system rejects this program:
 
     > fun square-wrong(x:int) { x x }
                                 ^
@@ -336,7 +336,7 @@ Just like programming languages like
 which automatically adds semicolons at appropriate places. This enables the
 programmer to leave out most semicolons:
 
-Koka inserts semicolons automatically for any statements
+&koka; inserts semicolons automatically for any statements
 and declarations that are _aligned between curly braces_ (`{` and `}`).
 {padding-left:1em}
 
@@ -387,7 +387,7 @@ more. Moreover, it means that the visual indentation of a program corresponds
 directly to how the compiler interprets the statements. Many tricky layout
 examples in other programming languages are often based on a mismatch between
 the visual representation and how a compiler interprets the tokens -- with
-Koka's layout rule such issues are largely avoided.
+&koka;'s layout rule such issues are largely avoided.
 
 To still allow for "block-style" layout, the
 layout rule does not insert a  semicolon for an aligned statement if it