feat: add Alternative.many #1595
Conversation
github-actions
bot
added
the
awaiting-review
|
Please add a copyright header and follow style from similar files. |
fgdorais
added
awaiting-author
fgdorais
changed the title
414owen
force-pushed
the
os/alternative-many
branch
from
7fc04f7 to
65ab39c
Compare
|
I made a few minor edits, mostly so that CI works. I hope you don't mind, it was easier to do than to explain. PS: Avoid force push. |
Absolutely fine. Be my guest. |
|
Mathlib CI status (docs):
|
Batteries/Control/Alternative.lean
Outdated
| def many1 [Alternative f] | ||
| (p : f α) : f (Σ n, Vector α (1 + n)) := | ||
| let g x xs := ⟨xs.1, Vector.singleton x ++ xs.2⟩ | ||
| let toVec (l : List α) : Σ n, Vector α n := | ||
| let arr := List.toArray l | ||
| ⟨arr.size, ⟨arr, rfl⟩⟩ | ||
| let manyVec : f (Σ n, (Vector α n)) := toVec <$> Alternative.many p | ||
| g <$> p <*> manyVec <|> Alternative.failure |
There was a problem hiding this comment.
Happy to wait for pending Zulip discussion; but the two many1 functions in Lean already are the much simpler
| def many1 [Alternative f] | |
| (p : f α) : f (Σ n, Vector α (1 + n)) := | |
| let g x xs := ⟨xs.1, Vector.singleton x ++ xs.2⟩ | |
| let toVec (l : List α) : Σ n, Vector α n := | |
| let arr := List.toArray l | |
| ⟨arr.size, ⟨arr, rfl⟩⟩ | |
| let manyVec : f (Σ n, (Vector α n)) := toVec <$> Alternative.many p | |
| g <$> p <*> manyVec <|> Alternative.failure | |
| def many1 [Alternative f] (p : f α) : f (List α) := | |
| List.cons <$> p <*> many p |
in the absence of a concrete use case requiring the complexity, I'd be inclined to pick this much simpler option.
There was a problem hiding this comment.
(note that independently, the <|> Alternative.failure looks like a no-op to me)
There was a problem hiding this comment.
def many1 [Alternative f] (p : f α) : f (List α) :=
List.cons <$> p <*> many p
I'm not a huge fan of this version to be honest. It means that, even though you know there's at least one element, operations like head, and tail are partial.
It throws away useful information, and goes against "make error states unrepresentable" / "parse, don't validate", etc.
There was a problem hiding this comment.
True, but my proposal is consistent with Std.Internal.Parsec.many1 from the standard library.
There was a problem hiding this comment.
That is something I can't deny :)
The design for `many1` doesn't seem very clear-cut, it's sparked quite a bit of discourse in zulip: https://leanprover.zulipchat.com/#narrow/channel/348111-batteries/topic/Nonempty.20List.20Type/with/567406954 Let's defer it to another PR.
|
Since |
414owen
changed the title
4 participants
Closes #1577