5Things we have yet to classify, or are two small to justify their own page.
11If you're having a hard time debugging why the unifier won't accept
12something (often while debugging the compiler itself), try applying the
13special operator ``%unifyLog`` to the expression in question. This will
14cause the type checker to spit out all sorts of informative messages.
17Namespaces and type-directed disambiguation
18===========================================
20Names can be defined in separate namespaces, and disambiguated by type.
21An expression ``with NAME EXPR`` will privilege the namespace ``NAME``
22in the expression ``EXPR``. For example:
26 Idris> with List [[1,2],[3,4],[5,6]]
27 [[1, 2], [3, 4], [5, 6]] : List (List Integer)
29 Idris> with Vect [[1,2],[3,4],[5,6]]
30 [[1, 2], [3, 4], [5, 6]] : Vect 3 (Vect 2 Integer)
32 Idris> [[1,2],[3,4],[5,6]]
33 Can't disambiguate name: Prelude.List.::, Prelude.Stream.::, Prelude.Vect.::
39The syntax ``(| option1, option2, option3, ... |)`` type checks each
40of the options in turn until one of them works. This is used, for
41example, when translating integer literals.
45 Idris> the Nat (| "foo", Z, (-3) |)
49This can also be used to give simple automated proofs, for example: trying
50some constructors of proofs.
54 syntax Trivial = (| Oh, Refl |)
57Totality checking assertions
58============================
60All definitions are checked for *coverage* (i.e. all well-typed
61applications are handled) and either for *termination* (i.e. all
62well-typed applications will eventually produce an answer) or, if
63returning codata, for productivity (in practice, all recursive calls are
66Obviously, termination checking is undecidable. In practice, the
67termination checker looks for *size change* - every cycle of recursive
68calls must have a decreasing argument, such as a recursive argument of a
69strictly positive data type.
71There are two built-in functions which can be used to give the totality
74- ``assert_total x`` asserts that the expression ``x`` is terminating
75 and covering, even if the totality checker cannot tell. This can be
76 used for example if ``x`` uses a function which does not cover all
77 inputs, but the caller knows that the specific input is covered.
78- ``assert_smaller p x`` asserts that the expression ``x`` is
79 structurally smaller than the pattern ``p``.
81For example, the following function is not checked as total:
85 qsort : Ord a => List a -> List a
87 qsort (x :: xs) = qsort (filter (<= x) xs) ++ (x :: qsort (filter (>= x) xs)))
89This is because the checker cannot tell that ``filter`` will always
90produce a value smaller than the pattern ``x :: xs`` for the recursive
91call to ``qsort``. We can assert that this will always be true as
97 qsort : Ord a => List a -> List a
99 qsort (x :: xs) = qsort (assert_smaller (x :: xs) (filter (<= x) xs)) ++
100 (x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs))))
106This syntax is defined in the module ``Syntax.PreorderReasoning`` in the
107``base`` package. It provides a syntax for composing proofs of
108reflexive-transitive relations, using overloadable functions called
109``step`` and ``qed``. This module also defines ``step`` and ``qed``
110functions allowing the syntax to be used for demonstrating equality.
115 import Syntax.PreorderReasoning
116 multThree : (a, b, c : Nat) -> a * b * c = c * a * b
118 (a * b * c) ={ sym (multAssociative a b c) }=
119 (a * (b * c)) ={ cong (multCommutative b c) }=
120 (a * (c * b)) ={ multAssociative a c b }=
121 (a * c * b) ={ cong {f = (* b)} (multCommutative a c) }=
124Note that the parentheses are required -- only a simple expression can
125be on the left of ``={ }=`` or ``QED``. Also, when using preorder
126reasoning syntax to prove things about equality, remember that you can
127only relate the entire expression, not subexpressions. This might
128occasionally require the use of ``cong``.
130Finally, although equality is the most obvious application of preorder
131reasoning, it can be used for any reflexive-transitive relation.
132Something like ``step1 ={ just1 }= step2 ={ just2 }= end QED`` is
133translated to ``(step step1 just1 (step step2 just2 (qed end)))``,
134selecting the appropriate definitions of ``step`` and ``qed`` through
135the normal disambiguation process. The standard library, for example,
136also contains an implementation of preorder reasoning on isomorphisms.
139Pattern matching on Implicit Arguments
140======================================
142Pattern matching is only allowed on implicit arguments when they are
143referred by name, e.g.
147 foo : {n : Nat} -> Nat
155 foo : {n : Nat} -> Nat
158The latter could be shortened to the following:
162 foo : {n : Nat} -> Nat
165That is, ``{x}`` behaves like ``{x=x}``.
168Existence of an implementation
169==============================
171In order to show that an implementation of some interface is defined for some
172type, one could use the ``%implementation`` keyword:
177 foo = %implementation
182``ty <== name`` applies the function ``name`` in such a way that it has
183the type ``ty``, by matching ``ty`` against the function's type. This
184can be used in proofs, for example:
188 plus_comm : (n : Nat) -> (m : Nat) -> (n + m = m + n)
190 (Z + m = m + Z) <== plus_comm =
191 rewrite ((m + Z = m) <== plusZeroRightNeutral) ==>
195 (S k + m = m + S k) <== plus_comm =
196 rewrite ((k + m = m + k) <== plus_comm) in
197 rewrite ((S (m + k) = m + S k) <== plusSuccRightSucc) in
203Including ``%reflection`` functions and ``quoteGoal x by fn in t``,
204which applies ``fn`` to the expected type of the current expression, and
205puts the result in ``x`` which is in scope when elaborating ``t``.
210Use of ``optparse-applicative`` allows Idris to support Bash
211completion. You can obtain the completion script for Idris using the
214 idris --bash-completion-script `which idris`
217To enable completion for the lifetime of your current session, run the
220 source <(idris --bash-completion-script `which idris`)
223To enable completion permanently you must either:
225* Modify your bash init script with the above command.
227* Add the completion script to the appropriate ``bash_completion.d/``
228 folder on your machine.
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list