I was reading this excellent blog post, and came across the following line that I'm not sure what it does:

data NonEmpty a = a :| [a]

What is :| doing here? I tried this out in ghci but wasn't actually able to construct anything of this type.

CodePudding user response：

Compare it to this line:

data PrefixNonEmpty a = MkNonEmpty a [a]

Just like that line defines the (prefix) MkNonEmpty data constructor, your line defines the (infix) :| data constructor.