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

[ dependent-types, library, mit, program ] [ Propose Tags ] [ Report a vulnerability ]

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.


[Skip to Readme]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

Versions [RSS] 0.2014.1.9, 0.2014.5.5, 0.2014.9.12, 0.2016.12.19, 0.2017.2.18, 0.2018.11.4, 0.2018.11.6, 0.2019.3.29, 0.2019.12.13, 0.2020.4.14, 0.2022.3.11, 0.2025.7.23
Change log CHANGELOG
Dependencies array (>=0.3 && <0.6), base (>=4.9 && <5), containers (>=0.3 && <1), haskell-src-exts (>=1.21 && <1.22), MiniAgda, mtl (>=2.2.1 && <2.4), optparse-applicative (>=0.16.0.0 && <1), pretty (>=1.0 && <1.2), string-qq, transformers [details]
Tested with ghc ==9.12.2, ghc ==9.10.2, ghc ==9.8.4, ghc ==9.6.7, ghc ==9.4.8, ghc ==9.2.8, ghc ==9.0.2, ghc ==8.10.7, ghc ==8.8.4, ghc ==8.6.5, ghc ==8.4.4, ghc ==8.2.2, ghc ==8.0.2
License MIT
Author Andreas Abel and Karl Mehltretter
Maintainer Andreas Abel <andreas.abel@cse.gu.se>
Category Dependent types
Home page http://www.cse.chalmers.se/~abela/miniagda/
Bug tracker https://github.com/andreasabel/miniagda/issues
Source repo head: git clone https://github.com/andreasabel/miniagda
Uploaded by AndreasAbel at 2025-07-23T12:49:00Z
Distributions
Reverse Dependencies 1 direct, 0 indirect [details]
Executables miniagda
Downloads 7451 total (16 in the last 30 days)
Rating 2.0 (votes: 1) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2025-07-23 [all 1 reports]

Readme for MiniAgda-0.2025.7.23

[back to package description]

MiniAgda

Cabal build Hackage

A prototypical dependently typed languages with sized types and variances.

Installation from Hackage

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

  cabal update
  cabal install MiniAgda

Installation from Stackage

MiniAgda is not on Stackage because it depends on a specific version of haskell-src-exts rather than the latest version. You can install with stack from source though, see next section.

Installation from source

  1. Obtain the sources.

    git clone https://github.com/andreasabel/miniagda
    cd miniagda
    
  2. Checkout the desired version (optional): If you want to build a released version or a branch rather than the latest master, switch to this version/branch.

    git checkout $REF
    

    E.g. REF = v0.2022.3.11 for version 0.2022.3.11 or REF = unfold for branch unfold.

  3. Building and running the tests (optional).

    • With cabal (requires ghc in your PATH):

      cabal build --enable-tests
      cabal test
      

      After building, you can run MiniAgda locally, e.g.:

      cabal run miniagda -- examples/Gcd/gcd.ma
      
    • With stack:

      stack build --stack-yaml=stack-$GHCVER.yaml
      stack test  --stack-yaml=stack-$GHCVER.yaml
      

      At the time of writing (2025-07-23), GHCVER can be any of 9.12, 9.10, 9.8, 9.6, and some older ones.

      After building, you can run MiniAgda locally, e.g.:

      stack run --stack-yaml=stack-9.12.yaml -- examples/Gcd/gcd.ma
      

      You can copy stack-$GHCVER.yaml for your choice of GHCVER into stack.yaml and drop the --stack-yaml argument from stack invocation.

  4. Install.

    • With cabal (requires ghc in your PATH):
      cabal install
      
    • With stack:
      stack install --stack-yaml=stack-$GHCVER.yaml
      

    Note that the respective installation directory should be on your PATH.

Examples

See directories test/succeed/ and examples/.

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