[Agda] Naive person's questions about agda vs. haskell symbol notation

[Miëtek Bak]

Agda supports section notation.  For example:

	data Nat : Set where
	  zero : Nat
	  suc  : Nat → Nat
	{-# BUILTIN NATURAL Nat #-} -- For the literals

	_+_ : Nat → Nat → Nat
	zero  + m = m
	suc n + m = suc (n + m)

	plus = _+_

	postinc = _+ 1

	preinc = 1 +_

In general, Agda supports mixfix operator notation.  For example:

	data Bool : Set where
	  true  : Bool
	  false : Bool

	if_then_else_ : {A : Set} → Bool → A → A → A
	if true  then x else y = x
	if false then x else y = y

	_<|_|>_ = if_then_else_

Agda’s new documentation website has a page on mixfix operators:
http://agda.readthedocs.io/en/latest/language/mixfix-operators.html

As far as I know, there is no equivalent to the backtick notation.  Instead, we default to declaring infix operators, and then we use the full name with the underscores whenever the prefix form is required.

Using the prefix form is required to bind implicit arguments.  For example:

	_<|_|>'_ : {A : Set} → Bool → A → A → A
	_<|_|>'_ {A} b x y = if_then_else_ {A} b x y

-- 
Mietek


> On 24 Dec 2017, at 13:46, Peter Hancock <hancock at fastmail.fm> wrote:
> 
> I have never properly learnt to use Agda's fancy notational features,
> except in a basic ad-hoc way, that accomplishes most of what I want.  I'm
> not referring to unicode symbols and whatnot, but the business of making
> symbols by scattering '_' characters in some line-noise.
> 
> I'd like some hints and tips about how to get the most out of this feature.
> RTFM with a pointer would be fine.
> 
> Away from the keyboard, I often use some haskell-like apparatus for dealing with infix
> symbols.  Namely:
> 
> * "section notation", as in (*), (*a), (a*), where * is binary infix.
>  Anything that avoids having to write a lambda-expression or think 
>  of a bound-variable name is great.
> * "backtick" notation, as in (a `foo` b), where foo is a name.  Something
>  that turns a short name into an infix symbol is great.
> * I very much like the notation  (a <| b |> c) for "if b, then a else c"
>  that allows three-place relations to masquerade as infix relations. 
> 
> How much of this can be supported or emulated with Agda's symbol-wizardry? 
> 
> Hank
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda