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

[Lennart Augustsson]

For me the main reason was (when doing Cayenne, which had very similar
rules) that I liked being explicit when defining things.  You only
define things in one place, and give the full story.  And then when
you use it, you can take advantage of the implicit arguments.

I think it's largely a matter of taste, and no deep fundamental reasons.

  -- Lennart

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).
>
>> ⑵ 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>