There has been some informal discussion about changing the singleton list/vector [_] to a pattern synonym so that you can use it on the left hand side and write things like:
intersperse : List A -> A -> List A
intersperse [] _ = []
intersperse [ x ] _ = [ x ]
intersperse (x :: xs) y = x :: y :: intersperse xs y
However, swapping functions for (untyped) pattern synonyms is not backwards compatible so it hasn't been carried out yet.
In the meantime I propose that we redefine [_] to make it more powerful so we can write an arbitrary number of objects inside of the brackets as in other programming languages, e.g. [ 5 , 2 , 3 ]. This can be achieved by using _^_ from Data.Vec.Recursive as follows:
[_] : A ^ (suc n) → Vec A (suc n)
[_] x = toVec _ x
This is a backwards compatible change, and I don't think precludes making it a pattern in v2.0? @gallais
(although it may need a bit of rejigging to fix the dependency cycles)
There has been some informal discussion about changing the singleton list/vector
[_]to a pattern synonym so that you can use it on the left hand side and write things like:However, swapping functions for (untyped) pattern synonyms is not backwards compatible so it hasn't been carried out yet.
In the meantime I propose that we redefine
[_]to make it more powerful so we can write an arbitrary number of objects inside of the brackets as in other programming languages, e.g.[ 5 , 2 , 3 ]. This can be achieved by using_^_fromData.Vec.Recursiveas follows:This is a backwards compatible change, and I don't think precludes making it a pattern in v2.0? @gallais
(although it may need a bit of rejigging to fix the dependency cycles)