Promouvoir des variables libres dans les termes de type aux arguments de fonction implicites

Question

Pour que ma question soit significative, je dois fournir quelques informations de base.

---

je pense qu'il serait utile d'avoir un langage typé qui peut dépendamment déduire l'existence et le type d'un argument a pour une fonction dont les autres paramètres et/ou de la valeur de retour ont des types qui dépendent a. Considérons l'extrait suivant dans une langue que je suis la conception:

(* 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 

Si nous faisons deux hypothèses (certes, injustifiées):

1. Aucune dépendance doit exister qui ne peut être déduite de l'information fournie explicitement.
2. Chaque variable libre doit être convertie en un argument implicite du dernier identificateur introduit en utilisant def ou exs.

On peut interpréter l'extrait ci-dessus comme étant équivalente à la suivante:

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 

Ce qui est plus ou moins la même chose que l'extrait Agda suivant:

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) 

De toute évidence, deux hypothèses injustifiées nous ont sauvé beaucoup de dactylographie!

Remarque: Bien entendu, ce mécanisme ne fonctionne que tant que les hypothèses d'origine sont vérifiées. Par exemple, on ne peut pas déduire correctement les arguments implicites de l'opérateur de composition de fonction dépendante:

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

Dans ce cas, nous devons fournir explicitement des informations supplémentaires:

(* 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) 

qui peut être étendue dans la suit:

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) 

est ici l'équivalent définition Agda, à titre de comparaison:

_∘_ : ∀ {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) 

Fin de la note

---

Le mécanisme décrit ci-dessus réalisable? Mieux encore, existe-t-il un langage qui implémente quelque chose ressemblant à ce mécanisme?

Answer 1

Cela ressemble à implicit generalization in Coq.