Discussion - Githubissues

ice1000 commented 5 years ago

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 commented 5 years ago

@AD1024 @zyh3838438zyh :wink:

owo-bot commented 5 years ago

OwO

anqurvanillapy commented 4 years ago

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

ice1000 commented 4 years ago

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 commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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

ice1000 commented 3 years ago

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

owo-lang / narc-rs

Discussion #2