Say I’d like to introduce a concise notation for partial functions, represented by total functions of type
'a ⇒ 'b option. I want users to be able to write
π⟨pattern⟩. ⟨expression⟩ and have this translated to
λx. case x of ⟨pattern⟩ ⇒ Some ⟨expression⟩ | _ ⇒ None. I’ve tried to do this with
translations, but this doesn’t seem to be possible, because I have to introduce the new, probably fresh, variable
x on the right-hand side. How can I implement syntax translations that introduce bound variables like in this example?
So you do not like
I don’t see how
map_option would help here. Can you please enlighten me?
Also, what I actually want to implement is a bit more complex.
You are trying to do:
map_option (%x. f x) \pi
so do you really need a new syntax for it?
wait you want to do something even weirder
It’s not weird. I want to write a partial function.
Why not use do notation?
My actual use case is more complex. Above, I just used a sort of minimal example to explain the technical problem. It’s a solution to this technical problem I’m seeking, not recommendations how to do things differently.
Last updated: Dec 07 2023 at 08:19 UTC