[Agda] Compile-time parsing

[Conor McBride]

On 16 Dec 2011, at 11:01, Bengt Nordstrom wrote:

> I look at a metavariable as a part of an expression which is not
> filled in yet. So an expression with
> a metavariable is not erroneous, it is just not yet complete. It would
> be erroneous if it is impossible
> to fill it in.

I don't think metavariables, in general, should be considered
erroneous. Nor do I quite understand why metavariables (which,
after all, inhibit computation) should be quite so problematic
in typechecking. Perhaps they cause the creation of large
neutral terms, especially with eta-expansion. Metavariables
which do get solved, but late in the process, will create
expensive substitutions, of course.

A metavariable of a canonical type with no canonical constructors
is, in a consistent context, impossible to fill in. One might
argue that problems involving such variables are irredeemable.
Of course, if the context is inconsistent, then the metavariable
can be filled, but then again, if the context is inconsistent it
should be possible to arrange not to need the metavariable in
the first place, by an absurd pattern or some other "left rule".

If it is, in practice, necessary to construct expressions in
empty types, perhaps we could have a clear syntax indicating that
an expression is being constructed specifically for the purpose
of refutation. That might clarify the contexts in which such
irredeemable metavariables should or should not be considered
erroneous.

All the best

Conor

PS In the presence of equality on sets, where coercion between
provably equal sets is definable, it is possible to replace very
many type errors by irredeemable metavariables, turning brown to
yellow.

>
> Or do you have some special interpretation of the word "erroneous"?
>
> Best regards,
> Bengt
>
> On Fri, Dec 16, 2011 at 11:13 AM, Conor McBride
> <conor at strictlypositive.org> wrote:
>>
>> On 16 Dec 2011, at 10:03, Nils Anders Danielsson wrote:
>>
>>> On 2011-12-15 12:35, Andres Löh wrote:
>>>>
>>>> I don't understand completely why you're opposed to your first
>>>> solution. Code being highlighted in yellow *is* a (particular  
>>>> kind of)
>>>> type error in Agda. In fact, it's a particularly well-behaved  
>>>> kind of
>>>> type error from which the type checker can recover and still  
>>>> check the
>>>> rest of the program. There's no implication that yellow means  
>>>> "almost
>>>> correct" ...
>>>
>>>
>>> At the last AIM Nicolas Pouillard suggested that unsolved meta- 
>>> variables
>>> should (by default) be treated as errors. I think his main  
>>> motivation
>>> was that type-checking can be very slow if you have an unsolved
>>> meta-variable at the top of a long file. What do you think of this?
>>>
>>> (I'm not sure how easy this would be to implement, given that
>>> meta-variables related to goals should not be treated as errors.)
>>
>>
>> How about treating as an error an unsolved meta whose type, were it  
>> an
>> hypothesis, would be dismissed by an absurd pattern?
>>
>> Conor_______________________________________________
>>
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda