Documentation #3

amyliao commented 2026年04月20日 14:24:22 +02:00

We've inherited Agda's documentation in the repo. I haven't stripped it of the branding yet. However, we could also take this as an opportunity to rewrite the documentation to be actual reference documentation, instead of the half-tutorial half-reference docs we have now.

We've inherited Agda's documentation in the repo. I haven't stripped it of the branding yet. However, we could also take this as an opportunity to rewrite the documentation to be actual *reference* documentation, instead of the half-tutorial half-reference docs we have now.

amyliao commented 2026年05月07日 23:56:45 +02:00

• In general I think there is very little purpose to tutorial-style content in the language reference (e.g. most of the module on records). A couple examples are fine, but the bulk of the content should be to the point, tuned for someone that wants to quickly clear something up. Tutorials can be in another section (or website...).
• Each section in the new docs should completely describe a feature, be it a part of the core type system or a form of top-level declaration. To an approximation, the following sections should be merged:
  • Function Types, Lambda Abstractions, and Telescopes
  • Universe Levels, Two-Level Type Theory, Prop, and Sort System
  • Function Definitions, Coverage Checking, Termination Checking, and Copatterns
  • Abstract definitions and Opaque definitions
  • Data Types and Positivity Checking
• The Cubical, Cubical compatible and Without K sections all need to be rewritten to stop sounding like they're describing optional additions and not parts of the core language. In particular:
  • Cubical compatible can just go entirely
  • The sections in Without K should be moved to their respective pages:
    • Restrictions on pattern matching and Restrictions on termination checking → Function Definitions
    • Restrictions on universe levels → Data Types

I also think that the docs should get a new top-level structure, but I'm unclear on what exactly it should look like. Maybe something like:

• Types and terms
  • Function types
  • Universes
  • Built-in data types (Nat, String, etc)
  • Syntactic sugar
  • Implicit and instance arguments
  • Metaprogramming???
• Declarations and definitions
  • Function definitions
    • with abstraction
  • Data types
  • Record types
  • Operator parsing, syntax declarations
  • Pattern synonyms
  • Postulates
  • Abstract and opaque definitions
  • Modules

Reorganizing like this would mean moving all of the command line options next to the things they control. I think the added locality is a good thing... Sphinx can still generate an index of all the options for quickly searching for one.

* In general I think there is very little purpose to tutorial-style content in the language reference (e.g. most of the module on records). A couple examples are fine, but the bulk of the content should be to the point, tuned for someone that wants to quickly clear something up. Tutorials can be in another section (or website...). * Each section in the new docs should completely describe a feature, be it a part of the core type system or a form of top-level declaration. To an approximation, the following sections should be merged: * `Function Types`, `Lambda Abstractions`, and `Telescopes` * `Universe Levels`, `Two-Level Type Theory`, `Prop`, and `Sort System` * `Function Definitions`, `Coverage Checking`, `Termination Checking`, and `Copatterns` * `Abstract definitions` and `Opaque definitions` * `Data Types` and `Positivity Checking` * The `Cubical`, `Cubical compatible` and `Without K` sections all need to be rewritten to stop sounding like they're describing optional additions and not parts of the core language. In particular: * `Cubical compatible` can just go entirely * The sections in `Without K` should be moved to their respective pages: + `Restrictions on pattern matching` and `Restrictions on termination checking` → `Function Definitions` + `Restrictions on universe levels` → `Data Types` I also think that the docs should get a new top-level structure, but I'm unclear on what exactly it should look like. Maybe something like: * Types and terms * Function types * Universes * Built-in data types (`Nat`, `String`, etc) * Syntactic sugar * Implicit and instance arguments * Metaprogramming??? * Declarations and definitions * Function definitions + `with` abstraction * Data types * Record types * Operator parsing, `syntax` declarations * Pattern synonyms * Postulates * Abstract and opaque definitions * Modules Reorganizing like this would mean moving all of the command line options next to the things they control. I think the added locality is a good thing... Sphinx can still generate an index of all the options for quickly searching for one.