This sounds like implicit generalization in Coq.
Promoting free variables in type terms to implicit function arguments
-
16-01-2022 - |
Pregunta
In order for my question to be meaningful, I must provide some background.
I think it would be useful to have a dependently typed language that can infer the existence and type of an argument a
for a function whose other parameters and/or return value have types that depend on a
. Consider the following snippet in a language I am designing:
(* 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
If we make two (admittedly, unwarranted) assumptions:
- No dependencies must exist that cannot be inferred from explicitly provided information.
- Every free variable must be converted into an implicit argument of the last identifier introduced using
def
orexs
.
We can interpret the above snippet as being equivalent to the following one:
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
Which is more or less the same as the following Agda snippet:
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)
Clearly, two unwarranted assumptions have saved us a lot of typing!
Note: Of course, this mechanism only works as long as the original assumptions hold. For example, we cannot correctly infer the implicit arguments of the dependent function composition operator:
(* Only infers (?2 -> ?3) -> (?1 -> ?2) -> (?1 -> ?3) *)
def `.` g f x := g (f x)
In this case, we have to explicitly provide some additional information:
(* 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)
Which can be expanded into the following:
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)
Here is the equivalent Agda definition, for comparison:
_∘_ : ∀ {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)
End of Note
Is the mechanism described above feasible? Even better, is there any language that implements something resembling this mechanism?
Solución