將類型術語中的自由變量提升爲隱式函數參數

Question

爲了讓我的問題具有意義，我必須提供一些背景知識。

---

我認爲這將是非常有用的一個依賴性類型的語言，可以推斷論據a的存在和類型，其其它參數和/或返回值有依賴於a類型的函數。考慮語言下面的代碼片段我設計：

(* Backticks are used for infix functions *) 
def Cat (`~>` : ob -> ob -> Type) := 
    sig 
    exs id : a ~> a 
    exs `.` : b ~> c -> a ~> b -> a ~> c 
    exs lid : id . f = f 
    exs rid : f . id = f 
    exs asso : (h . g) . f = h . (g . f) 
    end 

如果我們做兩個（誠然，莫須有）假設：

1. 沒有依賴關係必須存在一個不能從明確提供的信息推斷。
2. 必須將每個自由變量轉換爲使用def或exs引入的最後一個標識符的隱式參數。

我們可以解釋上面的代碼等價於下列之一：

def Cat {ob} (`~>` : ob -> ob -> Type) := 
    sig 
    exs id : all {a} -> a ~> a 
    exs `.` : all {a b c} -> b ~> c -> a ~> b -> a ~> c 
    exs lid : all {a b} {f : a ~> b} -> id . f = f 
    exs rid : all {a b} {f : a ~> b} -> f . id = f 
    exs asso : all {a b c d} {f : a ~> b} {g} {h : c ~> d} 
       -> (h . g) . f = h . (g . f) 
    end 

這是或多或少一樣以下阿格達片段：

record Cat {ob : Set} (_⇒_ : ob → ob → Set) : Set₁ where 
    field 
    id : ∀ {a} → a ⇒ a 
    _∙_ : ∀ {a b c} → b ⇒ c → a ⇒ b → a ⇒ c 
    lid : ∀ {a b} {f : a ⇒ b} → id ∙ f ≡ f 
    rid : ∀ {a b} {f : a ⇒ b} → f ∙ id ≡ f 
    asso : ∀ {a b c d} {f : a ⇒ b} {g} {h : c ⇒ d} → (h ∙ g) ∙ f ≡ h ∙ (g ∙ f) 

顯然，二毫無根據的假設爲我們節省了大量的打字工作！

注意：當然，這種機制只有在原始假設成立的情況下才能發揮作用。例如，我們不能正確地推斷出相關的函數組合操作的隱含參數：

(* Only infers (?2 -> ?3) -> (?1 -> ?2) -> (?1 -> ?3) *) 
def `.` g f x := g (f x) 

在這種情況下，我們必須明確地提供一些額外的信息：

(* If we omitted {x}, it would become an implicit argument of `.` *) 
def `.` (g : all {x} (y : B x) -> C y) (f : all x -> B x) x := g (f x) 

可擴展到以下：

def `.` {A} {B : A -> Type} {C : all {x} -> B x -> Type} 
     (g : all {x} (y : B x) -> C y) (f : all x -> B x) x := g (f x) 

這裏是等效阿格達定義，爲了進行比較：

注意

---

的

_∘_ : ∀ {A : Set} {B : A → Set} {C : ∀ {x} → B x → Set} 
     (g : ∀ {x} (y : B x) → C y) (f : ∀ x → B x) x → C (f x) 
(g ∘ f) x = g (f x) 

末端是可行以上描述的機制？更好的是，有沒有實現類似這種機制的語言？

Answer 1

這聽起來像是implicit generalization in Coq.