= Solution
Use tagged <disjoint unions> for results that can contain either a value or an error message. This avoids ambiguity even if the item set itself contains the string `Empty queue`. The operation signatures are
$$
\boxed{\begin{aligned}
\operatorname{create}&:1\to Q,\\
\operatorname{head}&:Q\to I\sqcup M,\\
\operatorname{add}&:I\times Q\to Q,\\
\operatorname{delete}&:Q\to Q\sqcup M,\\
\operatorname{empty}&:Q\to B.
\end{aligned}}
$$
Here $1$ is a singleton, expressing that `create` takes no meaningful argument. Write successful results as $\operatorname{ok}_I(i)$ and $\operatorname{ok}_Q(q)$, and errors as $\operatorname{err}_I(e)$ and $\operatorname{err}_Q(e)$ for $e=\text{Empty queue}$. Returning an error is not returning a queue, so its result must not be silently passed to another queue operation.
Back to article page
