Wolfgang Jeltsch (Jul 28 2023 at 12:24): Wolfgang Jeltsch (Jul 28 2023 at 12:24):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 syntax and 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?
Mathias Fleury (Jul 30 2023 at 20:07):So you do not like map_option?
Wolfgang Jeltsch (Jul 31 2023 at 12:13):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.
Mathias Fleury (Jul 31 2023 at 12:18):You are trying to do:
map_option (%x. f x) \pi
so do you really need a new syntax for it?
Mathias Fleury (Jul 31 2023 at 12:19):wait you want to do something even weirder
Wolfgang Jeltsch (Jul 31 2023 at 12:19):It’s not weird. I want to write a partial function.
Lukas Stevens (Aug 12 2023 at 10:18):Why not use do notation?
Wolfgang Jeltsch (Aug 12 2023 at 12:49):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 21 2024 at 12:33 UTC