|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Overloading{\isadigit{0}}}% |
|
4 % |
|
5 \isamarkupsubsubsection{An initial example} |
|
6 % |
|
7 \begin{isamarkuptext}% |
|
8 We start with a concept that is required for type classes but already |
|
9 useful on its own: \emph{overloading}. Isabelle allows overloading: a |
|
10 constant may have multiple definitions at non-overlapping types. For example, |
|
11 if we want to introduce the notion of an \emph{inverse} at arbitrary types we |
|
12 give it a polymorphic type% |
|
13 \end{isamarkuptext}% |
|
14 \isacommand{consts}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}% |
|
15 \begin{isamarkuptext}% |
|
16 \noindent |
|
17 and provide different definitions at different instances:% |
|
18 \end{isamarkuptext}% |
|
19 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
|
20 inverse{\isacharunderscore}bool{\isacharcolon}\ {\isachardoublequote}inverse{\isacharparenleft}b{\isacharcolon}{\isacharcolon}bool{\isacharparenright}\ {\isasymequiv}\ {\isasymnot}\ b{\isachardoublequote}\isanewline |
|
21 inverse{\isacharunderscore}set{\isacharcolon}\ \ {\isachardoublequote}inverse{\isacharparenleft}A{\isacharcolon}{\isacharcolon}{\isacharprime}a\ set{\isacharparenright}\ {\isasymequiv}\ {\isacharminus}A{\isachardoublequote}\isanewline |
|
22 inverse{\isacharunderscore}pair{\isacharcolon}\ {\isachardoublequote}inverse{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}inverse{\isacharparenleft}fst\ p{\isacharparenright}{\isacharcomma}\ inverse{\isacharparenleft}snd\ p{\isacharparenright}{\isacharparenright}{\isachardoublequote}% |
|
23 \begin{isamarkuptext}% |
|
24 \noindent |
|
25 Isabelle will not complain because the three definitions do not overlap: no |
|
26 two of the three types \isa{bool}, \isa{{\isacharprime}a\ set} and \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} have a |
|
27 common instance. What is more, the recursion in \isa{inverse{\isacharunderscore}pair} is |
|
28 benign because the type of \isa{inverse} becomes smaller: on the left it is |
|
29 \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} but on the right \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and \isa{{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}. The \isa{{\isacharparenleft}overloaded{\isacharparenright}} tells Isabelle that the definitions do |
|
30 intentionally define \isa{inverse} only at instances of its declared type |
|
31 \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely supresses warnings to that effect. |
|
32 |
|
33 However, there is nothing to prevent the user from forming terms such as |
|
34 \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}}, |
|
35 although we never defined inverse on lists. We hasten to say that there is |
|
36 nothing wrong with such terms and theorems. But it would be nice if we could |
|
37 prevent their formation, simply because it is very likely that the user did |
|
38 not mean to write what he did. Thus he had better not waste his time pursuing |
|
39 it further. This requires the use of type classes.% |
|
40 \end{isamarkuptext}% |
|
41 \end{isabellebody}% |
|
42 %%% Local Variables: |
|
43 %%% mode: latex |
|
44 %%% TeX-master: "root" |
|
45 %%% End: |