A toy dependently typed programming language with type-based termination.

MiniAgda is a tiny dependently-typed programming language in the style of Agda. It serves as a laboratory to test potential additions to the language and type system of Agda. MiniAgda's termination checker is a fusion of sized types and size-change termination and supports coinduction. Equality incorporates eta-expansion at record and singleton types. Function arguments can be declared as static; such arguments are discarded during equality checking and compilation. Recent features include bounded size quantification and destructor patterns for a more general handling of coinduction.

MiniAgda

A prototypical dependently typed languages with sized types and variances.

Installation

Requires ghc and cabal, for instance via the Haskell Platform or via ghcup. In a shell, type

  cabal update
  cabal install MiniAgda

To build MiniAgda from source, replace the last command with

 make

Examples

See directories test/succeed/ and examples/.

Some examples are commented on the (dormant) MiniAgda blog.