<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
Hey Florian.<br>
<br>
Just my two cents, but does uncurrying buy you anything here?<br>
<br>
The function doing the actual work, "do_foo" in your example, has
not been given a name and type before. So you're free to have it
accept a tuple:<br>
<br>
fun do_foo (x_1, x_2, ... x_n) = ...<br>
<br>
And now val foo_cmd = read_foo_spec #> do_foo<br>
<br>
It's possibly a slight nuisance to someone wanting to wrap some
parameter adjustment around do_foo, although that was probably
fiddly anyway.<br>
<br>
Yours,<br>
Thomas.<br>
<br>
<br>
On 28/04/13 00:31, Florian Haftmann wrote:
<blockquote cite="mid:517BE139.7050200@informatik.tu-muenchen.de"
type="cite">
<pre wrap="">Hi all,
when Isabelle packages (in the widest sense) provide an interface to the
user, the following pattern is common practice:
</pre>
<blockquote type="cite">
<pre wrap="">fun gen_foo prep_1 … prep_n raw_x_1 … raw_x_n ctxt =
let
val x_1 = prep_1 ctxt raw_x_1;
…
val x_n = prep_n ctxt raw_x_n;
in
ctxt
|> …
end;
val foo = gen_foo cert_1 … cert_n;
val foo_cmd = gen_foo read_1 … read_n;
</pre>
</blockquote>
<pre wrap="">
Here, raw_x_1 … raw_x_n are unchecked arguments to the abstract
interface foo; these must be checked if provided from outside (via
cert_1 … cert_n) or parse if fed from Isar source text (via read_1 …
read_n).
This pattern tends to obfuscate if foo again is parametrized, see e.g.
<a class="moz-txt-link-freetext" href="http://isabelle.in.tum.de/repos/isabelle/file/182454c06a80/src/Pure/Isar/expression.ML#l848">http://isabelle.in.tum.de/repos/isabelle/file/182454c06a80/src/Pure/Isar/expression.ML#l848</a>
ff.
I'm asking myself whether we could spend some combinators for that
problem (cf. attached file). The idea is that two separate functions
fun cert_foo_spec ctxt raw_x_1 … raw_x_n = …
fun read_foo_spec ctxt raw_x_1 … raw_x_n = …
certify resp. parse their input arguments and provide the result as a
tuple. This would be connected to the process function proper using e.g.
val foo = cert_foo_spec #~~~> do_foo
val foo_cmd = read_foo_spec #~~~> do_foo
The drawback is that the signatures of the combinators contain numerous
type variables, and for each arity a separate combinator is needed
(which, I guess, you cannot escape when you perform uncurrying of
arbitrary-sized tuples). Maybe it is worth some thought nevertheless.
Florian
</pre>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a></pre>
</blockquote>
<br>
</body>
</html>