diff --git a/docs/index.rst b/docs/index.rst index 25612e4..4d8a424 100644 --- a/docs/index.rst +++ b/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 diff --git a/docs/typedd/typedd.rst b/docs/typedd/typedd.rst new file mode 100644 index 0000000..0cd9613 --- /dev/null +++ b/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 `_ +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 + diff --git a/docs/updates/updates.rst b/docs/updates/updates.rst index a64c164..79743f9 100644 --- a/docs/updates/updates.rst +++ b/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).