the semantics of inv :: (a -> b) -> (b -> a)

From: Sebastian Hanowski <>
Date: Fri, 07 Mar 2008 11:23:17 +0100


a while ago Sebastian Fischer posted (among other things) this
interesting program:

        inv :: (a -> b) -> (b -> a)
        inv f b | f(a) =:= b = a where a free

Let's try to give it a precise semantics when applied to total functions
with a discrete codomain.

We first observe that when a pure function (f :: a -> b) isn't *onto*
then ((inv f) :: b -> a) is a partial function defined only on a subset
of the set of all elements of type b.

And second when (f :: a -> b) isn't *one-to-one* then
((inv f) :: b -> a) is non-deterministic, returning subsets of the set
of all elements of type a.

Making this explicit with an /inverse image/ operation couldn't be

        type Sub a = a -> Success

        (*) :: (a -> b) -> (Sub b -> Sub a)
        (f* v) a = v(f(a))

But since Curry supports existential quantification via free variables
we can also do this in the other direction with a /direct image/

        (#) :: (a -> b) -> (Sub a -> Sub b)
        (f# u) b = let a free in u(a) & f(a) =:= b

The relation between those two operations is that of an adjunction, i.e.
for any (f :: a -> b), (u :: Sub a) and (v :: Sub b) it holds that the
direct image of u under f is contained in v exactly when u is contained
in the inverse image of v under f.

        (f# u) \subset v iff u \subset (f* v)

(If /failed/ is observable in Curry than we must add the condition that
the predicates u,v and the function f don't mention each other, I

We can now characterise inv with laws like

        (f# u) \subset v iff u \subset ((inv f)# v)

What other - probably more interesting - laws are there? I've only just
begun to explore this.

curry mailing list
Received on Fr Mär 07 2008 - 11:45:28 CET

This archive was generated by hypermail 2.3.0 : Sa Jul 24 2021 - 07:15:04 CEST