Docs: add syntax trick to use Unicode instead of Haskell-compatible ASCII identifiers

[omelkonian]

Although users should generally use Haskell-compile identifiers for the definitions they compile with agda2hs, one could use syntax or pattern declarations in Agda to emulate Unicode mixfix definitions that are translated away at the time we compile the internal syntax where all this has been de-sugared.

As an example, we can use an infix notations for vectors:

open import Haskell.Prelude hiding ([]; _∷_)

data Vec (a : Set) : (@0 n : Nat) → Set where
  Nil : Vec a 0
  Cons : {@0 n : Nat} → a → Vec a n → Vec a (suc n)
{-# COMPILE AGDA2HS Vec #-}

pattern [] = Nil
pattern _∷_ x xs = Cons x xs

mapV : {a b : Set} {@0 n : Nat} (f : a → b) → Vec a n → Vec b n

syntax mapV f xs = f ⟨$⟩ xs

mapV f [] = []
mapV f (x ∷ xs) = f x ∷ (f ⟨$⟩ xs)
{-# COMPILE AGDA2HS mapV #-}

incV : {@0 n : Nat} → Vec Nat n → Vec Nat n
incV xs = (1 +_) ⟨$⟩ xs
{-# COMPILE AGDA2HS incV #-}

tailV : {a : Set} {@0 n : Nat} → Vec a (suc n) → Vec a n
tailV (x ∷ xs) = xs
{-# COMPILE AGDA2HS tailV #-}

that still compiles to the expected Haskell:

import Numeric.Natural (Natural)

data Vec a = Nil
           | Cons a (Vec a)

mapV :: (a -> b) -> Vec a -> Vec b
mapV f Nil = Nil
mapV f (Cons x xs) = Cons (f x) (mapV f xs)

incV :: Vec Natural -> Vec Natural
incV xs = mapV (1 +) xs

tailV :: Vec a -> Vec a
tailV (Cons x xs) = xs

(Credits to Ramsay Taylor of IOG for the idea)

[flupe]

That's also what we used in agda-core!

https://github.com/jespercockx/agda-core/blob/2229d9ec6b78448b93b492b681a38a62f6efe121/src/Agda/Core/Typing.agda#L69