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

[Andreas Abel]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Darin Morrison wrote:
> 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.

I agree, these solutions are not pretty.  My suggestion is to prefix an
identifier to be bound with a special symbol, as the historic "^" from
which the lambda was derived.

  append : Vect ^A ^n -> Vect A ^m -> Vect A (n + m)

This indicates that A, n, m should be generalized.  Elaboration is just:

  append : forall {A n m} -> Vect A n -> Vect A m -> Vect A (n + m)

However, the user should not be able to rely on a particular order,
another possible elaboration is

  append : forall {n m A} -> Vect A n -> Vect A m -> Vect A (n + m)

Thus, implicit arguments can only be passed by name, e.g.,

  append {A = Bool} v w

Something like

  lemma : length (append ^v ^w) == length (append w v)

can be elaborated using Hindley-Milner-inference techniques to

  lemma : forall {bla1 bla2 bla3} ->
                 {v : Vect bla1 bla2}{w : Vect bla1 bla3} ->
                 length (append ^v ^w) == length (append w v)

bla1, bla2, bla3 are system-generated names, and consequently, the
corresponding implicit arguments cannot be passed explicitely.

   lemma {bla1 = Bool} ...

is illegal.

As far as Twelf type annotation facility is concerned:

  lemma : length (append (^v : Vect ^A ^n) v) == n + n

can be stated as

  lemma : {v : Vect ^A ^n} -> length (append v v) == n + n

which is not horribly more verbose, so I think that does not have to be
incorporated.

Andreas

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


- --
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFJ0jbfPMHaDxpUpLMRAij0AJ0T+hV34LahuuuInd36RqoGqdr6igCg1Gk5
Y7sI7lqq6nSrNUtevbBZ2/A=
=cedh
-----END PGP SIGNATURE-----