git.iko.soy/Idris-dev
on bd8ea0a help sign in
Idris-dev/docs/reference/language-features.rst
54 lines 2.1 kB history raw
1**********************
2Core Language Features
3**********************
6- Full-spectrum dependent types
7- Strict evaluation (plus ``Lazy : Type -> Type`` type constructor for
8 explicit laziness)
9- Lambda, Pi (forall), Let bindings
10- Pattern matching definitions
11- Export modifiers ``public``, ``abstract``, ``private``
12- Function options ``partial``, ``total``
13- ``where`` clauses
14- "magic with"
15- Implicit arguments (in top level types)
16- "Bound" implicit arguments ``{n : Nat} -> {a : Type} -> Vect n a``
17- "Unbound" implicit arguments --- ``Vect n a`` is equivalent to the
18 above in a type, ``n`` and ``a`` are implicitly bound. This applies
19 to names beginning with a lower case letter in an argument position.
20- 'Tactic' implicit arguments, which are solved by running a tactic
21 script or giving a default argument, rather than by unification.
22- Unit type ``()``, empty type ``Void``
23- Tuples (desugaring to nested pairs)
24- Dependent pair syntax ``(x : T ** P x)`` (there exists an ``x`` of
25 type ``T`` such that ``P x``)
26- Inline ``case`` expressions
27- Heterogeneous equality
28- ``do`` notation
29- Idiom brackets
30- Interfaces (like type classes), supporting default methods and dependencies between
31 methods
32- ``rewrite`` prf ``in`` expr
33- Metavariables
34- Inline proof/tactic scripts
35- Implicit coercion
36- ``codata``
37- Also ``Inf : Type -> Type`` type constructor for mixed data/codata.
38 In fact ``codata`` is implemented by putting recursive arguments under
39 ``Inf``.
40- ``syntax`` rules for defining pattern and term syntactic sugar
41- these are used in the standard library to define
42 ``if ... then ... else`` expressions and an Agda-style preorder
43 reasoning syntax.
44- `Uniqueness
45 typing <https://github.com/idris-lang/Idris-dev/wiki/Uniqueness-Types>`__
46 using the ``UniqueType`` universe.
47- `Partial
48 evaluation <https://github.com/idris-lang/Idris-dev/wiki/Static-Arguments-and-Partial-Evaluation>`__
49 by ``%static`` argument annotations.
50- Error message reflection
51- Eliminators
52- Label types ``'name``
53- ``%logging n``
54- ``%unifyLog``