Re: Proposal: Add singleton function to Data.List module

In the Agda code base there is a overloaded version of the singleton function. Even more useful in its overloaded form! https://github.com/agda/agda/blob/master/src/full/Agda/Utils/Singleton.hs As you can see here, singleton exists for many collection types already, it makes very much sense to have it also for List (and List.Nonempty). +1 on Data.List.singleton, (but please not in the Prelude). On 2019-08-12 20:36, Brent Yorgey wrote:

At the risk of completely derailing the conversation, I have always called this the "robot monkey operator".  I fail to see what is so ninja-like about it.

Anyway, I think I am +1 on adding Data.List.singleton.

-Brent

On Mon, Aug 12, 2019, 12:35 PM Zemyla mailto:zemyla@gmail.com> wrote:

I also like the ninja-robot operator, because it's visually interesting and easy to search for.

Also, if you're importing several libraries which already use "singleton", then you have to use "List.singleton" every time, which is far uglier to me.

On Mon, Aug 12, 2019 at 12:03 PM Herbert Valerio Riedel mailto:hvriedel@gmail.com> wrote: > > > - `(:[])`: Subjectively ugly. > > I consider "subjectively ugly" to be a non-technical and thus really > weak argument to dismiss the list-idiomatic ninja-robot-operator (:[]) > which also happens to be shorter than the proposed alias for it. I for > one don't see a significant benefit for adding a redundant synonym to > `Data.List` and are thus -1 on this. > > > singleton :: a -> [a] > > singleton x = [x]