.. _updates-index: #####################Changes since Idris 1##################### Idris 2 is mostly backwards compatible with Idris 1, with some minorexceptions. This document describes the changes, approximately in order oflikelihood of encountering them in practice. New features are described atthe end, in Section :ref:`sect-new-features`. The Section :ref:`typedd-index` describes how these changes affect the codein the book `Type-Driven Development with Idris <https://www.manning.com/books/type-driven-development-with-idris>`_by Edwin Brady, available from `Manning <https://www.manning.com>`_. .. note::   The documentation for Idris has been published under the Creative   Commons CC0 License. As such to the extent possible under law, *The   Idris Community* has waived all copyright and related or neighboring   rights to Documentation for Idris.    More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/ New Core Language: Quantities in Types====================================== Idris 2 is based on `Quantitative Type Theory (QTT)<https://bentnib.org/quantitative-type-theory.html>`_, a core languagedeveloped by Bob Atkey and Conor McBride. In practice, this means that everyvariable in Idris 2 has a *quantity* associated with it. A quantity is one of: * ``0``, meaning that the variable is *erased* at run time* ``1``, meaning that the variable is used *exactly once* at run time* *Unrestricted*, which is the same behaviour as Idris 1 For more details on this, see Section :ref:`sect-multiplicities`. In practice,this might cause some Idris 1 programs not to type check in Idris 2 due toattempting to use an argument which is erased at run time. Erasure------- In Idris, names which begin with a lower case later are automatically boundas implicit arguments in types, for example in the following skeletondefinition, ``n``, ``a`` and ``m`` are implicitly bound: .. code-block:: idris     append : Vect n a -> Vect m a -> Vect (n + m) a    append xs ys = ?append_rhs One of the difficulties in compiling a dependently typed programming languageis deciding which arguments are used at run time and which can safely beerased. More importantly, it's one of the difficulties when programming: howcan a programmer *know* when an argument will be erased? In Idris 2, a variable's quantity tells us whether it will be available atrun time or not. We can see the quantities of the variables in scope in``append_rhs`` by inspecting the hole at the REPL: ::     Main> :t append_rhs     0 m : Nat     0 a : Type     0 n : Nat       ys : Vect m a       xs : Vect n a    -------------------------------------    append_rhs : Vect (plus n m) a The ``0`` next to ``m``, ``a`` and ``n`` mean that they are in scope, but therewill be ``0`` occurrences at run-time. That is, it is *guaranteed* that theywill be erased at run-time. This does lead to some potential difficulties when converting Idris 1 programs,if you are using implicit arguments at run time.  For example, in Idris 1 youcan get the length of a vector as follows: .. code-block:: idris     vlen : Vect n a -> Nat    vlen {n} xs = n This might seem like a good idea, since it runs in constant time and takesadvantage of the type level information, but the trade off is that ``n`` has tobe available at run time, so at run time we always need the length of thevector to be available if we ever call ``vlen``. Idris 1 can infer whether thelength is needed, but there's no easy way for a programmer to be sure. In Idris 2, we need to state explicitly that ``n`` is needed at run time .. code-block:: idris     vlen : {n : Nat} -> Vect n a -> Nat    vlen xs = n (Incidentally, also note that in Idris 2, names bound in types are also availablein the definition without explicitly rebinding them.) This also means that when you call ``vlen``, you need the length available. Forexample, this will give an error .. code-block:: idris     sumLengths : Vect m a -> Vect n a —> Nat    sumLengths xs ys = vlen xs + vlen ys Idris 2 reports::   vlen.idr:7:20--7:28:While processing right hand side of Main.sumLengths at vlen.idr:7:1--10:1:  m is not accessible in this context This means that it needs to use ``m`` as an argument to pass to ``vlen xs``,where it needs to be available at run time, but ``m`` is not available in``sumLengths`` because it has multiplicity ``0``. We can see this more clearly by replacing the right hand side of``sumLengths`` with a hole... .. code-block:: idris     sumLengths : Vect m a -> Vect n a -> Nat    sumLengths xs ys = ?sumLengths_rhs ...then checking the hole's type at the REPL::   Main> :t sumLengths_rhs   0 n : Nat   0 a : Type   0 m : Nat     ys : Vect n a     xs : Vect m a  -------------------------------------  sumLengths_rhs : Nat Instead, we need to give bindings for ``m`` and ``n`` withunrestricted multiplicity .. code-block:: idris     sumLengths : {m, n : _} -> Vect m a -> Vect n a —> Nat    sumLengths xs ys = vlen xs + vlen xs Remember that giving no multiplicity on a binder, as with ``m`` and ``n`` here,means that the variable has unrestricted usage. If you're converting Idris 1 programs to work with Idris 2, this is probably thebiggest thing you need to think about. It is important to note,though, that if you have bound implicits, such as... .. code-block:: idris     excitingFn : {t : _} -> Coffee t -> Moonbase t ...then it's a good idea to make sure ``t`` really is needed, or performancemight suffer due to the run time building the instance of ``t`` unnecessarily! One final note on erasure: it is an error to try to pattern match on anargument with multiplicity ``0``, unless its value is inferrable fromelsewhere. So, the following definition is rejected .. code-block:: idris     badNot : (0 x : Bool) -> Bool    badNot False = True    badNot True = False This is rejected with the error::   badnot.idr:2:1--3:1:Attempt to match on erased argument False in  Main.badNot The following, however, is fine, because in ``sNot``, even though we appearto match on the erased argument ``x``, its value is uniquely inferrable fromthe type of the second argument .. code-block:: idris     data SBool : Bool -> Type where         SFalse : SBool False         STrue  : SBool True     sNot : (0 x : Bool) -> SBool x -> Bool    sNot False SFalse = True    sNot True  STrue  = False Experience with Idris 2 so far suggests that, most of the time, as long asyou're using unbound implicits in your Idris 1 programs, they will work withoutmuch modification in Idris 2. The Idris 2 type checker will point out where yourequire an unbound implicit argument at run time - sometimes this is bothsurprising and enlightening!  Linearity--------- Full details on linear arguments with multiplicity ``1`` are given in Section:ref:`sect-multiplicities`. In brief, the intuition behind multiplicity ``1`` isthat if we have a function with a type of the following form... .. code-block:: idris     f : (1 x : a) -> b ...then the guarantee given by the type system is that *if* ``f x`` *is usedexactly once, then* ``x`` *is used exactly once* in the process. Prelude and ``base`` libraries============================== The Prelude in Idris 1 contained a lot of definitions, many of them rarelynecessary. The philosophy in Idris 2 is different. The (rather vaguelyspecified) rule of thumb is that it should contain the basic functionsrequired by almost any non-trivial program. This is a vague specification since different programmers will considerdifferent things absolutely necessary, but the result is that it contains: - Anything the elaborator can desugar to (e.g. tuples, ``()``, ``=``)- Basic types ``Bool``, ``Nat``, ``List``, ``Stream``, ``Dec``, ``Maybe``,  ``Either``- The most important utility functions: ``id``, ``the``, composition, etc- Interfaces for arithmetic and implementations for the primitives and  basic types- Basic ``Char`` and ``String`` manipulation- ``Show``, ``Eq``, ``Ord``, and implementations for all types in the prelude- Interfaces and functions for basic proof (``cong``, ``Uninhabited``, etc)- ``Semigroup``, ``Monoid``- ``Functor``, ``Applicative``, ``Monad`` and related functions- ``Foldable``, ``Alternative`` and ``Traversable``- ``Enum``, for list range syntax- Console ``IO`` Anything which doesn't fit in here has been moved to the ``base`` libraries.Among other places, you can find some of the functions which used to bein the prelude in: - ``Data.List`` and ``Data.Nat``- ``Data.Maybe`` and ``Data.Either``- ``System.File`` and ``System.Directory``, (file management was previously  part of the prelude)- ``Decidable.Equality`` Smaller Changes=============== Ambiguous Name Resolution------------------------- Idris 1 worked very hard to resolve ambiguous names, by type, even if thisinvolved some complicated interaction with interface resolution. This couldsometimes be the cause of long type checking times. Idris 2 simplifies this, atthe cost of sometimes requiring more programmer annotations on ambiguousnames. As a general rule, Idris 2 will be able to disambiguate between names whichhave different concrete return types (such as data constructors), or which havedifferent concrete argument types (such as record projections). It may struggleto resolve ambiguities if one name requires an interface to be resolved.It will postpone resolution if a name can't be resolved immediately, but unlikeIdris 1, it won't attempt significant backtracking. If you have deeply nestedambiguous names (beyond a small threshold, default 3) Idris 2 will report anerror.  You can change this threshold with a directive, for example: .. code-block:: idris     %ambiguity_depth 10 However, in such circumstances it is almost certainly a better idea todisambiguate explicitly. Indeed in general, if you get an ambiguous name error, the best approach is togive the namespace explicitly. You can also rebind names locally: .. code-block:: idris     Main> let (::) = Prelude.(::) in [1,2,3]    [1, 2, 3] One difficulty which remains is resolving ambiguous names where one possibilityis an interface method, and another is a concrete top level function.For example, we may have: .. code-block:: idris     Prelude.(>>=) : Monad m => m a -> (a -> m b) -> m b    LinearIO.(>>=) : (1 act : IO a) -> (1 k : a -> IO b) -> IO b As a pragmatic choice, if type checking in a context where the more concretename is valid (``LinearIO.(>>=)`` here, so if type checking an expression knownto have type ``IO t`` for some ``t``), the more concrete name will be chosen. This is somehow unsatisfying, so we may revisit this in future! Modules, namespaces and export------------------------------ The visibility rules, as controlled by the ``private``, ``export`` and``public export`` modifiers, now refer to the visibility of names fromother *namespaces*, rather than other *files*. So if you have the following, all in the same file... .. code-block:: idris     namespace A      private      aHidden : Int -> Int      aHidden x = x * 2       export      aVisible : Int -> Int      aVisibile x = aHidden x     mamespace B      export      bVisible : Int -> Int      bVisible x = aVisible (x * 2) ...then ``bVisible`` can access ``aVisible``, but not ``aHidden``. Records are, as before, defined in their own namespace, but fields are alwaysvisible from the parent namespace. Also, module names must now match the filename in which they're defined, withthe exception of the module ``Main``, which can be defined in a file withany name. ``%language`` pragmas--------------------- There are several ``%language`` pragmas in Idris 1, which define variousexperimental extensions. None of these are available in Idris 2, althoughextensions may be defined in the future. ``let`` bindings---------------- ``let`` bindings, i.e. expressions of the form ``let x = val in e`` haveslightly different behaviour. Previously, you could rely on the computationalbehaviour of ``x`` in the scope of ``e``, so type checking could take intoaccount that ``x`` reduces to ``val``. Unfortunately, this leads to complicationswith ``case`` and ``with`` clauses: if we want to preserve the computationalbehaviour, we would need to make significant changes to the way ``case`` and``with`` are elaborated. So, for simplicity and consistency (and, realistically, because I don't haveenough time to resolve the problem for ``case`` and ``with``) the aboveexpression ``let x = val in e`` is equivalent to ``(\x => e) val``. So, ``let`` now effectively generalises a complex subexpression.If you do need the computational behaviour of a definition, it is now possibleusing local function definitions instead - see Section :ref:`sect-local-defs`below. ``auto``-implicits and Interfaces--------------------------------- Interfaces and ``auto``-implicit arguments are similar, in that they invoke anexpression search mechanism to find the value of an argument. In Idris 1,they were implemented separately, but in Idris 2, they use the same mechanism.Consider the following *total* definition of ``fromMaybe``: .. code-block:: idris     data IsJust : Maybe a -> Type where         ItIsJust : IsJust (Just val)     fromMaybe : (x : Maybe a) -> {auto p : IsJust x} -> a    fromMaybe (Just x) {p = ItIsJust} = x Since interface resolution and ``auto``-implicits are now the same thing,the type of ``fromMaybe`` can be written as: .. code-block:: idris     fromMaybe : (x : Maybe a) -> IsJust x => a So now, the constraint arrow ``=>`` means that the argument will be foundby ``auto``-implicit search. When defining a ``data`` type, there are ways to control how ``auto``-implicitsearch will proceed, by giving options to the data type. For example: .. code-block:: idris     data Elem : (x : a) -> (xs : List a) -> Type where         [search x]         Here : Elem x (x :: xs)         There : Elem x xs -> Elem x (y :: xs) The ``search x`` option means that ``auto``-implicit search for a value oftype ``Elem t ts`` will start as soon as the type checker has resolved thevalue ``t``, even if ``ts`` is still unknown. By default, ``auto``-implicit search uses the constructors of a data typeas search hints. The ``noHints`` option on a data type turns this behaviouroff. You can add your own search hints with the ``%hint`` option on a function.For example: .. code-block:: idris     data MyShow : Type -> Type where         [noHints]         MkMyShow : (myshow : a -> String) -> MyShow a     %hint    showBool : MyShow Bool    showBool = MkMyShow (\x => if x then "True" else "False")     myShow : MyShow a => a -> String    myShow @{MkMyShow myshow} = myshow In this case, searching for ``MyShow Bool`` will find ``showBool``, as wecan see if we try evaluating ``myShow True`` at the REPL: ::     Main> myShow True    "True" In fact, this is how interfaces are elaborated. However, ``%hint`` should beused with care. Too many hints can lead to a large search space! Totality and Coverage--------------------- ``%default covering`` is now the default status [Actually still TODO, butplanned soon!] Build artefacts--------------- This is not really a language change, but a change in the way Idris saveschecked files, and still useful to know. All checked modules are now saved in adirectory ``build/ttc``, in the root of the source tree, with the directorystructure following the directory structure of the source.  Executables areplaced in ``build/exec``. .. _sect-new-features: New features============ As well as the change to the core language to use quantitative type theory,described above, there are several other new features. .. _sect-local-defs: Local function definitions-------------------------- Functions can now be defined locally, using a ``let`` block. For example,``greet`` in the following example, which is defined in the scope of a localvariable ``x``: .. code-block:: idris     chat : IO ()    chat        = do putStr "Name: "             x <- getLine             let greet : String -> String                 greet msg = msg ++ " " ++ x             putStrLn (greet "Hello")             putStrLn (greet "Bye") These ``let`` blocks can be used anywhere (in the middle of ``do`` blocksas above, but also in any function, or in type declarations).``where`` blocks are now elaborated by translation into a local ``let``. However, Idris no longer attempts to infer types for functions defined in``where`` blocks, because this was fragile. This may be reinstated, if we cancome up with a good, predictable approach. Scope of implicit arguments--------------------------- Implicit arguments in a type are now in scope in the body of a definition.We've already seen this above, where ``n`` is in scope automatically in thebody of ``vlen``: .. code-block:: idris     vlen : {n : Nat} -> Vect n a -> Nat    vlen xs = n This is important to remember when using ``where`` blocks, or local definitions,since the names in scope will also be in scope when declaring the *type* ofthe local definition. For example, the following definition, where we attemptto define our own version of ``Show`` for ``Vect``, will fail to type check: .. code-block:: idris     showVect : Show a => Vect n a -> String    showVect xs = "[" ++ showBody xs ++ "]"      where

Lines 1–500 of 659. Load more