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 and a 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 type Void

  • Tuples (desugaring to nested pairs)

  • Dependent pair syntax (x : T ** P x) (there exists an x of type T such that P x)

  • Inline case expressions

  • Heterogeneous equality

  • do notation

  • Idiom brackets

  • Interfaces (like type classes), supporting default methods and dependencies between methods

  • rewrite prf in expr

  • Metavariables

  • Inline proof/tactic scripts

  • Implicit coercion

  • codata

  • Also Inf : Type -> Type type constructor for mixed data/codata. In fact codata is implemented by putting recursive arguments under Inf.

  • syntax rules for defining pattern and term syntactic sugar

  • these 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