Show Either
Some checks are pending
Publish Playground / build (push) Waiting to run
Publish Playground / deploy (push) Blocked by required conditions

This commit is contained in:
2025-12-26 19:52:18 -08:00
parent d19f39fa18
commit 70348f3e5d
2 changed files with 17 additions and 8 deletions

15
TODO.md
View File

@@ -2,26 +2,31 @@
## TODO ## TODO
- [ ] "Expected keyword" at `\ a ->` should be error at the `->` - [ ] "Expected keyword" at `\ a ->` should be error at the `->`
- [ ] Show Either - [x] Show Either
- [ ] `local` for `where`-like `let` clauses? (I want a `where` that closes over more stuff) - [ ] `local` for `where`-like `let` clauses? (I want a `where` that closes over more stuff)
- I can do `let f : ... = \ a b c => ...`. But it doesn't work for recursion and cases are awkward. - I can do `let f : ... = \ a b c => ...`. But it doesn't work for recursion and cases are awkward.
- [x] Erasure checking happens at compile time and isn't surfaced to editor.. - [x] Erasure checking happens at compile time and isn't surfaced to editor..
- [ ] Erasure issue during AoC from case building replacing a non-erased value with erased. - [ ] Erasure issue during AoC from case building replacing a non-erased value with erased.
- [ ] Add Foldable? - [ ] Add Foldable?
- [ ] "Failed to unify %var0 and %var1" - get names in there - [ ] "Failed to unify %var0 and %var1" - get names in there
- Need fancier `Env` - Need fancier `Env` or the index...
- Editor support:
- [ ] add missing cases should skip indented lines - [ ] add missing cases should skip indented lines
- [ ] add missing cases should handle `_::_` - [ ] add missing cases should handle `_::_`
- [ ] add missing cases should share code between vscode and playground
- [ ] "Not in scope" should offer to import - [ ] "Not in scope" should offer to import
- [ ] Dependent records (I guess I missed that bit) - [ ] Dependent records (I guess I missed that bit)
- [ ] Arguments on records - [ ] Arguments on records
- [ ] Add sugar for type aliases (maybe infer arguments) - [ ] Add sugar for type aliases (maybe infer arguments)
- [ ] see if we can get a better error on `for` instead of `for_` in do blocks - Lean has this, we maybe could run infer on the RHS and call it a day? We would need a simple LHS, though.
- [ ] Maybe make the editor json more compact - [ ] see if we can get a better error if `for` is used instead of `for_` in do blocks
- [ ] Maybe make the editor json more compact (we want to replace this with REPL / LSP though)
- [ ] Remove erased args from primitive functions - [ ] Remove erased args from primitive functions
- But we need separate `+` functions rather than the magic `∀ a. a -> a -> a` to support other backends - But we need separate `+` functions rather than the magic `∀ a. a -> a -> a` to support other backends
- [ ] consider moving primitive functions to a support file - [ ] consider moving primitive functions to a support file
- Downside here is that we lose some dead code elimination, but it better supports bootstrapping when calling convention changes. - Downside here is that we lose some dead code elimination
- it better supports bootstrapping when calling convention changes.
- it better supports other
- [ ] Alternate backend - [ ] Alternate backend
- Options are scheme, C, WASM, arm assembly. Maybe C is the next step. - Options are scheme, C, WASM, arm assembly. Maybe C is the next step.
- [ ] allow declaration of primitive operators - [ ] allow declaration of primitive operators

View File

@@ -899,6 +899,10 @@ instance ∀ a. {{Show a}} → Show (Maybe a) where
show Nothing = "Nothing" show Nothing = "Nothing"
show (Just a) = "Just \{show a}" show (Just a) = "Just \{show a}"
instance a b. {{Show a}} {{Show b}} Show (Either a b) where
show (Left a) = "Left \{show a}"
show (Right b) = "Right \{show b}"
pfunc isPrefixOf uses (True False): String String Bool := `(pfx, s) => s.startsWith(pfx) ? Prelude_True : Prelude_False` pfunc isPrefixOf uses (True False): String String Bool := `(pfx, s) => s.startsWith(pfx) ? Prelude_True : Prelude_False`
pfunc isSuffixOf uses (True False): String String Bool := `(pfx, s) => s.endsWith(pfx) ? Prelude_True : Prelude_False` pfunc isSuffixOf uses (True False): String String Bool := `(pfx, s) => s.endsWith(pfx) ? Prelude_True : Prelude_False`
pfunc strIndex : String Int Char := `(s, ix) => s[ix]` pfunc strIndex : String Int Char := `(s, ix) => s[ix]`