Email Gateway (Aug 19 2022 at 10:59): Email Gateway (Aug 19 2022 at 10:59):From: "C. Diekmann" <diekmann@in.tum.de>
Hi,
there seems to be a problem with curried and uncurried parameters, in
particular in Scala.
For example, in the collections framework, the function parameters are
normally omitted. rs_iteratei serves as example. It is defined as
follows:
rs_iteratei ≡ s_iteratei rm_iteratei
The type is
('a, unit) RBT.rbt => ('b => bool) => ('a => 'b => 'b) => 'b => 'b
Often, I just want to apply the first four parameters and just get the
result back. For example in the following definition
definition do_something :: "(nat, unit) RBT.rbt ⇒ nat" where
"do_something tree = rs_iteratei tree (%x. True) (%x y. x) (0::nat)"
This yields the following Scala code
def do_something(tree: RBT.rbt[Nat.nat, Unit]): Nat.nat =
RBTSetImpl.rs_iteratei[Nat.nat,
Nat.nat].apply(tree).apply((_: Nat.nat) =>
true).apply((x: Nat.nat) =>
(_: Nat.nat) => x).apply(Nat.Zero_nat())
As rs_iteratei is exported as curried function, the code looks really
ugly because of all those apply calls. The signature of rs_iteratei is
(RBT.rbt[A, Unit]) => (B => Boolean) => (A => B => B) => B => B
There are some problems with that. First, it looks scary. Second, it
creates those long class files during compilation. Third, applying
apply four times is way more inefficient than passing just four
parameters at once. And finally, IDEs might have problems with those
scary long function types.
The following code lemma adds the parameters to rs_iteratei
lemma[code]: "rs_iteratei t sfun mfun strt = s_iteratei rm_iteratei
t sfun mfun strt"
Now, in the exported Scala code, the signature looks as follows.
(t: RBT.rbt[A, Unit], sfun: B => Boolean, mfun: A => B => B, strt: B): B
This is very beautiful, provides a good documentation, and helps the
IDE to use the function. The do_something also looks better now.
def do_something(tree: RBT.rbt[Nat.nat, Unit]): Nat.nat =
RBTSetImpl.rs_iterateiNat.nat,
Nat.nat
I heard that one does not want the parameters explicitly listed in e.g. SML.
It would be a great feature if for certain languages, the function
parameters and a useful name for them could be added.
Regards
Cornelius
Last updated: Apr 19 2024 at 01:05 UTC