Idris2/docs/source/updates/updates.rst

.. _updates-index:

#####################
Changes since Idris 1
#####################

Idris 2 is mostly backwards compatible with Idris 1, with some minor
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`.

The Section :ref:`typedd-index` describes how these changes affect the code
in 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 language
developed by Bob Atkey and Conor McBride. In practice, this means that every
variable 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 to
attempting to use an argument which is erased at run time.

Erasure
-------

In Idris, names which begin with a lower case letter are automatically bound
as implicit arguments in types, for example in the following skeleton
definition, ``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 language
is deciding which arguments are used at run time and which can safely be
erased. More importantly, it's one of the difficulties when programming: how
can a programmer *know* when an argument will be erased?

In Idris 2, a variable's quantity tells us whether it will be available at
run 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 there
will be ``0`` occurrences at run-time. That is, it is *guaranteed* that they
will 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 you
can 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 takes
advantage of the type level information, but the trade off is that ``n`` has to
be available at run time, so at run time we always need the length of the
vector to be available if we ever call ``vlen``. Idris 1 can infer whether the
length 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 available
in the definition without explicitly rebinding them.)

This also means that when you call ``vlen``, you need the length available. For
example, 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`` with
unrestricted 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 the
biggest 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 performance
might 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 an
argument with multiplicity ``0``, unless its value is inferrable from
elsewhere. 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 appear
to match on the erased argument ``x``, its value is uniquely inferrable from
the 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 as
you're using unbound implicits in your Idris 1 programs, they will work without
much modification in Idris 2. The Idris 2 type checker will point out where you
require an unbound implicit argument at run time - sometimes this is both
surprising 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`` is
that 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 used
exactly 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 rarely
necessary. The philosophy in Idris 2 is different. The (rather vaguely
specified) rule of thumb is that it should contain the basic functions
required by almost any non-trivial program.

This is a vague specification since different programmers will consider
different 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``
- ``Range``, 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 be
in 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 this
involved some complicated interaction with interface resolution. This could
sometimes be the cause of long type checking times. Idris 2 simplifies this, at
the cost of sometimes requiring more programmer annotations on ambiguous
names.

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.
It will postpone resolution if a name can't be resolved immediately, but unlike
Idris 1, it won't attempt significant backtracking. If you have deeply nested
ambiguous names (beyond a small threshold, default 3) Idris 2 will report an
error.  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 to
disambiguate explicitly.

Indeed in general, if you get an ambiguous name error, the best approach is to
give 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 possibility
is 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 concrete
name is valid (``LinearIO.(>>=)`` here, so if type checking an expression known
to 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 from
other *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

    namespace 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 always
visible from the parent namespace.

Also, module names must now match the filename in which they're defined, with
the exception of the module ``Main``, which can be defined in a file with
any name.

``%language`` pragmas
---------------------

There are several ``%language`` pragmas in Idris 1, which define various
experimental extensions. None of these are available in Idris 2, although
extensions may be defined in the future.

Also removed was the ``%access`` pragma for default visibility, use visibility
modifiers on each declaration instead.

``let`` bindings
----------------

``let`` bindings, i.e. expressions of the form ``let x = val in e`` have
slightly different behaviour. Previously, you could rely on the computational
behaviour of ``x`` in the scope of ``e``, so type checking could take into
account that ``x`` reduces to ``val``. Unfortunately, this leads to complications
with ``case`` and ``with`` clauses: if we want to preserve the computational
behaviour, 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 have
enough time to resolve the problem for ``case`` and ``with``) the above
expression ``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 possible
using local function definitions instead - see Section :ref:`sect-local-defs`
below.

Also, an alternative syntax ``let x := val in e`` is available.
See Section :ref:`sect-let-bindings` for more info.

``auto``-implicits and Interfaces
---------------------------------

Interfaces and ``auto``-implicit arguments are similar, in that they invoke an
expression 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 found
by ``auto``-implicit search.

When defining a ``data`` type, there are ways to control how ``auto``-implicit
search 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 of
type ``Elem t ts`` will start as soon as the type checker has resolved the
value ``t``, even if ``ts`` is still unknown.

By default, ``auto``-implicit search uses the constructors of a data type
as search hints. The ``noHints`` option on a data type turns this behaviour
off.

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 we
can 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 be
used with care. Too many hints can lead to a large search space!

Record fields
-------------

Record fields can now be accessed via a ``.``. For example, if you have:

.. code-block:: idris

    record Person where
        constructor MkPerson
        firstName, middleName, lastName : String
        age : Int

and you have a record ``fred : Person``, then you can use ``fred.firstName``
to access the ``firstName`` field.

Totality and Coverage
---------------------

``%default covering`` is now the default status, so all functions must cover
all their inputs unless stated otherwise with a ``partial`` annotation, or
switching to ``%default partial`` (which is not recommended - use a ``partial``
annotation instead to have the smallest possible place where functions are
partial).

.. _build-artefacts:

Build artefacts
---------------

This is not really a language change, but a change in the way Idris saves
checked files, and still useful to know. 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``.

Packages
--------

Dependencies on other packages are now indicated with the ``depends`` field,
the ``pkgs`` field is no longer recognized. Also, fields with URLS or other
string data (other than module or package names), must be enclosed in double
quotes.
For example:

::

        package lightyear

        sourceloc  = "git://git@github.com:ziman/lightyear.git"
        bugtracker = "http://www.github.com/ziman/lightyear/issues"

        depends = effects

        modules = Lightyear
                , Lightyear.Position
                , Lightyear.Core
                , Lightyear.Combinators
                , Lightyear.StringFile
                , Lightyear.Strings
                , Lightyear.Char
                , Lightyear.Testing


.. _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 local
variable ``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`` blocks
as 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 can
come 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 the
body 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* of
the local definition. For example, the following definition, where we attempt
to 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
        showBody : Vect n a -> String
        showBody [] = ""
        showBody [x] = show x
        showBody (x :: xs) = show x ++ ", " ++ showBody xs

This fails because ``n`` is in scope already, from the type of ``showVect``,
in the type declaration for ``showBody``, and so the first clause ``showBody
[]`` will fail to type check because ``[]`` has length ``Z``, not ``n``. We can
fix this by locally binding ``n``:

.. code-block:: idris

    showVect : Show a => Vect n a -> String
    showVect xs = "[" ++ showBody xs ++ "]"
      where
        showBody : forall n . Vect n a -> String
        ...

Or, alternatively, using a new name:

.. code-block:: idris

    showVect : Show a => Vect n a -> String
    showVect xs = "[" ++ showBody xs ++ "]"
      where
        showBody : Vect n' a -> String
        ...

Idris 1 took a different approach here: names which were parameters to data
types were in scope, other names were not. The Idris 2 approach is, we hope,
more consistent and easier to understand.

.. _sect-app-syntax-additions:

Function application syntax additions
-------------------------------------

From now on you can utilise the new syntax of function applications:

.. code-block:: idris

    f {x1 [= e1], x2 [= e2], ...}

There are three additions here:

1. More than one argument can be written in braces, separated with commas:

.. code-block:: idris

    record Dog where
      constructor MkDog
      name : String
      age : Nat

    -- Notice that `name` and `age` are explicit arguments.
    -- See paragraph (2)
    haveADog : Dog
    haveADog = MkDog {name = "Max", age = 3}

    pairOfStringAndNat : (String, Nat)
    pairOfStringAndNat = MkPair {x = "year", y = 2020}

    myPlus : (n : Nat) -> (k : Nat) -> Nat
    myPlus {n = Z   , k} = k
    myPlus {n = S n', k} = S (myPlus n' k)

    twoPlusTwoIsFour : myPlus {n = 2, k = 2} === 4
    twoPlusTwoIsFour = Refl

2. Arguments in braces can now correspond to explicit, implicit and auto implicit
   dependent function types (``Pi`` types), provided the domain type is named:

.. code-block:: idris

    myPointlessFunction : (exp : String) -> {imp : String} -> {auto aut : String} -> String
    myPointlessFunction exp = exp ++ imp ++ aut

    callIt : String
    callIt = myPointlessFunction {imp = "a ", exp = "Just ", aut = "test"}

Order of the arguments doesn't matter as long as they are in braces and the names are distinct.
It is better to stick named arguments in braces at the end of your argument list, because
regular unnamed explicit arguments are processed first and take priority:

.. code-block:: idris

    myPointlessFunction' : (a : String) -> String -> (c : String) -> String
    myPointlessFunction' a b c = a ++ b ++ c

    badCall : String
    badCall = myPointlessFunction' {a = "a", c = "c"} "b"

This snippet won't type check, because "b" in ``badCall`` is passed first,
although logically we want it to be second.
Idris will tell you that it couldn't find a spot for ``a = "a"`` (because "b" took its place),
so the application is ill-formed.

Thus if you want to use the new syntax, it is worth naming your ``Pi`` types.

3. Multiple explicit arguments can be "skipped" more easily with the following syntax:

.. code-block:: idris

    f {x1 [= e1], x2 [= e2], ..., xn [= en], _}

or

.. code-block:: idris

    f {}

in case none of the named arguments are wanted.

Examples:

.. code-block:: idris

    import Data.Nat

    record Four a b c d where
      constructor MkFour
      x : a
      y : b
      z : c
      w : d

    firstTwo : Four a b c d -> (a, b)
    firstTwo $ MkFour {x, y, _} = (x, y)
    -- firstTwo $ MkFour {x, y, z = _, w = _} = (x, y)

    dontCare : (x : Nat) -> Nat -> Nat -> Nat -> (y : Nat) -> x + y = y + x
    dontCare {} = plusCommutative {}
    --dontCare _ _ _ _ _ = plusCommutative _ _

Last rule worth noting is the case of named applications with repeated argument names, e.g:

.. code-block:: idris

    data WeirdPair : Type -> Type -> Type where
      MkWeirdPair : (x : a) -> (x : b) -> WeirdPair a b

    weirdSnd : WeirdPair a b -> b
    --weirdSnd $ MkWeirdPair {x, x} = x
    --                        ^
    -- Error: "Non linear pattern variable"
    -- But that one is okay:
    weirdSnd $ MkWeirdPair {x = _, x} = x

In this example the name ``x`` is given repeatedly to the ``Pi`` types of the data constructor ``MkWeirdPair``.
In order to deconstruct the ``WeirdPair a b`` in ``weirdSnd``, while writing the left-hand side of the pattern-matching clause
in a named manner (via the new syntax), we have to rename the first occurrence of ``x`` to any fresh name or the ``_`` as we did.
Then the definition type checks normally.

In general, duplicate names are bound sequentially on the left-hand side and must be renamed for the pattern expression to be valid.

The situation is similar on the right-hand side of pattern-matching clauses:

.. code-block:: idris

   0 TypeOf : a -> Type
   TypeOf _ = a

   weirdId : {0 a : Type} -> (1 a : a) -> TypeOf a
   weirdId a = a

   zero : Nat
   -- zero = weirdId { a = Z }
   --                      ^
   -- Error: "Mismatch between: Nat and Type"
   -- But this works:
   zero = weirdId { a = Nat, a = Z }

Named arguments should be passed sequentially in the order they were defined in the ``Pi`` types,
regardless of their (imp)explicitness.

Better inference
----------------

In Idris 1, holes (that is, unification variables arising from implicit
arguments) were local to an expression, and if they were not resolved while
checking the expression, they would not be resolved at all. In Idris 2,
they are global, so inference works better. For example, we can now say:

.. code-block:: idris

    test : Vect ? Int
    test = [1,2,3,4]

    Main> :t test
    Main.test : Vect (S (S (S (S Z)))) Int

The ``?``, incidentally, differs from ``_`` in that ``_`` will be bound as
an implicit argument if unresolved after checking the type of ``test``, but
``?`` will be left as a hole to be resolved later. Otherwise, they can be
used interchangeably.

Dependent case
--------------

``case`` blocks were available in Idris 1, but with some restrictions. Having
better inference means that ``case`` blocks work more effectively in Idris 2,
and dependent case analysis is supported.

.. code-block:: idris

    append : Vect n a -> Vect m a -> Vect (n + m) a
    append xs ys
        = case xs of
               [] => ys
               (x :: xs) => x :: append xs ys

The implicit arguments and original values are still available in the body of
the ``case``. Somewhat contrived, but the following is valid:

.. code-block:: idris

    info : {n : _} -> Vect n a -> (Vect n a, Nat)
    info xs
        = case xs of
               [] => (xs, n)
               (y :: ys) => (xs, n)


Record updates
--------------

Dependent record updates work, provided that all relevant fields are updated
at the same time. Dependent record update is implemented via dependent ``case``
blocks rather than by generating a specific update function for each field as
in Idris 1, so you will no longer get mystifying errors when trying to update
dependent records!

For example, we can wrap a vector in a record, with an explicit length
field:

.. code-block:: idris

    record WrapVect a where
      constructor MkVect
      purpose : String
      length : Nat
      content : Vect length a

Then, we can safely update the ``content``, provided we update the ``length``
correspondingly:

.. code-block:: idris

    addEntry : String -> WrapVect String -> WrapVect String
    addEntry val = record { length $= S,
                            content $= (val :: ) }

Another novelty - new update syntax (previous one still functional):

.. code-block:: idris

    record Three a b c where
      constructor MkThree
      x : a
      y : b
      z : c

    -- Yet another contrived example
    mapSetMap : Three a b c -> (a -> a') -> b' -> (c -> c') -> Three a' b' c'
    mapSetMap three@(MkThree x y z) f y' g = {x $= f, y := y', z $= g} three

The ``record`` keyword has been discarded for brevity, symbol ``:=`` replaces ``=``
in order to not introduce any ambiguity.

Generate definition
-------------------

A new feature of the IDE protocol supports generating complete definitions from
a type signature. You can try this at the REPL, for example, given our
favourite introductory example...

.. code-block:: idris

    append : Vect n a -> Vect m a -> Vect (n + m) a

...assuming this is defined on line 3, you can use the ``:gd`` command as
follows:

.. code-block:: idris

    Main> :gd 3 append
    append [] ys = ys
    append (x :: xs) ys = x :: append xs ys

This works by a fairly simple brute force search, which tries searching for a
valid right hand side, and case splitting on the left if that fails, but is
remarkably effective in a lot of situations. Some other examples which work:

.. code-block:: idris

    my_cong : forall f . (x : a) -> (y : a) -> x = y -> f x = f y
    my_curry : ((a, b) -> c) -> a -> b -> c
    my_uncurry : (a -> b -> c) -> (a, b) -> c
    append : Vect n a -> Vect m a -> Vect (n + m) a
    lappend : (1 xs : List a) -> (1 ys : List a) -> List a
    zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c

This is available in the IDE protocol via the ``generate-def`` command.

Chez Scheme target
------------------

The default code generator is, for the moment, `Chez Scheme
<https://www.scheme.com/>`_. Racket and Gambit code generators are also
available.  Like Idris 1, Idris 2 `supports plug-in code generation
<https://idris2.readthedocs.io/en/latest/backends/custom.html>`_
to allow you to write a back end for the platform of your choice.
To change the code generator, you can use the ``:set cg`` command:

::

    Main> :set cg racket

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).