[Agda] Overloading atoms and operators

[Andreas Abel]

Well, yes, in Agda any unicode sequence can be used as atom or operator. 
  You get the latter if you place underscores appropriately.  Like

   _⊢_Type

would be a mixfix operator.  There is no pre-given separation of names 
into operators and axioms.  While you would want to use μ as a scalar in 
linear algebra and as a type operator in type theory, it is probably a 
bad idea to have both in scope in the same file.

Cheers,
Andreas


On 24.07.2015 11:38, Gabriel Scherer wrote:
> 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

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