Core Language Features¶
Full-spectrum dependent types
Strict evaluation (plus
Lazy : Type -> Type
type constructor for explicit laziness)Lambda, Pi (forall), Let bindings
Pattern matching definitions
Export modifiers
public
,abstract
,private
Function options
partial
,total
where
clauses“magic with”
Implicit arguments (in top level types)
“Bound” implicit arguments
{n : Nat} -> {a : Type} -> Vect n a
“Unbound” implicit arguments —
Vect n a
is equivalent to the above in a type,n
anda
are implicitly bound. This applies to names beginning with a lower case letter in an argument position.‘Tactic’ implicit arguments, which are solved by running a tactic script or giving a default argument, rather than by unification.
Unit type
()
, empty typeVoid
Tuples (desugaring to nested pairs)
Dependent pair syntax
(x : T ** P x)
(there exists anx
of typeT
such thatP x
)Inline
case
expressionsHeterogeneous equality
do
notationIdiom brackets
Interfaces (like type classes), supporting default methods and dependencies between methods
rewrite
prfin
exprMetavariables
Inline proof/tactic scripts
Implicit coercion
codata
Also
Inf : Type -> Type
type constructor for mixed data/codata. In factcodata
is implemented by putting recursive arguments underInf
.syntax
rules for defining pattern and term syntactic sugarthese are used in the standard library to define
if ... then ... else
expressions and an Agda-style preorder reasoning syntax.Uniqueness typing using the
UniqueType
universe.Partial evaluation by
%static
argument annotations.Error message reflection
Eliminators
Label types
'name
%logging n
%unifyLog