Skip to content

Instantly share code, notes, and snippets.

@thealmarty

thealmarty/totalityCheckerPlan.md Secret

Last active April 23, 2020 16:57
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save thealmarty/2e58f3949d1ff2bac926a2313c7d6a75 to your computer and use it in GitHub Desktop.
Save thealmarty/2e58f3949d1ff2bac926a2313c7d6a75 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
totalityCheckerPlan.md

MVP Totality checker implementation plan

The implementation of the totality checker can be split into a few smaller, separate tasks/PRs for smoother transition and easier testing.

The goal of the MVP is to add:

  • positivity check: data type declarations should be strictly positive, i.e., in every constructor argument, the data type to be defined is not allowed to occur in a function domain or in an application.
  • pattern matching coverage check: for function declaration patterns should cover all cases.
  • termination check: functions should terminate.

First stage: update current type checker

Currently, the type checker only has terms or expressions. We will need to add a few more expressions, data type declarations, pattern matching, and function declarations. (Declarations contain expressions.)

At the end of this stage, all the above are defined, and expressions are checked. Signatures are stored in a state monad.

let declarations can also be added if desired.

Tests can be written for expressions.

Second stage: check data type declarations (including strict positivity check)

Add type checking of data declarations, which includes type checking of constructor, which includes strict positivity checks.

Tests can be written for data declarations.

Third stage: check function declarations (including patterns)

Add type checking of function declarations, which includes type checking of patterns and clauses of functions.

Tests can be written for function declarations.

Fourth stage: check pattern matching coverage

Add check to make sure that function declarations cover all cases, following thesis describing Agda (section 2.2).

Tests can be written to make sure the pattern matching coverage checks are valid.

Fifth stage: check function declarations terminate (syntactic checks)

Follow section 4 of a very early version of miniAgda.

Tests for the check.

Sixth stage: check function declarations terminate (type-based checks)

Follow section 5 of a very early version of miniAgda.

Tests for the check.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment