Discussion

[ice1000]

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?

[ice1000]

@AD1024 @zyh3838438zyh :wink:

[owo-bot]

OwO

[anqurvanillapy]

Typecheck ok gives 🐮🍺, and qutting REPL gives 🍵.

[ice1000]

Typecheck ok gives 🐮🍺, and qutting REPL gives 🍵.

I'm not doing this right now -- 🍵 is the output for scope-check failure. I tried 🌶🐔, but both Windows Terminal & VSCode console cannot display this properly.

[zypeh]

May I know is there a reason that you remove the row polymorphism?

I saw it from the Changelog 0.0.2 #1 but I can't find any documentation expressing the reason.

[anqurvanillapy]

May I know is there a reason that you remove the row polymorphism?

narc-rs is the language that implements core features from Agda, and voile-rs is the one that experiments with row polymorphism and dependent types.

[zypeh]

I see, I thought narc-rs would be superseding the voile-rs so I am expecting the row polymorphism feature. Got it!

[ice1000]

I see, I thought narc-rs would be superseding the voile-rs so I am expecting the row polymorphism feature. Got it!

I did some minor research in the first year and I've found row polymorphism to be unpleasant in a dependent type setting.

Btw, the effort has been moved to the Aya prover, you can take a look if you're interested. Currently we're working on some UX features and it's going to be published once the module, library, and releasing systems are ready