Proposal: Add singleton function to Data.List module

[Andreas Abel]

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 <zemyla at gmail.com 
> <mailto:zemyla at 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
>     <hvriedel at gmail.com <mailto:hvriedel at 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]