Unicode double brace is not preserved by C-c C-SPC

[UlfNorell]

From guillaum...@gmail.com on October 23, 2012 22:59:19

If you enter a term using C-c C-SPC containing Unicode double braces (instance arguments), the Unicode characters ⦃ and ⦄ are translated to {{ and }}.

For λ and → the opposite happens, if you enter \x -> x it gets converted to λ x → x.

I’m not sure why Agda is pretty printing from the concrete syntax instead of keeping verbatim the input string, but it should at least be consistent and always output Unicode characters when possible.

Original issue: http://code.google.com/p/agda/issues/detail?id=733

[UlfNorell]

From andreas....@gmail.com on October 23, 2012 15:57:52

I'd favor to keep the user input. Anything speaking against it?

Status: Accepted
Labels: Type-Enhancement Emacs Interaction

[UlfNorell]

From nils.anders.danielsson on October 24, 2012 01:45:32

If you enter a term using C-c C-SPC containing Unicode double braces (instance arguments), the Unicode characters ⦃ and ⦄ are translated to {{ and }}.

No, they aren't. Perhaps you were using refine? In the case of give the text that you wrote is inserted verbatim, possibly with surrounding parentheses. In the case of refine Agda (sometimes) manipulates what you wrote, and a "pretty"-printed variant of it is inserted.

Internally we don't keep track of exactly what token was used, how much whitespace the text contained, which implicit arguments were given explicitly, etc., and changing Agda to keep track of all these things seems like lots of (boring) work. However, it would be very easy to switch from {{ to ⦃.

Andreas, what do you think?

[UlfNorell]

From andreas....@gmail.com on October 24, 2012 05:00:07

Mmh, I rather would not switch. A bit inconsequently, my defaults are \lambda, \to (unicode for \, ->) but {{ instead of unicode double braces. I am not even sure the (redundant) introduction of unicode substitutes for the double braces was such a good idea...

The Prelude uses ascii double braces.

Maybe Dominique has an opinion!?

Status: InfoNeeded
Cc: dominique.devriese@gmail.com

[UlfNorell]

From dominique.devriese@gmail.com on October 24, 2012 05:18:59

I personally am indifferent about the changes from/to unicode using refine.

About the introduction of the unicode double braces: I did this because I found they looked slightly nicer than the ascii ones. They are indeed redundant, but so are -> and \lambda. Can you say what you do not like about them?

[UlfNorell]

From andreas....@gmail.com on October 24, 2012 05:50:13

Well, I think {{ }} is syntactically closer to { } than the unicode symbols. Also, whenever we reserve new symbols we take them away from the user for his own definitions. So, we want to keep the reserved symbols minimal. AFAIAC, we would not have needed -> and \lambda, but now I am used to it.

[UlfNorell]

From dominique.devriese@gmail.com on October 24, 2012 06:00:55

I personally like -> and \lambda and use them most of the time. I think they give the code a nicer feel and are actually more natural than the ascii ones. From a (perhaps overly) principled point of view, the only reasons to fake them with ascii symbols are (I guess) conventionality and support for editors/tools that have trouble with unicode. Not that I would argue to remove the ascii symbols though.

[UlfNorell]

From guillaum...@gmail.com on October 24, 2012 06:05:55

In the case of give the text that you wrote is inserted verbatim, possibly with surrounding parentheses.

No it doesn’t. Write the following

foo : Set1 foo = ?

Then with the cursor in the goal do

M-x agda2-give RET Set -> Set RET

You get an unicode arrow (and similarly for lambda).

I also prefer unicode symbols, I think they are nicer that the ASCII symbols (including for the double brace).

[UlfNorell]

From stevan.a...@gmail.com on October 24, 2012 06:33:13

In the case of give the text that you wrote is inserted verbatim, possibly with surrounding parentheses.

I find the insertion of extra parentheses annoying, is there a good reason for not trusting the user when it comes to parentheses?

[UlfNorell]

From guillaum...@gmail.com on October 24, 2012 06:40:11

I find the insertion of extra parentheses annoying, is there a good reason for not trusting the user when it comes to parentheses?

I find it rather helpful usually. Say your term is ? × 5 and you give Agda the term 1 + 1 I do want the output to be (1 + 1) × 5 instead of 1 + 1 × 5

There are some cases where the extra parentheses are unneeded, though.

[UlfNorell]

From stevan.a...@gmail.com on October 24, 2012 07:11:26

I find it rather helpful usually.

Well, I think it's up to YOU to insert the parentheses in this example, if indeed you do want the addition to have precedence over the multiplication.

Consider instead writing, say, primitive recursion for the W-type. If you do it interactively (using give and refine), you end up with:

rec : ∀ {S P}{X : Set} → (Σ[ s ∶ S ](P s → W S P × X) → X) → W S P → X rec φ (sup s k) = φ (s , (λ p → (k p) , (rec φ (k p))))

If Agda didn't insert parentheses then you would have ended up with:

rec : ∀ {S P}{X : Set} → (Σ[ s ∶ S ](P s → W S P × X) → X) → W S P → X rec φ (sup s k) = φ (s , λ p → k p , rec φ (k p))

Which is a lot nicer.

[UlfNorell]

From stevan.a...@gmail.com on October 24, 2012 07:25:45

However, I guess situations like:

C (sup x {! proj₁ ∘ f !}) ---> C (sup x (proj₁ ∘ f))

Where you do want the parentheses, are quite common...

[UlfNorell]

From guillaum...@gmail.com on October 24, 2012 07:28:10

Well, I think it's up to YOU to insert the parentheses in this example, if indeed you do want the addition to have precedence over the multiplication.

It seems natural to me to assume that in ? × 5, the whole content of whatever I put in the hole will be multiplied by 5 and not just the right half because I gave 1 + 1 and that multiplication happens to have precedence over addition.

On the other hand, if I fill the hole of ? + 5 with 1 × 1 I do not want the extra parentheses.

If the precedences of + and × have been declared, Agda already handle both cases as expected (just tested it). If the precedences of + and × are not declared, then Agda put extra parentheses in both cases, which is also what I would expect.

In your example, if Agda indeed insert too many parentheses and if you have declared your precedences correctly, I would rather call it a bug in the code that checks whether parentheses should be added.

[UlfNorell]

From nils.anders.danielsson on October 24, 2012 10:40:24

Then with the cursor in the goal do

M-x agda2-give RET Set -> Set RET

Oh, I wasn't aware of this. When I give things I usually write the text in the goal before invoking give.

[UlfNorell]

From nils.anders.danielsson on October 24, 2012 10:45:30

If the precedences of + and × are not declared [...]

In this case + and × get the same, default precedence.

In your example, if Agda indeed insert too many parentheses and if you have declared your precedences correctly, I would rather call it a bug in the code that checks whether parentheses should be added.

Yes. (Don't report such bugs in this ticket, create a new one.)

Let's get back to the main issue: should we print ⦃ or {{? I think we should be consistent. Currently we print λ and →, so I think we should print ⦃. An alternative is to remove ⦃ from the language, but this could be disruptive.