From fd2ebd52c30aebdfe007eb90638638cf773603e9 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Wed, 20 May 2020 11:31:24 +0100 Subject: [PATCH] Add licence and changelog and update REAMDE --- CHANGELOG.md | 55 +++++++++++++++++++++++++++++ LICENSE | 32 +++++++++++++++++ README.md | 98 +++++++++++++++++++++++++++++++++++++++++++++++----- 3 files changed, 177 insertions(+), 8 deletions(-) create mode 100644 CHANGELOG.md create mode 100644 LICENSE diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 index 000000000..abcfc3b81 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,55 @@ +Changes since Idris 2 v0.1.0 +---------------------------- + +The implementation is now self-hosted. To initialise the build, either use +the [bootstrapping version of Idris2](https://github.com/edwinb/Idris2-boot) +or build fromt the generated Scheme, using `make bootstrap`. + +Compiler updates: + +* Data types with a single constructor, with a single unerased arguments, + are translated to just that argument, to save repeated packing and unpacking. + (c.f. `newtype` in Haskell) + + A data type can opt out of this behaviour by specifying `noNewtype` in its + options list. `noNewtype` allows code generators to apply special handling + to the generated constructor/deconstructor, for a newtype-like data type, + that would otherwise be optimised away. +* 0-multiplicity constructor arguments are now properly erased, not just + given a placeholder null value. + +Language extensions: + +* %transform directive, for declaring transformation rules on runtime + expressions. Transformation rules are automatically added for top level + implementations of interfaces. +* A %spec flag on functions which allows arguments to be marked for partial + evaluation, following the rules from "Scrapping Your Inefficient Engine" + (ICFP 2010, Brady & Hammond) + +Library additions: + +* Additional file management operations in `base` +* New modules in `contrib` for time (`System.Clock`); JSON (`Language.JSON.*`); + random numbers (`System.Random`) + +Other improvements: + +* Various performance improvements in the typechecker: + + Noting which metavariables are blocking unification constraints, so that + they only get retried if those metavariables make progress. + + Evaluating `fromInteger` at compile time. + + In the run-time, reuse the old heap after garbage collection if it + hasn't been resized, to avoid unnecessary system calls. + +* Extend Idris2's literate mode to support reading Markdown and OrgMode files. + For more details see: https://idris2.readthedocs.io/en/latest/reference/literate.html + +* Fields of records can be accessed (and updated) using the dot syntax, + such as `r.field1.field2` or `record { field1.field2 = 42 }`. + For details, see https://idris2.readthedocs.io/en/latest/reference/records.html + +Changes since Idris 1 +--------------------- + +Everything :). For full details, see: +https://idris2.readthedocs.io/en/latest/updates/updates.html diff --git a/LICENSE b/LICENSE new file mode 100644 index 000000000..0685846f4 --- /dev/null +++ b/LICENSE @@ -0,0 +1,32 @@ +Copyright (c) 2020 Edwin Brady + School of Computer Science, University of St Andrews +All rights reserved. + +This code is derived from software written by Edwin Brady +(ecb10@st-andrews.ac.uk). + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: +1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. +2. Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. +3. None of the names of the copyright holders may be used to endorse + or promote products derived from this software without specific + prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY +EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE +LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR +CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF +SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR +BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, +WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE +OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN +IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +*** End of disclaimer. *** diff --git a/README.md b/README.md index 6f110a3d7..5cba49977 100644 --- a/README.md +++ b/README.md @@ -1,12 +1,94 @@ -Self-hosted Idris 2 -------------------- +Idris 2 +======= -It finally happened! +[![Build Status](https://travis-ci.org/edwinb/Idris2-SH.svg?branch=master)](https://travis-ci.org/edwinb/Idris2) -See `INSTALL.md` for installation instructions. +[Idris 2](https://idris-lang.org/) is a purely functional programming language +with first class types. -There are no guarantees: This repository might move or be renamed or deleted or -anything at no notice. It will eventually turn into the real Idris 2 -repository, one way or another. +For full installation instructions, see [INSTALL.md](INSTALL.md). Briefly, if +you have Chez Scheme installed, with the executable name `chez`, type: -Good luck :) +* `make bootstrap SCHEME=chez` +* `make install` + +You may need to change `chez` to be the local name of your Chez Scheme. This +is often one of `scheme`, `chezscheme` or `chezscheme9.5` (depending on the +version) + +Idris 2 is mostly backwards compatible with Idris 1, with some minor +exceptions. The most notable user visible differences, which might cause Idris +1 programs to fail to type check, are: + ++ Unbound implicit arguments are always erased, so it is a type error to + attempt to pattern match on one. ++ Simplified resolution of ambiguous names, which might mean you need to + explicitly disambiguate more often. As a general rule, Idris 2 will be able + to disambiguate between names which have different concrete return types + (such as data constructors), or which have different concrete argument + types (such as record projections). It may struggle to resolve ambiguities + if one name requires an interface to be resolved. ++ Minor differences in the meaning of export modifiers `private`, `export`, + and `public export`, which now refer to visibility of names from other + *namespaces* rather than visibility from other *files*. ++ Module names must match the filename in which they are defined (unless + the module's name is "Main"). ++ Anything which uses a `%language` pragma in Idris 1 is likely to be different. + Notably, elaborator reflection will exist, but most likely in a slightly + different form because the internal details of the elaborator are different. ++ The `Prelude` is much smaller (and easier to replace with an alternative). ++ `let x = val in e` no longer computes with `x` in `e`, instead being + essentially equivalent to `(\x => e) val`. This is to make the + behaviour of `let` consistent in the presence of `case` and `with` (where + it is hard to push the computation inside the `case`/`with` efficiently). + Instead, you can define functions locally with `let`, which do have + computational force, as follows: + + let x : ? + x = val in + e + +Watch this space for more details and the rationale for the changes, as I +get around to writing it... + +Summary of new features: + ++ A core language based on "Quantitative Type Theory" which allows explicit + annotation of erased types, and linear types. ++ `let` bindings are now more expressive, and can be used to define pattern + matching functions locally. ++ Names which are in scope in a type are also always in scope in the body of + the corresponding definition. ++ Better inference. Holes are global to a source file, rather than local to + a definition, meaning that some holes can be left in function types to be + inferred by the type checker. This also gives better inference for the types + of `case` expressions, and means fewer annotations are needed in interface + declarations. ++ Better type checker implementation which minimises the need for compile + time evaluation. ++ New Chez Scheme based back end which both compiles and runs faster than the + default Idris 1 back end. (Also, optionally, Racket and Gambit can be used + as targets). ++ Everything works faster :). + +A significant change in the implementation is that there is an intermediate +language `TTImp`, which is essentially a desugared Idris, and is cleanly +separated from the high level language which means it is potentially usable +as a core language for other high level syntaxes. + +Things still missing +==================== + ++ Disambiguation via 'with' ++ Cumulativity (so we currently have Type : Type! Bear that in mind when you + think you've proved something :)) ++ 'rewrite' doesn't yet work on dependent types ++ Parts of the ide-mode, particularly syntax highlighting ++ Documentation strings and HTML documentation generation ++ ':search' and ':apropos' at the REPL ++ Metaprogramming (reflection, partial evaluation) + +Talks +===== + +[![Idris 2 - Type-driven Development of Idris (Curry On - London 2019)](https://img.youtube.com/vi/DRq2NgeFcO0/0.jpg)](https://www.youtube.com/watch?v=DRq2NgeFcO0 "Idris 2 - Type-driven Development of Idris (Curry On - London 2019)")