Skip to content

Latest commit

 

History

History
153 lines (96 loc) · 6.82 KB

README.md

File metadata and controls

153 lines (96 loc) · 6.82 KB
Raw

Menkar - the multimode presheaf proof assistant

Menkar is (will be) a dependently typed programming language with a special focus on supporting modal and even multimode type systems, as well as type systems based on presheaf models.

It is named after the star Alpha Ceti.

2022 Update

The Menkar project has been on hold/discontinued since Fall 2019. The direct cause for this were performance issues in menkar reldtt (although menkar trivial seems to be working fine). Try for example

menkar reldtt src/code-examples/reldtt/paramdtt.menkar

and watch your memory usage go through the roof. The cause of this is very likely the choice to implement renaming/substitution of terms as a functor/monad structure:

  • Originally, this meant that every substitution (lazily) causes a full traversal of the syntax tree.

  • An attempt to solve this by guarding certain syntax constructors with Coyoneda allowed substitutions to be fused, but implied that the substitution had to be computed upon every inspection of the term.

Other aspects (elaboration, equality checking) can be improved using known techniques.

However, the development of Menkar was in general hampered by an insufficiently abstract treatment of the concepts of

  • a syntax constructor,

  • a syntax tree traversal/elimination.

The Analyzer part of the codebase makes a reasonable (hacky) abstraction to at least disentangle the two concepts a bit. I am currently working on a more principled approach, called contextual algebraic theories. Important aspects of the Menkar implementation - the design of the type-checking monad, for instance - may well be reused in a future implementation based on contextual algebraic theories.

Meanwhile, Team Aarhus is working on Mitten.

Features

Currently supported features include:

  • type-checking of multimode MLTT with natural numbers, Π- and Σ-types, empty, unit and box types, an identity type and function extensionality,
  • a command-line interaction mode that provides the user with a wealth of information, including stack traces for almost everything,
  • smart eliminations, including
    • implicit arguments in the sense of Agda,
    • named arguments,
    • implicit unboxing,
    • named and numbered projections for nested Σ-types.
  • internal crisp mode and modality polymorphism (with no semantics),
  • a single universe that (inconsistently) contains itself,
  • support for type systems in which type and term have a different modality, via a parametric function El : {par | Uni} -> UniHS from a well-behaved (e.g. fibrant) universe to a possibly ill-behaved (e.g. non-fibrant) Hofmann-Streicher-universe whose codes can be promoted to the type level continuously.

Partly implemented (but presently unusable) features include:

  • a definitional relatedness checker (coined by A. Vezzosi), which may allow for the non-consideration of irrelevant subterms during conversion-checking.

Considered features include:

  • a Hofmann-Streicher-universe of propositions, equipped with logic operators,

  • the coproduct type,

  • non-recursive HITs via a type former for pushouts along ΣBφ -> B (a codependent coproduct),

  • non-recursive QITs via a type former for pushouts along B + B -> B or via an interval modelled by the unit type,

  • smart constructors, perhaps including

    • implicit first components,
    • named first components,
    • implicit boxing,
    • named and numbered injections for coproduct-like types,

  • support for context exponentiation (for working with dependably atomic objects),

  • internal presheaf operators, to wit:

    • definitional extension types,

    • transpension types (a.k.a. amazing dependent right adjoints) for working with dependably atomic objects,

    • the final type extension operation Glue.

      From these, one can implement:

    • the strictness axiom as used, among others, by Orton and Pitts,

    • from strictness, the initial type extension operation Weld (and Glue again),

    • Moulin's Ψ-type, dubbed "Gel" by Cavallo and Harper.

  • instance arguments - a feature analogous to Agda's instance arguments and Haskell's typeclasses. A resolution is essentially a user-defined open ad-hoc function which takes the role of Agda's and Haskell's instance resolution. Instance arguments are arguments annotated with a resolution; their values need not be actively passed, as they can be resolved,

  • the resolution-features necessary to implement a relatedness-checker within Menkar,

  • perhaps, one day, definitional inequality and subtyping.

Type systems

Multimode modal type systems currently supported are:

  • the trivial system (1 mode, 1 modality, i.e. basic MLTT),
  • RelDTT a.k.a. degrees of relatedness, albeit with enormous performance issues,
  • hence also ParamDTT, which is essentially the mode 2 (depth 1) fragment of RelDTT,

We also aim to support:

  • cubical type theory,
  • directed type theory,
  • guarded type theory with multiple clocks and time warps.

Where applicable, the user should ideally have the option to include/exclude/agnosticlude diagonals, symmetries and connections in the base category, as well as generalize from binary to n-ary systems.

Quick start guide

Installation

git clone <...> menkar
cd menkar/menkar
stack install

Menkar is now installed as menkar.

Running

Type-check the concatenation of three files:

menkar trivial path/to/file1.menkar path/to/file2.menkar path/to/file3.menkar
menkar reldtt path/to/file1.menkar path/to/file2.menkar path/to/file3.menkar

Other remarks

Menkar is still in early development. We absolutely do not guarantee any form of backwards compatibility at this stage.

More info?

Submission at types: abstract - slides

Don't hesitate to contact me if this project sparks your interest.