Hey Florian.

Just my two cents, but does uncurrying buy you anything here?

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:

fun do_foo (x_1, x_2, ... x_n) = ...

And now val foo_cmd = read_foo_spec #> do_foo

It's possibly a slight nuisance to someone wanting to wrap some parameter adjustment around do_foo, although that was probably fiddly anyway.


On 28/04/13 00:31, Florian Haftmann wrote:
Hi all,

when Isabelle packages (in the widest sense) provide an interface to the
user, the following pattern is common practice:

fun gen_foo prep_1 ... prep_n raw_x_1 ... raw_x_n ctxt =
     val x_1 = prep_1 ctxt raw_x_1;
     val x_n = prep_n ctxt raw_x_n;
     |>  ...

val foo = gen_foo cert_1 ... cert_n;
val foo_cmd = gen_foo read_1 ... read_n;
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 ...

This pattern tends to obfuscate if foo again is parametrized, see e.g.

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.


isabelle-dev mailing list

isabelle-dev mailing list

Reply via email to