Some documentation on changes since Idris 1

docs/index.rst

@@ -24,6 +24,7 @@ and yet to be updated, so use with caution!
 
    tutorial/index
    updates/updates
+   typedd/typedd
    proofs/index
    faq/faq
    reference/index

docs/typedd/typedd.rst

@@ -0,0 +1,318 @@
+.. _typedd-index:
+
+Type Driven Development with Idris: Updates Required
+====================================================
+
+The code in the book "Type Driven Development with Idris" by Edwin Brady,
+published by Manning, will mostly work in Idris 2, with some small changes
+as detailed in this document. The updated code is also [going to be] part
+of the test suite (see `tests/typedd-book <https://github.com/edwinb/Idris2/tree/master/tests/typedd-book>`_
+in the Idris 2 source).
+
+Chapter 1
+---------
+
+No changes necessary
+
+Chapter 2
+---------
+
+The Prelude is smaller than Idris 1, and many functions have been moved to
+the base libraries instead. So: 
+
+In ``Average.idr``, add:
+
+.. code-block:: idris
+
+    import Data.Strings -- for `words`
+    import Data.List -- for `length` on lists
+
+In ``AveMain.idr`` and ``Reverse.idr`` add:
+
+.. code-block:: idris
+
+    import System.REPL -- for 'repl'
+
+Chapter 3
+---------
+
+Unbound implicits have multiplicity 0, so we can't match on them at run-time.
+Therefore, in ``Matrix.idr``, we need to change the type of ``createEmpties``
+and ``transposeMat`` so that the length of the inner vector is available to
+match on:
+
+.. code-block:: idris
+
+    createEmpties : {n : _} -> Vect n (Vect 0 elem)
+    transposeMat : {n : _} -> Vect m (Vect n elem) -> Vect n (Vect m elem)
+
+Chapter 4
+---------
+
+For the reasons described above:
+
++ In ``DataStore.idr``, add ``import System.REPL`` and ``import Data.Strings``
++ In ``SumInputs.idr``, add ``import System.REPL``
++ In ``TryIndex.idr``, add an implicit argument:
+
+.. code-block:: idris
+
+    tryIndex : {n : _} -> Integer -> Vect n a -> Maybe a
+    
+Chapter 5
+---------
+
+There is no longer a ``Cast`` instance from ``String`` to ``Nat``, because its
+behaviour of returing Z if the ``String`` wasn't numeric was thought to be
+confusing. Instead, there is ``stringToNatOrZ`` in ``Data.Strings`` which at least
+has a clearer name. So:
+
+In ``Loops.idr`` and ``ReadNum.idr`` add ``import Data.Strings`` and change ``cast`` to
+``stringToNatOrZ``
+
+Chapter 6
+---------
+
+In ``DataStore.idr`` and ``DataStoreHoles.idr``, add ``import Data.Strings`` and
+``import System.REPL``. Also in ``DataStore.idr``, the ``schema`` argument to
+``display`` is required for matching, so change the type to:
+
+    display : {schema : _} -> SchemaType schema -> String
+
+In ``TypeFuns.idr`` add ``import Data.Strings``
+
+Chapter 7
+---------
+
+``Abs`` is now a separate interface from ``Neg``. So, change the type of ``eval``
+to include ``Abs`` specifically:
+
+    eval : (Abs num, Neg num, Integral num) => Expr num -> num
+
+Also, take ``abs`` out of the ``Neg`` implementation for ``Expr`` and add an
+implementation of ``Abs`` as follows:
+
+.. code-block:: idris
+
+    Abs ty => Abs (Expr ty) where
+        abs = Abs
+
+Chapter 8
+---------
+
+In ``AppendVec.idr``, add ``import Data.Nat`` for the ``Nat`` proofs
+
+``cong`` now takes an explicit argument for the function to apply. So, in
+``CheckEqMaybe.idr`` change the last case to:
+
+.. code-block:: idris
+
+    checkEqNat (S k) (S j) = case checkEqNat k j of
+                                  Nothing => Nothing
+                                  Just prf => Just (cong S prf)
+
+A similar change is necessary in ``CheckEqDec.idr``.
+
+In ``ExactLength.idr``, the ``m`` argument to ``exactLength`` is needed at run time,
+so change its type to:
+
+.. code-block:: idris
+
+    exactLength : {m : _} ->
+                  (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
+
+A similar change is necessary in ``ExactLengthDec.idr``. Also, ``DecEq`` is no
+longer part of the prelude, so add ``import Decidable.Equality``.
+
+In ``ReverseVec.idr``, add ``import Data.Nat`` for the ``Nat`` proofs.
+
+Chapter 9
+---------
+
++ In ``ElemType.idr``, add ``import Decidable.Equality``
+
+In ``Hangman.idr``:
+
++ Add ``import Decidable.Equality`` and ``import Data.Strings``
++ ``removeElem`` pattern matches on ``n``, so it needs to be written in its
+  type:
+
+.. code-block:: idris
+
+    removeElem : {n : _} ->
+                 (value : a) -> (xs : Vect (S n) a) ->
+                 {auto prf : Elem value xs} ->
+                 Vect n a
+
++ ``letters`` is used by ``processGuess``, because it's passed to ``removeElem``:
+
+.. code-block:: idris
+
+    processGuess : {letters : _} ->
+                   (letter : Char) -> WordState (S guesses) (S letters) ->
+                   Either (WordState guesses (S letters))
+                          (WordState (S guesses) letters)
+
++ ``guesses`` and ``letters`` are implicit arguments to ``game``, but are used by the
+  definition, so add them to its type:
+
+    game : {guesses : _} -> {letters : _} ->
+           WordState (S guesses) (S letters) -> IO Finished
+
+In ``RemoveElem.idr``
+
++ ``removeElem`` needs to be updated as above.
+
+Chapter 10
+----------
+
+Lots of changes necessary here, at least when constructing views, due to Idris
+2 having a better (that is, more precise and correct!) implementation of
+unification, and the rules for recursive ``with`` application being tightened up.
+
+In ``MergeSort.idr``, add ``import Data.List``
+
+In ``MergeSortView.idr``, add ``import Data.List``, and make the arguments to the
+views explicit:
+
+.. code-block:: idris
+
+    mergeSort : Ord a => List a -> List a
+    mergeSort input with (splitRec input)
+      mergeSort [] | SplitRecNil = []
+      mergeSort [x] | SplitRecOne x = [x]
+      mergeSort (lefts ++ rights) | (SplitRecPair lefts rights lrec rrec)
+           = merge (mergeSort lefts | lrec)
+                   (mergeSort rights | rrec)
+
+In ``SnocList.idr``, in ``my_reverse``, the link between ``Snoc rec`` and ``xs ++ [x]``
+needs to be made explicit. Idris 1 would happily decide that ``xs`` and ``x`` were
+the relevant implicit arguments to ``Snoc`` but this was little more than a guess
+based on what would make it type check, whereas Idris 2 is more precise in
+what it allows to unify. So, ``x`` and ``xs`` need to be explicit arguments to
+``Snoc``:
+
+.. code-block:: idris
+
+    data SnocList : List a -> Type where
+         Empty : SnocList []
+         Snoc : (x, xs : _) -> (rec : SnocList xs) -> SnocList (xs ++ [x])
+  
+Correspondingly, they need to be explicit when matching. For example:
+
+.. code-block:: idris
+
+      my_reverse : List a -> List a
+      my_reverse input with (snocList input)
+        my_reverse [] | Empty = []
+        my_reverse (xs ++ [x]) | (Snoc x xs rec) = x :: my_reverse xs | rec
+
+Similar changes are necessary in ``snocListHelp`` and ``my_reverse_help``. See
+tests/typedd-book/chapter10/SnocList.idr for the full details.
+
+Also, in ``snocListHelp``, ``input`` is used at run time so needs to be bound
+in the type:
+
+    snocListHelp : {input : _} ->
+                   (snoc : SnocList input) -> (rest : List a) -> SnocList (input +
+
+It's no longer necessary to give ``{input}`` explicitly in the patterns for
+``snocListHelp``, although it's harmless to do so.
+
+In ``IsSuffix.idr``, the matching has to be written slightly differently. The
+recursive with application in Idris 1 probably shouldn't have allowed this!
+
+.. code-block:: idris
+
+    isSuffix : Eq a => List a -> List a -> Bool
+    isSuffix input1 input2 with (snocList input1, snocList input2)
+      isSuffix [] input2 | (Empty, s) = True
+      isSuffix input1 [] | (s, Empty) = False
+      isSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc xsrec, Snoc ysrec)
+         = if x == y 
+              then isSuffix xs ys | (xsrec, ysrec)
+              else False
+
+This doesn't yet get past the totality checker, however, because it doesn't
+know about looking inside pairs.
+
+In ``DataStore.idr``: Well this is embarrassing - I've no idea how Idris 1 lets
+this through! I think perhaps it's too "helpful" when solving unification
+problems. To fix it, add an extra parameter ``scheme`` to ``StoreView``, and change
+the type of ``SNil`` to be explicit that the ``empty`` is the function defined in
+``DataStore``. Also add ``entry`` and ``store`` as explicit arguments to ``SAdd``:
+
+.. code-block:: idris
+
+    data StoreView : (schema : _) -> DataStore schema -> Type where
+         SNil : StoreView schema DataStore.empty
+         SAdd : (entry, store : _) -> (rec : StoreView schema store) ->
+                StoreView schema (addToStore entry store)
+
+Since ``size`` is as explicit argument in the ``DataStore`` record, it also needs
+to be relevant in the type of ``storeViewHelp``:
+
+.. code-block:: idris
+
+    storeViewHelp : {size : _} ->
+                    (items : Vect size (SchemaType schema)) ->
+                    StoreView schema (MkData size items)
+
+In ``TestStore.idr``:
+
++ In ``listItems``, ``empty`` needs to be ``DataStore.empty`` to be explicit that you
+  mean the function
++ In ``filterKeys``, there is an error in the ``SNil`` case, which wasn't caught
+  because of the type of ``SNil`` above. It should be:
+
+      filterKeys test DataStore.empty | SNil = []
+
+Chapter 11
+----------
+
+Remove ``%default total`` throughout - it's not yet implemented.
+
+In ``Streams.idr`` add ``import Data.Stream`` for ``iterate``.
+
+In ``Arith.idr`` and ``ArithTotal.idr``, the ``Divides`` view now has explicit
+arguments for the dividend and remainder, so they need to be explicit in
+``bound``:
+
+.. code-block:: idris
+
+    bound : Int -> Int
+    bound x with (divides x 12)
+      bound ((12 * div) + rem) | (DivBy div rem prf) = rem + 1
+
+In ``ArithCmd.idr``, update ``DivBy`` as above. Also add ``import Data.Strings`` for
+``Strings.toLower``.
+
+In ``ArithCmd.idr``, update ``DivBy`` and ``import Data.Strings`` as above. Also,
+since export rules are per-namespace now, rather than per-file, you need to
+export ``(>>=)`` from the namespaces ``CommandDo`` and ``ConsoleDo``.
+
+Chapter 12
+----------
+
+Remove ``%default total`` throughout, at least until it's implemented.
+
+For reasons described above: In ``ArithState.idr``, add ``import Data.Strings``.
+Also the ``(>>=)`` operators need to be set as ``export`` since they are in their
+own namespaces, and in ``getRandom``, ``DivBy`` needs to take additional
+arguments ``div`` and ``rem``.
+
+Chapter 13
+----------
+
+TODO
+
+Chapter 14
+----------
+
+TODO
+
+Chapter 15
+----------
+
+TODO
+

docs/updates/updates.rst

@@ -5,7 +5,11 @@ Changes since Idris 1
 #####################
 
 Idris 2 is mostly backwards compatible with Idris 1, with some minor
-exceptions. This document describes the changes.
+exceptions. This document describes the changes, approximately in order of
+likelihood of encountering them in practice. New features are described at
+the end, in Section :ref:`sect-new-features`.
+
+[NOT YET COMPLETE]
 
 .. note::
    The documentation for Idris has been published under the Creative
@@ -15,5 +19,105 @@ exceptions. This document describes the changes.
 
    More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
 
-TODO
+New Core Language: Quantities in Types
+======================================
 
+Erasure
+-------
+
+Linearity
+---------
+
+Prelude and ``base`` libraries
+==============================
+
+Prelide is much smaller, things moved to ``base``.
+
+Smaller Changes
+===============
+
+Ambiguous Name Resolution
+-------------------------
+
+Modules, namespaces and export
+------------------------------
+
+Change in visibility rules, and module names must match filenames except
+``Main``.
+
+``%language`` pragmas
+---------------------
+
+Not moved to Idris 2, any extensions are not implemented.
+
+``let`` bindings
+----------------
+
+Now don't compute, and equivalent to ``(\x => e) val``, but see 
+:ref:`sect-local-defs` below.
+
+``auto``-implicits and Interfaces
+---------------------------------
+
+Now the same thing
+
+Totality and Coverage
+---------------------
+
+``%default covering`` is now the default status [Actually still TODO, but
+planned soon!]
+
+Build artefacts
+---------------
+
+Not really a language change, but a change in the way Idris saves checked
+files. All checked modules are now saved in a directory ``build/ttc``, in the
+root of the source tree, with the directory structure following the directory
+structure of the source.  Executables are placed in ``build/exec``.
+
+.. _sect-new-features:
+
+New features
+============
+
+In addition to updating the core to QTT, described above.
+
+.. _sect-local-defs:
+
+Local function definitions
+--------------------------
+
+However, Idris no longer attempts to infer types for functions defined in
+``where`` blocks, because this was fragile. This may be reinstated, if we can
+come up with a good, predictable approach.
+
+Scope of implicit arguments
+---------------------------
+
+Better inference
+----------------
+
+Holes global to a source file, case works better.
+
+Dependent case
+--------------
+
+Record updates
+--------------
+
+Dependent record updates now work, as long as all relevant fields are updated
+at once.
+
+Generate definition
+-------------------
+
+A new feature of the IDE protocol, generating complete definitions from a
+type signature.
+
+Chez Scheme target
+------------------
+
+Also, optionally, Racket, which itself can compile via Chez scheme. Early
+experience shows that both are much faster than the Idris 1 C code generator,
+in both compile time and execution time (but we haven't done any formal
+study on this yet, so it's just anecdotal evidence).