Suppose we have a function `f :: a -> b`

and a function `g :: b -> a`

such that `f . g = id`

. You might say that `g`

is the “inverse” of `f`

(and vice versa). Could we then pattern match on something like `f x`

on the left hand side by replacing occurences of `x`

with `g x`

on the right hand side? For example:

`-- Here, (- 3) is the "inverse" of (+ 3), or more generally, (- n) is the "inverse" of (+ n) subtractThree (x + 3) = x subtractThree x = (x - 3) `

This just randomly came to my mind and I’m wondering if there is something fundamentally wrong with this.

Edit: This is my first post here and I’m unsure whether this is the right kind of question for this community. Please don’t hesitate to close this if this doesn’t belong here.