为什么函数组合(∘
)和应用($
)已在https://github.com/agda/agda-stdlib/blob/master/src/Function.agda#L74-L76可用的执行?复制在这里为了方便:
_∘_ : ∀ {a b c}
{A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
(∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
((x : A) → C (g x))
f ∘ g = λ x → f (g x)
_∘'_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
(B → C) → (A → B) → (A → C)
f ∘' g = λ x → f (g x)
_$_ : ∀ {a b} {A : Set a} {B : A → Set b} →
((x : A) → B x) → ((x : A) → B x)
f $ x = f x
_$'_ : ∀ {a b} {A : Set a} {B : Set b} →
(A → B) → (A → B)
f $' x = f x
我最初以为这背后的理由是,$
将能够处理更高的秩序类型$'
将无法处理。例如,考虑A = NAT,B =名单,f是::,其中B依赖于A.但是大量的测试后,我无法想出这将表明$'
的实施不充分的例子。什么情景呢$
搞定$'
不能办理? (同样,什么样的情况呢∘
搞定∘'
不?
open import Agda.Builtin.Nat public
open import Agda.Primitive public
--data List {a} (A : Set a) : Set a where
-- [] : List A
-- _∷_ : (x : A) (xs : List A) → List A
data Vec {a} (A : Set a) : Nat → Set a where
[] : Vec A zero
_∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)
tail : ∀ {a n} {A : Set a} → Vec A (suc n) → Vec A n
tail (x ∷ s) = s
_$_ : ∀ {a b} {A : Set a} {B : A → Set b} →
((x : A) → B x) → ((x : A) → B x)
f $ x = f x
_$'_ : ∀ {a b} {A : Set a} {B : Set b} →
(A → B) → (A → B)
f $' x = f x
_∘_ : ∀ {a b c}
{A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
(∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
((x : A) → C (g x))
f ∘ g = λ x → f (g x)
_∘'_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
(B → C) → (A → B) → (A → C)
f ∘' g = λ x → f (g x)
Vecc : ∀ {a} → Nat → (A : Set a) → (Set a)
Vecc x y = Vec y x
data Pair {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
_,_ : (x : A) → (y : B x) → Pair A B
-- Dependent Pair attempt
--fst : ∀ {a b} {A : Set a} {B : A → Set b} → Pair A B → A
--fst (a , b) = a
--
--f : Pair Nat $' Vec Nat
--f = _,_ zero $' []
--
--g : Pair (Pair Nat $' Vec Nat) $' λ x → Nat
--g = _,_ (_,_ zero $' []) $' zero
-- Some other attempt
--f : ∀ {a n} {A : Set a} → Vec A ((suc ∘' suc) n) → Vec A n
--f {a} = tail {a} ∘' tail {a}
-- Vec attempt
--f : ∀ {a} (A : Set a) → (Set a)
--f {a} = Vecc {a} (suc zero) ∘' Vecc {a} (suc zero)
--
--h = f Nat
--
--x : h
--x = (zero ∷ []) ∷ []
-- List attempt
--f : ∀ {a} (A : Set a) → (Set a)
--f {a} = List {a} ∘' List {a}
--
--g : ∀ {a} (A : Set a) → (Set a)
--g {a} = List {a} ∘ List {a}
--
--h = f Nat
--i = g Nat
--
--x : h
--x = (zero ∷ []) ∷ []
∘′
和$′
不依赖职能的工作。你根本没有尝试与相关的功能的任何测试。对于f $ x
例子,f
必须依赖,对于f ∘ g
,任一的功能必须依赖。例:
open import Data.Nat
open import Data.Vec
open import Function
open import Relation.Binary.PropositionalEquality
replicate' : {A : Set} → A → (n : ℕ) → Vec A n
replicate' a n = replicate a
refl' : {A : Set}(a : A) → a ≡ a
refl' a = refl
-- fail1 : Vec ℕ 10
-- fail1 = replicate' 10 $′ 10
ok1 : Vec ℕ 10
ok1 = replicate' 10 $ 10
-- fail2 : ∀ n → replicate' 10 n ≡ replicate' 10 n
-- fail2 = refl' ∘′ replicate' 10
ok2 : ∀ n → replicate' 10 n ≡ replicate' 10 n
ok2 = refl' ∘ replicate' 10
一个与相关功能的工作原理,其他没有,因为安德拉斯科瓦奇提及。
最重要的区别在于,对于非相关的功能可以被构造更强证明。例如:
eq : {A B} -> f : (A -> B) -> x y : A -> x == y -> (f x) == (f y)
eq f x .x refl = refl
在这里,我们可以构建f x
和f y
的平等。但是,我们不能对相关功能做同样的 - 因为没有办法证明B x == B y
。所以只有一个较弱的证明f x
可以“投”到f y
。
transport : {A} {B : A -> Set} -> f : (x : A -> B x) -> x y : A -> x == y -> f x -> f y
transport f x .x refl fx = fx
(实际上,transport
通常被定义为B x -> B y
,而不是依赖功能;但我不能想出更好的名字)