| \documentclass[a4paper,titlepage,twoside,12pt]{article} |
| \usepackage{zed-cm} |
| \usepackage{graphicx} |
| \markboth{Draft}{Version 0.1} |
| \pagestyle{myheadings} |
| \begin{document} |
| \parskip 2 pt |
| \parindent 10 pt |
| |
| \title{Optional matters} |
| \author{Steve Powell} |
| \maketitle |
| % The following three commands ensure the title page is stamped as |
| % confidential without a page number. Page numbering is started at the |
| % table of contents. |
| \thispagestyle{myheadings} |
| \pagenumbering{roman} |
| \setcounter{page}{0} |
| |
| %============================================================================= |
| We define an optional generic type (analogous to say, $\seq$) for use in specifications where optional values are to be supplied. |
| |
| |
| %\clearpage |
| %\pagenumbering{roman} |
| %\tableofcontents |
| |
| % Type checking hacks |
| \newcommand{\true}{true} |
| \newcommand{\false}{false} |
| \renewcommand{\emptyset}{\varnothing} |
| \newcommand{\defaultsTo}{\mathbin{\sf defaultsTo}} |
| |
| %============================================================================= |
| \clearpage |
| \tableofcontents |
| |
| \clearpage |
| \pagenumbering{arabic} |
| |
| \section{Optionals} |
| We wanted to define a data type that was generic, something that Zed proper doesn't allow (and fuzz doesn't type-check for us): |
| |
| %%unchecked |
| \begin{zed} |
| Opt[X] ::= Nil | Just \ldata X \rdata |
| \end{zed} |
| This fails because data type definitions aren't allowed to be generic. |
| |
| Nor are they allowed to be parametric, as in Haskell: |
| %%unchecked |
| \begin{zed} |
| \mathtt{data} Opt ~ a = Nil | Just ~a |
| \end{zed} |
| so instead we define the following generic construction: |
| \begin{zed} |
| Opt[X]==(\lambda s : \power X @ \{0\} \pfun s) |
| \end{zed} |
| where we declare an optional $Opt ~ S$ as a \emph{partial} function from a singleton set (the zero isn't significant, but we had to choose something, so what do you do?) to the set $S$ ---this essentially picks out a single element from $S$, or it doesn't. Exactly what we want. |
| |
| [The reason we chose to use functions and not simply subsets is because that makes it simple to define the function $defaultsTo$ (see below).] |
| |
| \subsection{Type injections $Nil$ and $Just$} |
| In order to exploit this definition in the normal way, we introduce two mechanisms, corresponding to the injections $Nil$ and $Just$ of the Haskell mechanism. |
| \begin{zed} |
| Nil [X] == \emptyset [\{0\} \cross X] |
| \end{zed} |
| which denotes the $Nil$ (`not supplied') object in $Opt ~ X$ (yes, the empty set---but the generic types here are significant for type inference), and: |
| \begin{zed} |
| Just[X] == (\lambda x : X @ \{0 \mapsto x \}) |
| \end{zed} |
| which puts a value $x$ in the set $S$ into the $Opt ~ S$ type (where $S$ has elements of type $X$). |
| |
| \subsection{Type deconstructor $Take$} |
| We also define $Take$, which, given an optional which is $Just ~ x$, extracts the value behind it. |
| |
| \begin{zed} |
| Take[X] == (\lambda o : Opt ~X @ o ~ 0) |
| \end{zed} |
| Of course, $Take$ is not defined on $Nil$. |
| |
| \subsection{Using optionals with a default mechanism} |
| Given an optional part of the state, it would be nice to define a value that was this optional value, but defaults to something else if the optional value is not supplied (is $Nil$). This can be conveniently captured by an infix operator $\defaultsTo$: |
| %%inop \defaultsTo 3 |
| \begin{gendef}[X] |
| \_ \defaultsTo \_ : Opt ~ X \cross X \fun X |
| \where |
| \forall o : Opt ~ X; x : X @ \\ |
| \t1 o \defaultsTo x = Take(Just ~ x \oplus o) |
| \end{gendef} |
| which can be used as in this small example: |
| %%unchecked |
| \begin{schema}{State} |
| value : Opt \nat |
| \end{schema} |
| Query the state and ask for the value -- if it is not set in the state (it is optional after all), we want to get a default value zero: |
| %%unchecked |
| \begin{schema}{QueryValue} |
| \Xi State \\ |
| val! : \nat |
| \where |
| val! = value \defaultsTo 0 |
| \end{schema} |
| |
| This operator can be chained, so that, if $oVal_1$ and $oVal_2$ are optional values (of the same type $\num$, say), the expression: |
| %%unchecked |
| \begin{zed} |
| oVal_1 \defaultsTo oVal_2 \defaultsTo 42 |
| \end{zed} |
| denotes the value in $oVal_1$, unless this is not specified, when it is that in $oVal_2$, unless \emph{that} is not specified, in which case it is the value $42$. |
| |
| \section{How to use this in specifications} |
| In order to use this in a specification there are two options: one, to include the definitions of $Opt$ and the like each time we wish to use them, and two, to ensure that these terms (and types) are available for $f$UZZ when it checks the document that uses them. |
| |
| There are two ways to get $f$UZZ to have these definitions around beforehand, one is to extend the standard prelude (a file called \texttt{fuzzlib} contains the standard prelude and this can be manually extended) and the other is simply to supply this file to $f$UZZ before the file that makes use of it. |
| |
| One drawback with these solutions is that the LaTeX formatting is still needed for the symbol $\defaultsTo$ for example. This is obtained by the definition: |
| \begin{verbatim} |
| \newcommand{\defaultsTo}{\mathbin{\sf defaultsTo}} |
| \end{verbatim} |
| which ought to be put near the top of the file that uses this symbol. |
| |
| \paragraph{Example} |
| The file \texttt{TestOptional.tex} is checked with the technique that supplies both files to $f$UZZ. We execute the command: |
| \begin{verbatim} |
| fuzz Optional.tex TestOptional.tex |
| \end{verbatim} |
| and this test... |
| |
| ...works! |
| |
| \end{document} |