[Agda] idiom brackets in 2.6.1

[Liang-Ting Chen]

Hi,

This syntactic sugar was first introduced to Haskell by Conor McBride

https://personal.cis.strath.ac.uk/conor.mcbride/pub/she/idiom.html

to extend the idiom bracket notation proposed by the paper “Applicative
Programming with Effects”

https://www.cambridge.org/core/journals/journal-of-functional-programming/article/applicative-programming-with-effects/C80616ACD5687ABDC86D2B341E83D298

to support applicative functors with a “choice” operation. It is also
called “MonadPlus” if the structure considered is indeed a monad.

For example, functions `catchTC` and `typeError` (modulo error messages)
form a Monad Plus on top of the TC monad in the Agda’s reflection
framework.

Hope this helps.

Best wishes,
Liang-Ting

On Wed, 18 Mar 2020 at 22:04, James Wood <james.wood.100 at strath.ac.uk>
wrote:

> Hi Sergei,
>
> I haven't used them myself, but the documentation for idiom brackets is
> here:
> https://agda.readthedocs.io/en/v2.6.1/language/syntactic-sugar.html#idiom-brackets
> . They're probably more useful in programming than proving.
>
> Regards,
> James
>
> On 18 March 2020 13:32:17 GMT, mechvel at scico.botik.ru wrote:
>>
>> 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
>> ------------------------------
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7Cdb12e08efccb4780914108d7cb40cb7e%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637201351459161057&sdata=vIvmJRfEwm2lwLRRKmRi%2BmEngLqzqRWEjpy2g81j5vc%3D&reserved=0
>>
>>
>>
> --
> Sent from my Android device with K-9 Mail. Please excuse my brevity.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-- 
— LT
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200319/8d9e4a8e/attachment.html>