[Agda] Re: Why aren't free vars in types automatically generalized

[Stefan Monnier]

> I agree that it is often annoying to write out all the implicit
> arguments in a type signature.  There are several reasons not to
> introduce the short-hand notation you suggest, though:

Were these the original reason for omitting such a feature?

> ⑴ If something called l were to come into scope, then your program would
>  be broken.  Hopefully you would get a type error, but not in all cases.

Indeed, it's a problem.  In SML, this is solved by using a ' prefix in
front of the free variables.  In Twelf it is solved by requiring the
free vars to start with a capital letter (and it is also less
significant since Twelf programs seem to be (ironically) a lot more
"closed" (maybe I should say "self-contained") and rely a lot less on
libraries).

> ⑵ What should the inferred implicit arguments be called? In your case it
>  is obvious, but what if l depended on something else? Note that you
>  can give implicit arguments by name when applying a function, so the
>  names matter:

>    f {A = …} x

Indeed, some arguments would not even appear, so their naming might be
an issue.  I know of 3 ways to reduce this problem:
- You don't need to give the name of explicitly provided implicit
  arguments.  You can pass them "positionally".  Or you could even
  imagine that Agda would just try to use explicitly provided implicit
  args "where they work" (i.e. look at the type of the provided argument
  to try and guess to which formal arg this corresponds).
  The main point here, is that this is only a problem of convenience,
  since it is easy to provide to the user some alternative way to give
  the necessary info.
- Twelf uses the %name annotation to help Twelf choose a name for
  a variable from its type.
- Hopefully you need to pass those implict arguments explicitly less
  often.  Notice, that one of the reasons why I like Twelf/HM's
  treatment of freevars-as-implicit-args is specifically because it
  reduces the need to pass implicit args explicitly, as shown in my
  "teLit" example:

      teLit  : ∀{l Γ} → ℕ → TExp{l} Γ tNat
    =>
      teLit  : ℕ → TExp Γ tNat

  Notice how I get to drop the {l} arg to TExp.  I find this situation
  to be one of the common cases where I need to provide implicit
  arguments explicitly.

> ⑶ Similarly, if several independent arguments are added, in which order
>  should they appear in the type signature?

Any correct order will do.

> This description is very vague, and I would not be surprised if I had
> missed some design choice or potential problem.  Has anyone worked out
> the details?  Would the algorithm be obvious to users of the language?

As mentioned, Twelf has been doing this for years, and I can't think of
any reason why the differences in the underlying type theory would have
much impact on this aspect of type reconstrution.


        Stefan