<div><div dir="auto">Hi, </div></div><div dir="auto"><br></div><div dir="auto">This syntactic sugar was first introduced to Haskell by Conor McBride</div><div dir="auto"><br></div><div dir="auto"><div><a href="https://personal.cis.strath.ac.uk/conor.mcbride/pub/she/idiom.html">https://personal.cis.strath.ac.uk/conor.mcbride/pub/she/idiom.html</a></div><br></div><div><div dir="auto">to extend the idiom bracket notation proposed by the paper “Applicative Programming with Effects”</div><div dir="auto"><br></div><div dir="auto"><div><a href="https://www.cambridge.org/core/journals/journal-of-functional-programming/article/applicative-programming-with-effects/C80616ACD5687ABDC86D2B341E83D298">https://www.cambridge.org/core/journals/journal-of-functional-programming/article/applicative-programming-with-effects/C80616ACD5687ABDC86D2B341E83D298</a></div><br></div><div dir="auto">to support applicative functors with a “choice” operation. It is also called “MonadPlus” if the structure considered is indeed a monad.</div><div dir="auto"><br></div><div dir="auto">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. </div><div dir="auto"><br></div><div dir="auto">Hope this helps.</div><div dir="auto"><br></div><div dir="auto">Best wishes,</div><div dir="auto">Liang-Ting</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, 18 Mar 2020 at 22:04, James Wood <<a href="mailto:james.wood.100@strath.ac.uk">james.wood.100@strath.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div>Hi Sergei,<br><br>I haven't used them myself, but the documentation for idiom brackets is here: <a href="https://agda.readthedocs.io/en/v2.6.1/language/syntactic-sugar.html#idiom-brackets" target="_blank">https://agda.readthedocs.io/en/v2.6.1/language/syntactic-sugar.html#idiom-brackets</a> . They're probably more useful in programming than proving.<br><br>Regards,<br>James<br><br><div class="gmail_quote">On 18 March 2020 13:32:17 GMT, <a href="mailto:mechvel@scico.botik.ru" target="_blank">mechvel@scico.botik.ru</a> wrote:<blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<pre>Can anybody, please, explain what does it mean the following?<br><br>"<br> Idiom brackets can accommodate none or multiple applications separated <br>by a vertical bar `|`<br> if there are two additional operations<br> ```agda<br> empty : ∀ {A} → F A<br> _<|>_ : ∀ {A} → F A → F A → F A<br> ```<br> i.e. an Alternative type class in Haskell.<br>".<br><br>Please, give an example.<br>What is an Alternative type class in Haskell ? In Agda ?<br><br>Is it like this:<br><br> f :: (Foo1 a) -> a -> a<br><br> | (Foo2 a) -> a -> (a, a)<br><br>- to declare f having two signatures?<br><br>Thanks,<hr>Sergei<hr>Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br><a href="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" target="_blank">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</a></pre></blockquote></div></div><div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><pre><br></pre></blockquote></div><br>-- <br>Sent from my Android device with K-9 Mail. Please excuse my brevity.</div>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div></div>-- <br><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature">— LT</div>