[Agda] Overloading atoms and operators

[Gabriel Scherer]

One (indeed rare) example of mathematical practice would be the
"congruence modulo" relation, wrriten "a ≡ b (mod 3)", which would
correspond to an operator "_≡_(mod_)". In computer science, full words
are something used as part of judgment syntax: (_ ⊢ _ Type), (_ ⊢ _
true).

Are λ, μ, ν, etc. valid atoms? One could think of someone doing
analysis in Agda, expecting to name a specific real constant λ, and on
the other hand a computer scientist using (λ _ . _) as binding syntax.

On Fri, Jul 24, 2015 at 11:15 AM, Andreas Abel <abela at chalmers.se> wrote:
> I see why there is a need to overload operators of ,different arity by the
> same name, for instance, unary and binary minus.
>
> postulate
>   ℤ : Set
>   -_ : ℤ → ℤ
>   _-_ : (x y : ℤ) → ℤ
>
> infix 10 -_
> infixl 5 _-_
>
> test : ℤ → ℤ
> test x = - x - x
>
> But what is the point of overloading and atom with an operator of the same
> name?  This is, as far as I know, not mathematical practice, and would only
> serve obfuscation.
>
> postulate
>   A B : Set
>   x a : A
>   _x_ : A → A → B
>
> infix 10 _x_
>
> There seems no way of making Agda parse
>
>   a x a
>
> thus, the operator is unusable.
>
> In the light of issue 1616, it seems sensible to rule out such overloading.
>
> An atom should be in name conflict with any operator containing this atom as
> a name part.
>
> Cheers,
> Andreas
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda