Appending an option to a list

Stream: general

[Eric Wieser]

Does this function have a name somewhere?

def cons? {α} (l : List α) : Option α → List α
  | none => l
  | some a => a :: l

Can I get it without a match with some monad transform?

[Mauricio Collares]

Is (·.toList ++ l) cheating?

[Damiano Testa]

Is (a::l.map some).reduceOption cheating?

[Chris Bailey]

What's wrong with the match?

[Adam Topaz]

Is if let some a := x then a :: l else l cheating?

[Mauricio Collares]

Damiano Testa said:

Is (a::l.map some).reduceOption cheating?

This one's linear time, I think. At least

def main := do
  let l := List.replicate 10000000 1
  for i in [1:1000] do
    IO.println <| List.take 100 <| cons? l (some i)

is slow.

[Marcus Rossel]

Is a.elim l l.conscheating?

[Chris Bailey]

Final offer: (a.map xs.cons).getD xs

[Kyle Miller]

Mauricio's is nice for mentioning each variable just once.

Here's a similar one for fun, but won't win in golf.

def cons? {α} (x? : Option α) : List α → List α := (x?.map List.cons).getD id