Hackage :: [Package]

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

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain] [Publish]

Warnings:

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]

Properties

Versions 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, 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]
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:46:33Z

Modules

[Index] [Quick Jump]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

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.