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

[Darin Morrison]

On Sun, Mar 29, 2009 at 8:04 PM, Stefan Monnier
<monnier at iro.umontreal.ca> wrote:
>> 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).

I dislike both of these "solutions".  I find it ugly to see ' all over
the place and also find having to use capital letters is too
restrictive, syntactically.  For example, the latter doesn't mesh well
at all with unicode because there isn't always a clear notion of
whether a symbol has a capital analogue.  Using capitals also prevents
one from being able to quantify over something which should be
interpreted as a mixfix operator (i.e., _◆_), which turns out to be
surprisingly convenient in Agda.

>> ⑵ 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".

You can already do this in Agda.  Most of the time it is ugly and
inconvenient though (not to mention hard to read) if you have a lot of
implicit variables.

>  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).

Hrmm.  I could imagine this seeming a bit too mysterious and perhaps
leading to strange typing issues elsewhere, but maybe I'm wrong.

> - Twelf uses the %name annotation to help Twelf choose a name for
>  a variable from its type.

You can achieve something which is sort of similar by giving a name
for an argument in the data constructor (i.e., introducing a trivial
dependency), although this name will be specific to that constructor
and not necessarily the type.  (Coq also does this AFAIK).  I think it
is a bit more flexible than using %name for everything.

> - 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.

Others may have a different experience, but I find that it's pretty
rare that I need to explicitly pass implicit arguments.  Perhaps I
have just developed an intuition about when Agda will be able to infer
the argument and I tend not to write code where this wouldn't work, or
maybe something else is going on.  In any case, I think it may be the
case that there are ways to write the kind of code that you want in a
slightly different way to where this issue doesn't occur as often.

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

But how will you be able to pass arguments "positionally" in this
case?  You will need to know which order Agda has shown, which is no
longer apparent on a purely syntactic basis.

>> 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.

Just because Twelf does it that way doesn't mean that it's the best
way or even that Agda should do it that way ;)

Just my 0.02...

(Personally, I would like to see some improvements in how implicit
arguments are handled but I'm not convinced that the Twelf way is
better).

-- 
Darin