[][src]Crate nar

Narc is a dependently-typed programming language with Agda style dependent pattern matching.

Goal

The purpose of this language is to realize the elaboration algorithm described in this paper.

The implementation is heavily inspired from Agda version 2.6.0.1. Special thanks to Jesper Cockx for answering my questions about the Agda codebase during the development of Narc.

I want this language to have:

  • Conversion check should be nominal for simplicity
  • Only case-tree instantiation need to be supported
  • Surface syntax should be considerate of parsing ease
  • Simple (co)inductive types (not indexed) with an identity type as described in Jesper's paper
    • It's not actually (co)inductive -- there's no termination or productivity checks yet
  • Definition by pattern matching according to Jesper's paper
  • Coverage check + case-tree generation described in Jesper's paper
  • Prefix (applying on projection) and postfix (projecting from data) projection (or maybe not?)

... and I plan to enhance everything in the next language after Narc, including (but not limited to):

  • Pattern instantiation, to see if we can prove things easier
  • Structural conversion check (or a partial one, like in mlang)
  • Totality check: termination/productivity
  • ... more?

... and even next language in the future:

  • Indexed data families, remove the built-in identity type
  • IDE mode like agda2-mode, but I'll go for both Code (primary) and Emacs (secondary)
  • De-morgan cubical primitives (Interval, Path, hcomp, transport, Glue)
  • ... more?

About the name, Narc This name is inspired from a friend whose username is Narc (or lwoo1999 on CodeWars and GitHub).
The real origin The word Narc is originated from the visual noval Narcissu.

Modules

check

Anything relevant to type-checking. Corresponds to Agda's Agda.TypeChecking.

syntax

Core language, abstract syntax, surface syntax, and the parser. Corresponds to Agda's Agda.Syntax.