[Agda] Mixfix binders: first patch

[Andreas Abel]

Hi Nisse and Ulf,

thanks for the clarification.  I understand now that the syntax  
translation needs to go both ways, which is certainly different from  
what other syntax mechanisms (Coq, C prepoc.) have.  Under these  
circumstances, of course, variables need to be linear on both sides.

Then it is probably a good idea to stick to the current proposal.  
Sorry for the noise.

Cheers,
Andreas

On Sep 13, 2010, at 12:23 PM, Ulf Norell wrote:
>
> What you have to remember is that we're not defining new syntax
> for an arbitrary piece of expression, we're defining the syntax for a
> particular function symbol (what Nisse wrote above). It's not valid
> (nor does it make sense) to define mult2 x to be the syntax for
> plus x x. Having the new syntax on the left would lead you to believe
> that you could define several different pieces of syntax for the same
> symbol, which isn't the case. For instance,
>
> -- not valid:
> syntax plus x x = mult2 x
> syntax plus x y = x + y

On Sep 13, 2010, at 12:14 PM, Nils Anders Danielsson wrote:

> On 2010-09-13 10:39, Andreas Abel wrote:
>> The cut-away argument implies that the RHS (in the terminology  
>> above) is
>> not linear in the use of variables, e.g., you could have
>>
>> Notation "exists x : A, B" := sigT A (fun x:A => B)
>>
>> which would hint toward binding the variables in the new notation  
>> rather
>> than the old one.
>
> Two points:
>
> * How could the variables be bound in the new notation? You could have
>
>    syntax foo a b c = bar a b c
>
>  just as well as
>
>    syntax c a b bar = bar a b c.
>
>  The two right-hand sides here are identical, but the sets of bound
>  variables are not.
>
> * I don't expect to be allowed to write non-linear LHSs. What would  
> the
>  following declaration mean?
>
>    syntax foo a a = bar a
>
>  When pretty-printing "foo e₁ e₂", should Agda first check if  
> e₁ and e₂
>  are syntactically equal, and only in that case use the new syntax?
>
>> Unless we want to allow non-linear new notation like
>>
>> Notation "x : A =myFakeHetId= y : A" := _==_ {A} x y
>>
>> which I rather would not.
>
> Me neither.




Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/