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

[Nils Anders Danielsson]

On 2009-03-29 20:04, Stefan Monnier 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?

Partly.

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

Yes, annotating bound variables would be a solution to this issue.

>> ⑵ What should the inferred implicit arguments be called?

>   The main point here, is that this is only a problem of convenience,

Not quite. You could for instance define the order of the inferred
arguments explicitly. However, I want the resulting code to be easy to
read, even if I unexpectedly need to give the 8th implicit argument to
some function explicitly.

With Agda's current approach we lose some convenience when giving type
signatures, and gain some readability later.

> As mentioned, Twelf has been doing this for years

Does the Twelf approach ever give rise to any surprises? Do people stay
away from certain kinds of definitions because they would be hard to
interpret? (This is not necessarily a bad thing: Giving people the
ability to shoot themselves in the foot can be useful, if you get
something else in return.)

I think the main problem with the current handling of implicit arguments
is that some definitions become hard to read. When defining an inductive
family I find it nice if every constructor can be laid out on one line,
so that it is easy to get an overview of the type, but the implicit
arguments often make the lines overly long. However, instead of changing
the language I have considered changing the user interface: one could
(optionally) suppress the display of implicit arguments. This would not
make it easier to write type signatures, but it would make it easier to
read them, and that is more important to me.

-- 
/NAD



This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.