[ new ] Data.SnocList.Base (re #2684)#2982
Conversation
JacquesCarette
left a comment
JacquesCarette
left a comment
There was a problem hiding this comment.
One minor nitpick.
Otherwise, this would be a lovely test case for a "rich" metaprogramming setup where this fully commented source file ought to be derivable.
| infixl 5 _<:_ | ||
|
|
||
| data List< (A : Set a) : Set a where | ||
| [<] : List< A |
There was a problem hiding this comment.
Part of me likes the clean separation of the constructors, going as far as to rename [] but I can't help thinking this is a case where the ability to overload constructor types/reuse constructor names is a virtue.
Would there be a problem with using [] throughout?
|
|
||
| data List< (A : Set a) : Set a where | ||
| [<] : List< A | ||
| _<:_ : List< A → A → List< A |
There was a problem hiding this comment.
Separately to the above, but related, the library expends considerable effort on 'left'/'right' superscript designators for concepts which arise as 'handed' notions.
I fully understand the different (symbolic/naming) legacy which this PR draws on (including 'fish' and 'chips'... ) and in this instance it may be a case of having constructor symbols clash with defined function names ... but why not _∷ˡ_ and _∷ʳ_ instead?
... and then fish and chips become eg _ˡ++ʳ_ and _ʳ++ˡ_ which would be 'more stdlib-like'...?
There was a problem hiding this comment.
Worth having the discussion. I rather like the current names in Snoc. (I think we over-use left/right, to be honest; but that's a complete-rewrite issue, not even an item worth contemplating in v3.0). _ˡ++ʳ_ is not nice at all, IMHO.
There was a problem hiding this comment.
and then fish and chips become eg
_ˡ++ʳ_and_ʳ++ˡ_which would be 'more stdlib-like'...?
Note that fish & chips additionally document the type of the output whereas these do not
There was a problem hiding this comment.
Not a hill I planned to die on, but I think that 'consistency' in naming ('style') is something worth striving for...
Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
3 participants
This is offering feature parity with
Data.List.Base(+ additional functions like fish & chips)In the process, I fixed a bug in
Data.List.Base:linesBywas trying to be too clever aboutempty lines when it's just more principled to return a trailing empty line if there is indeed
a trailing newline character at the end of the string being considered.