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))))
106Idris has two heaps where objects can be allocated:
108+--------------------------------------+---------------------------------------+
110+======================================+=======================================+
111| Cheney-collected | Mark-and-sweep-collected |
112+--------------------------------------+---------------------------------------+
113| Garbage collections touches only | Garbage collection has to traverse |
114| live objects. | all registered items. |
115+--------------------------------------+---------------------------------------+
116| Ideal for FP-style rapid allocation | Ideal for C-style allocation of a few |
117| of lots of small short-lived pieces | big buffers. |
118| of memory, such as data constructors.| |
119+--------------------------------------+---------------------------------------+
120| Finalizers are impossible to support | Items have finalizers that are called |
121| reasonably. | on deallocation. |
122+--------------------------------------+---------------------------------------+
123| Data is copied all the time (when | Copying does not happen. |
124| collecting garbage, modifying data, | |
125| registering managed pointers, etc.) | |
126+--------------------------------------+---------------------------------------+
127| Contains objects of various types. | Contains C heap items: ``(void *)`` |
128| | pointers with finalizers. A finalizer |
129| | is a routine that deallocates the |
130| | resources associated with the item. |
131+--------------------------------------+---------------------------------------+
132| Fixed set of object types. | The data pointer may point |
133| | to anything, as long as the finalizer |
134| | cleans up correctly. |
135+--------------------------------------+---------------------------------------+
136| Not suitable for C resources and | Suitable for C resources and arbitrary|
137| arbitrary pointers. | pointers. |
138+--------------------------------------+---------------------------------------+
139| Values form a compact memory block. | Items are kept in a linked list. |
140+--------------------------------------+---------------------------------------+
141| Any Idris value, most notably | Items represented by the |
142| ``ManagedPtr``. | Idris type ``CData``. |
143+--------------------------------------+---------------------------------------+
144| Data of ``ManagedPtr`` allocated | Data allocated in C, pointer copied |
145| in C, buffer then copied into the FP | into the C heap. |
147+--------------------------------------+---------------------------------------+
148| Allocation and reallocation not | Allocated and reallocate freely in C, |
149| possible from C code (without having | registering the allocated items |
150| a reference to the VM). Everything | in the FFI. |
151| is copied instead. | |
152+--------------------------------------+---------------------------------------+
154The FP heap is the primary heap. It may contain values of type ``CData``,
155which are references to items in the C heap. A C heap item contains
156a ``(void *)`` pointer and the corresponding finalizer. Once a C heap item
157is no longer referenced from the FP heap, it is marked as unused and
158the next GC sweep will call its finalizer and deallocate it.
160There is no Idris interface for ``CData`` other than its type and FFI.
165* Although not enforced in code, ``CData`` is meant to be opaque
166 and non-RTS code (such as libraries or C bindings) should
167 access only its ``(void *)`` field called ``data``.
169* Feel free to mutate both the pointer ``data`` (eg. after calling ``realloc``)
170 and the memory it points to. However, keep in mind
171 that this must not break Idris's referential transparency.
173* **WARNING!** If you call ``cdata_allocate`` or ``cdata_manage``,
174 the resulting ``CData`` object *must* be returned from your
175 FFI function so that it is inserted in the C heap by the RTS.
176 Otherwise the memory will be leaked.
180 some_allocating_fun : Int -> IO CData
181 some_allocating_fun i = foreign FFI_C "some_allocating_fun" (Int -> IO CData) i
183 other_fun : CData -> Int -> IO Int
184 other_fun cd i = foreign FFI_C "other_fun" (CData -> Int -> IO Int) cd i
188 #include "idris_rts.h"
190 static void finalizer(void * data)
192 MyStruct * ptr = (MyStruct *) data;
193 free_something(ptr->something);
197 CData some_allocating_fun(int arg)
199 void * data = (void *) malloc(...);
201 return cdata_manage(data, finalizer);
204 int other_fun(CData cd, int arg)
206 int result = foo(cd->data);
213This syntax is defined in the module ``Syntax.PreorderReasoning`` in the
214``base`` package. It provides a syntax for composing proofs of
215reflexive-transitive relations, using overloadable functions called
216``step`` and ``qed``. This module also defines ``step`` and ``qed``
217functions allowing the syntax to be used for demonstrating equality.
222 import Syntax.PreorderReasoning
223 multThree : (a, b, c : Nat) -> a * b * c = c * a * b
225 (a * b * c) ={ sym (multAssociative a b c) }=
226 (a * (b * c)) ={ cong (multCommutative b c) }=
227 (a * (c * b)) ={ multAssociative a c b }=
228 (a * c * b) ={ cong {f = (* b)} (multCommutative a c) }=
231Note that the parentheses are required -- only a simple expression can
232be on the left of ``={ }=`` or ``QED``. Also, when using preorder
233reasoning syntax to prove things about equality, remember that you can
234only relate the entire expression, not subexpressions. This might
235occasionally require the use of ``cong``.
237Finally, although equality is the most obvious application of preorder
238reasoning, it can be used for any reflexive-transitive relation.
239Something like ``step1 ={ just1 }= step2 ={ just2 }= end QED`` is
240translated to ``(step step1 just1 (step step2 just2 (qed end)))``,
241selecting the appropriate definitions of ``step`` and ``qed`` through
242the normal disambiguation process. The standard library, for example,
243also contains an implementation of preorder reasoning on isomorphisms.
246Pattern matching on Implicit Arguments
247======================================
249Pattern matching is only allowed on implicit arguments when they are
250referred by name, e.g.
254 foo : {n : Nat} -> Nat
262 foo : {n : Nat} -> Nat
265The latter could be shortened to the following:
269 foo : {n : Nat} -> Nat
272That is, ``{x}`` behaves like ``{x=x}``.
275Existence of an instance
276========================
278In order to show that an instance of some typeclass is defined for some
279type, one could use the ``%instance`` keyword:
289``ty <== name`` applies the function ``name`` in such a way that it has
290the type ``ty``, by matching ``ty`` against the function's type. This
291can be used in proofs, for example:
295 plus_comm : (n : Nat) -> (m : Nat) -> (n + m = m + n)
297 (Z + m = m + Z) <== plus_comm =
298 rewrite ((m + Z = m) <== plusZeroRightNeutral) ==>
302 (S k + m = m + S k) <== plus_comm =
303 rewrite ((k + m = m + k) <== plus_comm) in
304 rewrite ((S (m + k) = m + S k) <== plusSuccRightSucc) in
310Including ``%reflection`` functions and ``quoteGoal x by fn in t``,
311which applies ``fn`` to the expected type of the current expression, and
312puts the result in ``x`` which is in scope when elaborating ``t``.
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