mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-10-26 22:22:31 +03:00
fixed whitespace for *.md and .rst files
This commit is contained in:
parent
8b96614454
commit
29a6aa45e0
@ -15,7 +15,7 @@ beyond work on the language core, are (in no particular order):
|
||||
- code colouring
|
||||
- it'd be nice if Ctrl-C didn't quit the whole system!
|
||||
* IDE mode improvements
|
||||
- Syntax highlighting support for output
|
||||
- Syntax highlighting support for output
|
||||
- Several functions from the version 1 IDE protocol are not yet implemented,
|
||||
and I haven't confirmed it works in everything.
|
||||
- (Not really part of Idris 2, but an editing mode for vim would be lovely!)
|
||||
|
@ -120,7 +120,7 @@ If you are a [nix](https://nixos.org/features.html) user you can install Idris 2
|
||||
by running the following command:
|
||||
|
||||
nix-env -i idris2
|
||||
|
||||
|
||||
### Install from nix flakes
|
||||
|
||||
If you are a [nix flakes](https://nixos.wiki/wiki/Flakes) user you can install Idris 2 together with all the requirements by running the following command:
|
||||
|
@ -85,5 +85,3 @@ Rather than using ``State`` and ``Exception`` directly, however,
|
||||
we typically use interfaces to constrain the operations which are allowed
|
||||
in a list of errors. Internally, ``State`` is implemented via an
|
||||
``IORef``, primarily for performance reasons.
|
||||
|
||||
|
||||
|
@ -53,4 +53,3 @@ interfaces.
|
||||
exceptionsstate
|
||||
interfaces
|
||||
linear
|
||||
|
||||
|
@ -144,5 +144,3 @@ with any errors thrown by ``readFile``:
|
||||
readMain fname = handle (readFile fname)
|
||||
(\str => putStrLn $ "Success:\n" ++ show str)
|
||||
(\err : IOError => putStrLn $ "Error: " ++ show err)
|
||||
|
||||
|
||||
|
@ -105,4 +105,3 @@ is ``NoThrow`` or ``MayThrow``. But, in practice, all applications
|
||||
given to ``run`` will not throw at the top level, because the only
|
||||
exception type available is the empty type ``Void``. Any exceptions
|
||||
will have been introduced and handled inside the ``App``.
|
||||
|
||||
|
@ -5,7 +5,7 @@ Building Idris 2 with new backends
|
||||
The way to extend Idris 2 with new backends is to use it as
|
||||
a library. The module ``Idris.Driver`` exports the function
|
||||
``mainWithCodegens``, that takes a list of ``(String, Codegen)``,
|
||||
starting idris with these codegens in addition to the built-in ones. The first
|
||||
starting idris with these codegens in addition to the built-in ones. The first
|
||||
codegen in the list will be set as the default codegen.
|
||||
|
||||
Getting started
|
||||
|
@ -6,7 +6,7 @@ There is an experimental code generator which compiles to an executable via C,
|
||||
using a reference counting garbage collector. This is intended as a lightweight
|
||||
(i.e. minimal dependencies) code generator that can be ported to multiple
|
||||
platforms, especially those with memory constraints.
|
||||
|
||||
|
||||
Performance is not as good as the Scheme based code generators, partly because
|
||||
the reference counting has not yet had any optimisation, and partly because of
|
||||
the limitations of C. However, the main goal is portability: the generated
|
||||
|
@ -44,7 +44,7 @@ Where to find things:
|
||||
* ``Core/`` -- anything related to the core TT, typechecking and unification
|
||||
* ``TTImp/`` -- anything related to the implicit TT and its elaboration
|
||||
|
||||
+ ``TTImp/Elab/`` -- Elaboration state and elaboration of terms
|
||||
+ ``TTImp/Elab/`` -- Elaboration state and elaboration of terms
|
||||
+ ``TTImp/Interactive/`` -- Interactive editing infrastructure
|
||||
|
||||
* ``Parser/`` -- various utilities for parsing and lexing TT and TTImp (and other things)
|
||||
|
@ -31,7 +31,7 @@ Or if the ``proposition`` is,
|
||||
+-------+
|
||||
|
||||
we can't prove it is true, but it is still a valid proposition and perhaps we
|
||||
can prove it is false so the ``judgment`` is,
|
||||
can prove it is false so the ``judgment`` is,
|
||||
|
||||
+-------------+
|
||||
| 1+1=3 false |
|
||||
|
@ -4,7 +4,7 @@
|
||||
Theorem Proving
|
||||
###############
|
||||
|
||||
A tutorial on theorem proving in Idris 2.
|
||||
A tutorial on theorem proving in Idris 2.
|
||||
|
||||
.. note::
|
||||
|
||||
|
@ -101,7 +101,7 @@ yields:
|
||||
plus_commutes (S k) m = ?plus_commutes_S
|
||||
|
||||
That is, the hole has been filled with a call to a top level
|
||||
function ``plus_commutes_Z``, applied to the variable in scope ``m``.
|
||||
function ``plus_commutes_Z``, applied to the variable in scope ``m``.
|
||||
|
||||
Unfortunately, we cannot prove this lemma directly, since ``plus`` is
|
||||
defined by matching on its *first* argument, and here ``plus m Z`` has a
|
||||
@ -113,14 +113,14 @@ First, create a template definition with ``\d``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes_Z : (m : Nat) -> m = plus m Z
|
||||
plus_commutes_Z : (m : Nat) -> m = plus m Z
|
||||
plus_commutes_Z m = ?plus_commutes_Z_rhs
|
||||
|
||||
Now, case split on ``m`` with ``\c``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes_Z : (m : Nat) -> m = plus m Z
|
||||
plus_commutes_Z : (m : Nat) -> m = plus m Z
|
||||
plus_commutes_Z Z = ?plus_commutes_Z_rhs_1
|
||||
plus_commutes_Z (S k) = ?plus_commutes_Z_rhs_2
|
||||
|
||||
|
@ -26,7 +26,7 @@ match all possible values of ``n``. In this case
|
||||
|
||||
plusReducesR : (n : Nat) -> plus n Z = n
|
||||
plusReducesR Z = Refl
|
||||
plusReducesR (S k)
|
||||
plusReducesR (S k)
|
||||
= let rec = plusReducesR k in
|
||||
rewrite sym rec in Refl
|
||||
|
||||
@ -118,7 +118,7 @@ and these are also included in the prelude:
|
||||
Heterogeneous Equality
|
||||
======================
|
||||
|
||||
Also included in the prelude:
|
||||
Also included in the prelude:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -130,6 +130,3 @@ Also included in the prelude:
|
||||
||| @ y the right side
|
||||
(~=~) : (x : a) -> (y : b) -> Type
|
||||
(~=~) x y = (x = y)
|
||||
|
||||
|
||||
|
||||
|
@ -25,11 +25,11 @@ dependent types in general, can be obtained from various sources:
|
||||
|
||||
* Examining the prelude and exploring the ``samples`` in the
|
||||
distribution. The Idris 2 source can be found online at:
|
||||
|
||||
|
||||
* https://github.com/edwinb/Idris2.
|
||||
|
||||
* Existing projects on the ``Idris Hackers`` web space:
|
||||
|
||||
|
||||
* https://idris-hackers.github.io.
|
||||
|
||||
* Various papers (e.g. [#BradyHammond2012]_, [#Brady]_, and [#BradyHammond2010]_). Although these mostly
|
||||
|
@ -261,4 +261,3 @@ by using ``idris2 -–client``.
|
||||
More sophisticated support can be added by using the IDE protocol (yet to
|
||||
be documented for Idris 2, but which mostly extends to protocol documented for
|
||||
`Idris 1 <https://docs.idris-lang.org/en/latest/reference/ide-protocol.html>`_.
|
||||
|
||||
|
@ -117,7 +117,7 @@ Meaning for Functions
|
||||
about doing this.
|
||||
|
||||
.. note::
|
||||
|
||||
|
||||
Type synonyms in Idris are created by writing a function. When
|
||||
setting the visibility for a module, it is usually a good idea to
|
||||
``public export`` all type synonyms if they are to be used outside
|
||||
@ -130,15 +130,15 @@ Therefore, it's generally a good idea to avoid using ``public export`` for
|
||||
functions unless you really mean to export the full definition.
|
||||
|
||||
.. note::
|
||||
*For beginners*:
|
||||
*For beginners*:
|
||||
If the function needs to be accessed only at runtime, use ``export``.
|
||||
However, if it's also meant to be used at *compile* time (e.g. to prove
|
||||
a theorem), use ``public export``.
|
||||
However, if it's also meant to be used at *compile* time (e.g. to prove
|
||||
a theorem), use ``public export``.
|
||||
For example, consider the function ``plus : Nat -> Nat -> Nat`` discussed
|
||||
previously, and the following theorem: ``thm : plus Z m = m``.
|
||||
In order to to prove it, the type checker needs to reduce ``plus Z m`` to ``m``
|
||||
previously, and the following theorem: ``thm : plus Z m = m``.
|
||||
In order to to prove it, the type checker needs to reduce ``plus Z m`` to ``m``
|
||||
(and hence obtain ``thm : m = m``).
|
||||
To achieve this, it will need access to the *definition* of ``plus``,
|
||||
To achieve this, it will need access to the *definition* of ``plus``,
|
||||
which includes the equation ``plus Z m = m``.
|
||||
Therefore, in this case, ``plus`` has to be marked as ``public export``.
|
||||
|
||||
|
@ -76,7 +76,7 @@ By "used" we mean either:
|
||||
|
||||
* if the variable is a data type or primitive value, it is pattern matched against, ex. by being the subject of a *case* statement, or a function argument that is pattern matched against, etc.,
|
||||
* if the variable is a function, that function is applied (i.e. ran with an argument)
|
||||
|
||||
|
||||
First, we'll see how this works on some small examples of functions and
|
||||
data types, then see how it can be used to encode `resource protocols`_.
|
||||
|
||||
@ -151,10 +151,10 @@ wraps an argument with unrestricted use
|
||||
|
||||
data Lin : Type -> Type where
|
||||
MkLin : (1 _ : a) -> Lin a
|
||||
|
||||
|
||||
data Unr : Type -> Type where
|
||||
MkUnr : a -> Unr a
|
||||
|
||||
|
||||
If ``MkLin x`` is used once, then ``x`` is used once. But if ``MkUnr x`` is
|
||||
used once, there is no guarantee on how often ``x`` is used. We can see this a
|
||||
bit more clearly by starting to write projection functions for ``Lin`` and
|
||||
@ -164,10 +164,10 @@ bit more clearly by starting to write projection functions for ``Lin`` and
|
||||
|
||||
getLin : (1 _ : Lin a) -> a
|
||||
getLin (MkLin x) = ?howmanyLin
|
||||
|
||||
|
||||
getUnr : (1 _ : Unr a) -> a
|
||||
getUnr (MkUnr x) = ?howmanyUnr
|
||||
|
||||
|
||||
Checking the types of the holes shows us that, for ``getLin``, we must use
|
||||
``x`` exactly once (Because the ``val`` argument is used once,
|
||||
by pattern matching on it as ``MkLin x``, and if ``MkLin x`` is used once,
|
||||
@ -197,7 +197,7 @@ If ``getLin`` has an unrestricted argument...
|
||||
getLin (MkLin x) = ?howmanyLin
|
||||
|
||||
...then ``x`` is unrestricted in ``howmanyLin``::
|
||||
|
||||
|
||||
Main> :t howmanyLin
|
||||
0 a : Type
|
||||
x : a
|
||||
@ -267,12 +267,12 @@ So an example correct door protocol usage would be
|
||||
.. code-block:: idris
|
||||
|
||||
doorProg : IO ()
|
||||
doorProg
|
||||
doorProg
|
||||
= newDoor $ \d =>
|
||||
let d' = openDoor d
|
||||
d'' = closeDoor d' in
|
||||
deleteDoor d''
|
||||
|
||||
|
||||
It's instructive to build this program interactively, with holes along
|
||||
the way, and see how the multiplicities of ``d``, ``d'`` etc change. For
|
||||
example
|
||||
@ -280,7 +280,7 @@ example
|
||||
.. code-block:: idris
|
||||
|
||||
doorProg : IO ()
|
||||
doorProg
|
||||
doorProg
|
||||
= newDoor $ \d =>
|
||||
let d' = openDoor d in
|
||||
?whatnow
|
||||
@ -302,7 +302,7 @@ It's also fine to shadow the name ``d`` throughout
|
||||
.. code-block:: idris
|
||||
|
||||
doorProg : IO ()
|
||||
doorProg
|
||||
doorProg
|
||||
= newDoor $ \d =>
|
||||
let d = openDoor d
|
||||
d = closeDoor d in
|
||||
@ -315,7 +315,7 @@ can try not to delete the door before finishing
|
||||
.. code-block:: idris
|
||||
|
||||
doorProg : IO ()
|
||||
doorProg
|
||||
doorProg
|
||||
= newDoor $ \d =>
|
||||
let d' = openDoor d
|
||||
d'' = closeDoor d' in
|
||||
@ -332,7 +332,7 @@ at the type level. If we have an external resource which is guaranteed to
|
||||
be used linearly, like ``Door``, we don't need to run operations on that
|
||||
resource in an ``IO`` monad, since we're already enforcing an ordering on
|
||||
operations and don't have access to any out of date resource states. This is
|
||||
similar to the way interactive programs work in
|
||||
similar to the way interactive programs work in
|
||||
`the Clean programming language <https://clean.cs.ru.nl/Clean>`_, and in
|
||||
fact is how ``IO`` is implemented internally in Idris 2, with a special
|
||||
``%World`` type for representing the state of the outside world that is
|
||||
@ -380,7 +380,7 @@ For example, in Idris 1 you could get the length of a vector as follows
|
||||
|
||||
vlen : Vect n a -> Nat
|
||||
vlen {n} xs = n
|
||||
|
||||
|
||||
This is fine, since it runs in constant time, 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
|
||||
@ -392,7 +392,7 @@ In Idris 2, we need to state explicitly that ``n`` is needed at run time
|
||||
|
||||
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.)
|
||||
|
||||
@ -403,12 +403,12 @@ example, this will give an error
|
||||
|
||||
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``.
|
||||
@ -420,7 +420,7 @@ We can see this more clearly by replacing the right hand side of
|
||||
|
||||
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
|
||||
@ -450,7 +450,7 @@ 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!
|
||||
|
||||
@ -466,7 +466,7 @@ elsewhere. So, the following definition is rejected
|
||||
|
||||
This is rejected with the error::
|
||||
|
||||
badnot.idr:2:1--3:1:Attempt to match on erased argument False in
|
||||
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
|
||||
@ -478,7 +478,7 @@ the type of the second argument
|
||||
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
|
||||
@ -495,13 +495,13 @@ Pattern Matching on Types
|
||||
-------------------------
|
||||
|
||||
One way to think about dependent types is to think of them as "first class"
|
||||
objects in the language, in that they can be assigned to variables,
|
||||
objects in the language, in that they can be assigned to variables,
|
||||
passed around and returned from functions, just like any other construct.
|
||||
But, if they're truly first class, we should be able to pattern match on
|
||||
them too! Idris 2 allows us to do this. For example
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
|
||||
showType : Type -> String
|
||||
showType Int = "Int"
|
||||
showType (List a) = "List of " ++ showType a
|
||||
|
@ -89,7 +89,7 @@ which you can run:
|
||||
$ idris2 hello.idr -o hello
|
||||
$ ./build/exec/hello
|
||||
Hello world
|
||||
|
||||
|
||||
(On Macos you may first need to install realpath: ```brew install coreutils```)
|
||||
|
||||
Please note that the dollar sign ``$`` indicates the shell prompt!
|
||||
|
Loading…
Reference in New Issue
Block a user