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
[isabelle-dev] Monad_Syntax
Dear all,
any opinions on making the type of monadic bind more general (see the
attached patch)?
For my motivation see the farther below.
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?
Motivation:
I'm currently writing a small combinator parser library in Isabelle/HOL,
where (for reasons of totality) I have two types of parsers (both are
typedefs carved out from the function space "'a list => string + ('b *
'a list)":
- standard parsers (with the invariant that the remaining input after
parsing is not longer than before), and
- "consuming" parsers (with the invariant that the remaining input
after parsing is strictly shorter than before).
Then it is possible to have (recursive) combinators like (where types
are simplified for readability)
many :: "'a cparser => ('a list) parser"
where totality of "many p" relies on the fact that "p" consumes at least
one token. (Of course, it is trivial to turn a consuming parser into a
standard one.) Now for bind: let "p", "f" be standard and "cp" and "cf"
be consuming. Then suitable combinations that yield consuming parsers are:
cp >>= cf, p >>= cf, and cp >>= f
But until now the type of "Monad_Syntax.bind" was "'a => ('b => 'c) =>
'c" which does not allow the last combination (since the result of "f"
is not consuming, but "cp >>= f" is).
Concerning readability it would be neat if I could overload "bind" for
all these cases.
Any comments?
cheers
chris
# HG changeset patch
# User Christian Sternagel
# Date 1376987651 -32400
# Tue Aug 20 17:34:11 2013 +0900
# Node ID 4808a6ae009b22369d71658c64369574d6adea83
# Parent 7e89edba3db64dad93dadac77a9e64d45ffcfe49
more general typing of monadic bind
diff --git a/src/HOL/Library/Monad_Syntax.thy b/src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy
+++ b/src/HOL/Library/Monad_Syntax.thy
@@ -15,7 +15,7 @@
*}
consts
- bind :: "['a, 'b \ 'c] \ 'c" (infixr ">>=" 54)
+ bind :: "['a, 'b \ 'c] \ 'd" (infixr ">>=" 54)
notation (xsymbols)
bind (infixr "\=" 54)
@@ -24,7 +24,7 @@
bind (infixr "\" 54)
abbreviation (do_notation)
- bind_do :: "['a, 'b \ 'c] \ 'c"
+ bind_do :: "['a, 'b \ 'c] \ 'd"
where
"bind_do \ bind"
@@ -46,14 +46,14 @@
"_do_then" :: "'a \ do_bind" ("_" [14] 13)
"_do_final" :: "'a \ do_binds" ("_")
"_do_cons" :: "[do_bind, do_binds] \ do_binds" ("_;//_" [13, 12] 12)
- "_thenM" :: "['a, 'b] \ 'b" (infixr ">>" 54)
+ "_thenM" :: "['a, 'b] \ 'c" (infixr ">>" 54)
syntax (xsymbols)
"_do_bind" :: "[pttrn, 'a] \ do_bind" ("(_ \/ _)" 13)
- "_thenM" :: "['a, 'b] \ 'b" (infixr "\" 54)
+ "_thenM" :: "['a, 'b] \ 'c" (infixr "\" 54)
syntax (latex output)
- "_thenM" :: "['a, 'b] \ 'b" (infixr "\" 54)
+ "_thenM" :: "['a, 'b] \ 'c" (infixr "\" 54)
translations
"_do_block (_do_cons (_do_then t) (_do_final e))"
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
