Re: [isabelle-dev] Monad_Syntax
On 09/11/2013 05:04 PM, Makarius wrote: On Tue, 20 Aug 2013, Christian Sternagel wrote: any opinions on making the type of monadic bind more general (see the attached patch)? This thread seems to be still open. I now pushed the rebased change as eeff8139b3d8. Do monadic people have a standard Unicode point to render that operator? I would expect that most monadic people don't care very much about Unicode and are happy with latex and ascii... Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Monad_Syntax
On Wed, 11 Sep 2013, Florian Haftmann wrote:
Do monadic people have a standard Unicode point to render that operator?
If yes, we could assign that to \ and use it from STIX (or provide
a glyph in the IsabelleText font).
For LaTeX I once have been using
\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
following a suggestion by Jasmin as far as I remember.
We have the latex macro already since Isabelle/a33ecf47f0a0 (haftmann
2010).
If we find some Unicode point for it, we could reduce the variance of
notation to 2 or even 1. Allocating Unicode slots is a sport of many
subcultures, e.g. people writing text in Klingon (they did not make it
into the official charts, yet).
Looking around in Deja Vu or STIX for a few minutes, I did not find
anything like \ yet, but it might be still there hidden within
thousands of symbols.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Monad_Syntax
>> any opinions on making the type of monadic bind more general (see the
>> attached patch)?
No objections on my behalf.
>> "cp >>= f"
>
> Just a marginal question about concrete syntax: I see here various
> alternative notations:
>
> notation (output)
> bind_do (infixr ">>=" 54)
>
> notation (xsymbols output)
> bind_do (infixr "\=" 54)
>
> notation (latex output)
> bind_do (infixr "\" 54)
>
> Do monadic people have a standard Unicode point to render that operator?
> If yes, we could assign that to \ and use it from STIX (or provide
> a glyph in the IsabelleText font).
Good question. For LaTeX I once have been using
\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
following a suggestion by Jasmin as far as I remember.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Monad_Syntax
On Tue, 20 Aug 2013, Christian Sternagel wrote: any opinions on making the type of monadic bind more general (see the attached patch)? This thread seems to be still open. Looking at http://isabelle.in.tum.de/repos/isabelle/log/73d4c76d8eb2/src/HOL/Library/Monad_Syntax.thy, Florian Haftmann and Alex Krauss are the main authors and maintainers of this theory. "cp >>= f" Just a marginal question about concrete syntax: I see here various alternative notations: notation (output) bind_do (infixr ">>=" 54) notation (xsymbols output) bind_do (infixr "\=" 54) notation (latex output) bind_do (infixr "\" 54) Do monadic people have a standard Unicode point to render that operator? If yes, we could assign that to \ and use it from STIX (or provide a glyph in the IsabelleText font). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Monad_Syntax
Hi Chris, any opinions on making the type of monadic bind more general (see the attached patch)? Generalizing bind itself would rather be a topic for ICFP or POPL, and I cannot comment on that :-) Concerning the constant that represents it syntactically, I would say that if it does not break anything then it is fine. After all, this is just ad-hoc overloading, so generalizations can also be ad-hoc. I tested the change against IsaFoR (which makes heavy use of Monad_Syntax). Unfortunately, running JinjaThreads (which also uses Monad_Syntax) timed out on my machine (hopefully not due to the patch). Could anybody with access to a more powerful machine check this please? Pushed to testboard, which should run it on decent hardware: http://isabelle.in.tum.de/testboard/Isabelle/rev/eeff8139b3d8 Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
