是否可以注释函数的特殊属性(例如,主观性)？

Question

假设我有更高阶的功能f :: (a -> b) -> (a -> b).但f只有在输入函数是满射的情况下才能正常运行.反正有没有迫使这种情况发生在Haskell？例如,我真的希望f类型签名是这样的:

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

但这不起作用,因为我不希望a -> b声明该类型的所有函数都是满射的,只是其中的一部分.例如,可以f将满射函数转换为非满射函数.

我们可以将函数包装在一个特殊的数据类型中data Surjective f = Surjective f,然后定义

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

但这会使很难为函数分配多个属性.

在练习中有没有方便的方法呢？这在理论上是否可行？

Answer 1

这是一个如何在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

例如,id是outjective(一个简单的证明):

open import Function using ( id )

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

采用另一种仅适用于射影函数的身份函数:

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

我们可以通过id到id-for-surjective's其满射的证明作证:

id? : ? {a} {A : Set a} ? A ? A
id? = id-for-surjective's id {proof = id-is-surjective}

这id?与以下功能相同id:

id?id? : ? {a} {A : Set a} ? id {A = A} ? id?
id?id? = refl

试图传递非射影函数id-for-surjective's是不可能的:

open import Data.Nat using ( ? )

f : ? ? ?
f x = 1

f? : ? ? ?
f? = id-for-surjective's f {proof = {!!}} -- (y : ?) ? ? (? x ? f x ? y) (unprovable)

与之相似,许多其他特性可以以这样的方式来表达,阿格达的标准库已经具备必要的定义(例如Function.Surjection,Function.Injection,Function.Bijection等模块).