David, This is Todd, writing on behalf of Mark and Todd, because of logistical convenience, i.e., my nearness to his laptop. :)
> So, a bit deeper question, though, let's say I do have a method that
> really does only make sense with non-empty tuples? What is the
> correct or idiomatic way of getting from a possibly empty tuple to
> knowing we have one that isn't empty. Something along the lines of
>
> if thing is empty then [ handle the empty case ] else [ do the
> non-empty case ];
You want to use one of Avail's structured casting control structures. Let's
look at the two basic ones:
"Cast|cast_into_"
"Cast|cast_into_else_"
We will consider your case of an arbitrary tuple versus a non-empty tuple,
though the casting mechanism works for any type scenario.
Case 1: The programmer knows that `a` is non-empty after assignment, even
though this is not statically provable under the current regime of semantic
restrictions. If the programmer is wrong, then "Cast|cast_into_" raises a
bad-cast exception.
a : <any…|> := …;
Cast a into
[
t : <any…|1..>
|
/* The dynamic value of `a` is now bound to `t`. But `t` has a
* stronger static type, so operations that expect a non-empty
* tuple can now be used.
*/
…
];
/* If the cast fails, then the next line of program source is
unreachable,
* because a bad-cast exception is raised.
*/
Case 2: The programmer does not know that `a` is non-empty after assignment; it
might be, it might not. But the programmer wants to do something different in
each case. No exceptions are raised by "Cast|cast_into_else_" (unless they are
propagating through from one of the passed functions).
a : <any…|> := …;
Cast a into
[
t : <any…|1>
|
/* `a` = `t`, and `t` is non-empty, but `t` is more strongly
typed. */
]
else
[
/* `a` is empty (and `t` is not in scope). */
];
These control structures can also be used in value-producing contexts:
/* This isn't necessary anymore, because summation now allows empty
* tuples, but it illustrates the point.
*/
a : <integer…|> := …;
sum ::= cast a into [t : <integer…|1..> | ∑t] else [0];
There are several other variations of casting. For more information, see
/avail/Avail/Foundation/Casts
Todd [and Mark sitting nearby]
signature.asc
Description: Message signed with OpenPGP using GPGMail
