[Agda] idiom brackets in 2.6.1

mechvel at scico.botik.ru mechvel at scico.botik.ru
Wed Mar 18 14:32:17 CET 2020


Can anybody, please, explain what does it mean the following?

"
  Idiom brackets can accommodate none or multiple applications separated 
by a vertical bar `|`
   if there are two additional operations
   ```agda
   empty : ∀ {A} → F A
   _<|>_ : ∀ {A} → F A → F A → F A
   ```
   i.e. an Alternative type class in Haskell.
".

Please, give an example.
What is an Alternative type class in Haskell ?  In Agda ?

Is it like this:

   f :: (Foo1 a) -> a -> a

        | (Foo2 a) -> a -> (a, a)

- to declare  f  having two signatures?

Thanks,

------
Sergei




More information about the Agda mailing list