Generalization [Re: [Agda] Location of implicit argument(s)]

[Andreas Abel]

On Nov 20, 2009, at 1:03 PM, Dan Licata wrote:

> In Twelf, you can specify implicit arguments by giving a type
> annotation; e.g. you could write
> foo (x : Zomg) bar y for foo_bar_ {Zomg} x y
> (except Twelf doesn't have mixfix to begin with).
>
> I often find myself wishing for this in Agda; e.g. when I have
>
> Lam : forall {G A B} -> Term (A :: G) B -> Term G (A imp B)
>
> I want to write
>
> f (Lam (e : Term (A :: G) B)) = ...
>
> for
>
> f (Lam{G}{A}{B} e) = ...
>
> The reason is that the former saves me from having to remember what
> order the implicit arguments come in (when there's a lot of them, I  
> have
> to keep flipping back to the definition of the datatype).
>
> Could such a syntax be made to work for Agda?

Seconded!


On Nov 20, 2009, at 4:04 PM, Nils Anders Danielsson wrote:
> This function does not work in patterns. Dan seems to want to /bind/
> variables using type annotations. For injective type constructors I
> suppose this could be made to work, although at first sight it seems
> counter-intuitive to treat a type signature as a binding construct.


Well, is the generalization mechanism in Twelf.  You have a distinct  
syntactic class of free variables (capitals in Twelf), could be  
something like ^bla in Agda.  The type reconstruction finds them and  
reconstructs their types and quantifies over them at the very outside  
(as implicit parameters).  Just like the free type variables in a  
Haskell signature.  The order of quantification is unspecified, so you  
cannot pass them by order, only by name, or you can supply them via  
type annotations.  This automatic generalization is very convenient;  
if you formalize an inductive judgement in Agda or Coq you may need a  
long boring list of quantifications for every rule.  However, it is  
not completely trivial to implement, and the type reconstruction  
algorithm has to invent names for the variables which were not  
mentioned at all.

For instance, the constructor declaration

     ofForall : forall {n a u κ} -> forall {Γ : KiCxt n} ->
             Γ ⊢ u ∈ κ ->
             Γ , ≤ u ∈ κ ⊢ a ∈ * ->
             Γ ⊢ ∀≤ u ∈ κ , a ∈ *

would be simpler

   ofForall:
             ^Γ ⊢ ^u ∈ ^κ ->
             Γ , ≤ u ∈ κ ⊢ ^a ∈ * ->
             Γ ⊢ ∀≤ u ∈ κ , a ∈ *

where Γ, u, κ, a should be bound outside, and the name n which  
appears in the dependent type of Γ has to be invented.

I find the ^ crucial here, to tell which identifiers to bind.


--
Andreas ABEL
INRIA, Projet Pi.R2
23, avenue d'Italie
F-75013 Paris
Tel: +33.1.39.63.59.41