Here's my initial thoughts about this language:
- 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?
Here's my initial thoughts about this language:
... and I plan to enhance everything in the next language after Narc, including (but not limited to):
... and even next language in the future:
agda2-mode, but I'll go for both Code (primary) and Emacs (secondary)