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.
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
Coyonedaallowed 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.
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} -> UniHSfrom 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 -> Bor 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.
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.
git clone <...> menkar
cd menkar/menkar
stack install
Menkar is now installed as menkar.
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
Menkar is still in early development. We absolutely do not guarantee any form of backwards compatibility at this stage.
Submission at types: abstract - slides
Don't hesitate to contact me if this project sparks your interest.