wball/perga
1
0
Fork 0
Code Issues 15 Pull requests Projects Releases Packages Wiki Activity Actions

updated TODOs

Browse source
This commit is contained in:
William Ball 2024-11-14 22:02:25 -08:00
parent 51d97b15f5
commit f1d5fc7574
1 changed files with 9 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
README.md
View file

@ -68,12 +68,12 @@ Obviously not fully decidable, but I might be able to implement some basic unifi
### TODO Implicits
Much, much more useful than [inference](#orgda125c7), implicit arguments would be amazing. It also seems a lot more complicated, but any system for dealing with implicit arguments is far better than none.
Much, much more useful than [inference](#org21ef5f7), implicit arguments would be amazing. It also seems a lot more complicated, but any system for dealing with implicit arguments is far better than none.
### TODO Universes?
Not really necessary without [inductive definitions](#org0f7d084), but could be fun.
Not really necessary without [inductive definitions](#org4227b35), but could be fun.
### TODO Inductive Definitions
@ -101,14 +101,19 @@ The error messages currently aren’t terrible, but it would be nice to have
### TODO Improve β-equivalence check
The check for β-equivalence could certainly be a lot smarter. Right now it just fully normalizes both terms and checks if the normal forms are equal, which isn’t the best strategy. This is much less of an issue without [inductive definitions](#org0f7d084)/recursion, as far less computation gets done in general, let alone at the type level. That being said, it’s certainly not a bad idea.
The check for β-equivalence could certainly be a lot smarter. Right now it just fully normalizes both terms and checks if the normal forms are equal, which isn’t the best strategy. This is much less of an issue without [inductive definitions](#org4227b35)/recursion, as far less computation gets done in general, let alone at the type level. That being said, it’s certainly not a bad idea.
### TODO Better testing
### DONE Better testing
Using some kind of testing framework, like [QuickCheck](https://hackage.haskell.org/package/QuickCheck) and/or [HUnit](https://hackage.haskell.org/package/HUnit) seems like a good idea. I would like to avoid regressions as I keep working on this, and a suite of unit tests would make me feel much more comfortable.
### DONE Switch to `Text`
Currently I use `String` everywhere. Switching to `Text` should be straightforward, and would improve performance and Unicode support.
### TODO TUI
This is definitely a stretch goal, but I’m imagining a TUI split into two panels. On the left you can see the term you are building with holes in it. On the right you have the focused hole’s type as well as the types of everything in scope (like Coq and Lean show while you’re in the middle of a proof). Then you can interact with the system by entering commands (e.g. `intros`, `apply`, etc.) which changes the proof term on the left. You’d also just be able to type in the left window as well, and edit the proof term directly. This way you’d get the benefits of working with tactics, making it way faster to construct proof terms, and the benefits of working with proof terms directly, namely transparency and simplicity. I’ll probably want to look into [brick](https://hackage.haskell.org/package/brick) in order to make this happen.