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