copier1 / aya-dev

~ Youkai (∞, 1)-Mountain

Website contains:

• Development blogs which are written for general audience
• Installation instructions (basically telling you what to download in GitHub Releases)
• Tutorial for Haskellers

Aya is under active development, so please expect bugs, usability or performance issues (please file issues or create threads in discussions!).

Showcase

• Dependent types, including pi-types, sigma types, indexed families, etc. You could write a type-safe interpreter.
• De Morgan cubical type theory with generalized path types similar to a bounded cubical subtype.
  • Implementation prototype: Guest0x0.
  • Demonstration of higher inductive types: 3-torus (three dimensional torus!!).
• Pattern matching with first-match semantics. Checkout the red-black tree (without deletion yet).
• Overlapping and order-independent patterns. Very useful in theorem proving.
• A literate programming mode with inline code fragment support. We already have a prototype, but we plan to revise it before sharing demos.
• Binary operators, with precedence specified by a partial ordering (instead of a number, such as in Haskell or Agda) which is useful for equation reasoning.
• A fairly good termination checker that does not assume predicativity. We adapted some code from Agda's implementation to accept more definitions (which are rejected by, e.g. Arend).
• Inference of type checking order. That is to say, no syntax for forward-declarations is needed for mutual recursions, induction-recursion, or induction-induction.
• See also stdlib candidates style guide. We have a grand plan!

See also use as a library.

Contributing to Aya

Since you need Java 19 to set this project up, in case your choice of IDE is IntelliJ IDEA, version 2022.3 or higher is required.

• Questions or concerns are welcomed in the discussion area. We will try our best to answer your questions, but please be nice.
• We welcome nitpicks on error reporting! Please let us know anything not perfect. We have already implemented several user-suggested error messages.
• Before contributing in any form, please read the contribution guideline thoroughly and make sure you understand your responsibilities.
• Please follow the Code of Conduct to ensure an inclusive and welcoming community atmosphere.
• Ask @ice1000 to become an organization member.
  • If you want to contribute, ask before doing anything. We are reluctant to accept PRs that contradict our design goals. We value your time and enthusiasm, so we don't want to close your PRs :)

Use as a library

It's indexed in mvnrepository, and here are some example build configurations:

<!-- Maven -->
<dependency>
    <groupId>org.aya-prover</groupId>
    <artifactId>[project name]</artifactId>
    <version>[latest version]</version>
</dependency>

// Gradle
implementation group: 'org.aya-prover', name: '[project name]', version: '[latest version]'

• [project name] specifies the subproject of Aya you want to use, and the options are pretty, base, cli, parser, etc.
  • The type checker lives in base and parser.
  • The generalized pretty printing framework is in pretty.
  • The generalized binary operator parser, generalized tree builder, generalized mutable graph, and a bunch of other utilities (strings, files, etc.) are in tools.
  • The command and argument parsing framework is in tools-repl. It offers an implementation of ANTLR4-based jline3 parser and relevant facilities.
• [latest version] is what you see on this badge .