Is it possible to annotate a function's special properties (e.g. surjectivity)?

Question

Let's say I have a higher order function f :: (a -> b) -> (a -> b). But f only behaves properly if the input function is surjective. Is there anyway to force this to happen in Haskell? For example, I really want f's type signature to be something like:

f :: (Surjective (a -> b)) => (a -> b) -> (a -> b)

But this doesn't work because I don't want all functions of the type a -> b to be declared to be surjective, only some of them. For example, maybe f converts a surjective function into a non-surjective function.

We could wrap the functions in a special data type data Surjective f = Surjective f, and define

f :: Surjective (a -> b) -> (a -> b)

but this would make it difficult to assign multiple properties to a function.

Is there any convenient way to do this in practice? Is this even possible in theory?

Answer 1

This is an example of how surjectivity can be expressed in Agda:

module Surjectivity where

open import Data.Product using ( ∃; ,_ )
open import Relation.Binary.PropositionalEquality using ( _≡_; refl )

Surjective : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Set _
Surjective {A = A} {B = B} f = ∀ (y : B) → ∃ λ (x : A) → f x ≡ y

For example, id is surjective (a simple proof):

open import Function using ( id )

id-is-surjective : ∀ {a} {A : Set a} → Surjective {A = A} id
id-is-surjective _ = , refl

Taking another identity function which works only for surjective functions:

id-for-surjective's : ∀ {a b} {A : Set a} {B : Set b} → (F : A → B) → {proof : Surjective F} → A → B
id-for-surjective's f = f

we can pass id to id-for-surjective's with its surjectivity proof as witness:

id′ : ∀ {a} {A : Set a} → A → A
id′ = id-for-surjective's id {proof = id-is-surjective}

so that id′ is the same function as id:

id≡id′ : ∀ {a} {A : Set a} → id {A = A} ≡ id′
id≡id′ = refl

Trying to pass a non-surjective function to id-for-surjective's would be impossible:

open import Data.Nat using ( ℕ )

f : ℕ → ℕ
f x = 1

f′ : ℕ → ℕ
f′ = id-for-surjective's f {proof = {!!}} -- (y : ℕ) → ∃ (λ x → f x ≡ y) (unprovable)

Similary, many other properties can be expressed in such manner, Agda's standard library already have necessary definitions (e.g. Function.Surjection, Function.Injection, Function.Bijection and other modules).