2 % |
2 % |
3 \isamarkupheader{Syntactic classes} |
3 \isamarkupheader{Syntactic classes} |
4 \isacommand{theory}~Product~=~Main:% |
4 \isacommand{theory}~Product~=~Main:% |
5 \begin{isamarkuptext}% |
5 \begin{isamarkuptext}% |
6 \medskip\noindent There is still a feature of Isabelle's type system |
6 \medskip\noindent There is still a feature of Isabelle's type system |
7 left that we have not yet used: when declaring polymorphic constants |
7 left that we have not yet discussed. When declaring polymorphic |
8 $c :: \sigma$, the type variables occurring in $\sigma$ may be |
8 constants $c :: \sigma$, the type variables occurring in $\sigma$ may |
9 constrained by type classes (or even general sorts) in an arbitrary |
9 be constrained by type classes (or even general sorts) in an |
10 way. Note that by default, in Isabelle/HOL the declaration $\TIMES |
10 arbitrary way. Note that by default, in Isabelle/HOL the declaration |
11 :: \alpha \To \alpha \To \alpha$ is actually an abbreviation for |
11 $\TIMES :: \alpha \To \alpha \To \alpha$ is actually an abbreviation |
12 $\TIMES :: (\alpha::term) \To \alpha \To \alpha$. Since class $term$ |
12 for $\TIMES :: (\alpha::term) \To \alpha \To \alpha$. Since class |
13 is the universal class of HOL, this is not really a restriction at |
13 $term$ is the universal class of HOL, this is not really a constraint |
14 all. |
14 at all. |
15 |
15 |
16 The $product$ class below provides a less degenerate example of |
16 The $product$ class below provides a less degenerate example of |
17 syntactic type classes.% |
17 syntactic type classes.% |
18 \end{isamarkuptext}% |
18 \end{isamarkuptext}% |
19 \isacommand{axclass}\isanewline |
19 \isacommand{axclass}\isanewline |
20 ~~product~<~{"}term{"}\isanewline |
20 ~~product~<~{"}term{"}\isanewline |
21 \isacommand{consts}\isanewline |
21 \isacommand{consts}\isanewline |
22 ~~product~::~{"}'a::product~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymotimes}{"}~70)% |
22 ~~product~::~{"}'a::product~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~70)% |
23 \begin{isamarkuptext}% |
23 \begin{isamarkuptext}% |
24 Here class $product$ is defined as subclass of $term$ without any |
24 Here class $product$ is defined as subclass of $term$ without any |
25 additional axioms. This effects in logical equivalence of $product$ |
25 additional axioms. This effects in logical equivalence of $product$ |
26 and $term$, as is reflected by the trivial introduction rule |
26 and $term$, as is reflected by the trivial introduction rule |
27 generated for this definition. |
27 generated for this definition. |
49 This is done for class $product$ and type $bool$ as follows.% |
49 This is done for class $product$ and type $bool$ as follows.% |
50 \end{isamarkuptext}% |
50 \end{isamarkuptext}% |
51 \isacommand{instance}~bool~::~product\isanewline |
51 \isacommand{instance}~bool~::~product\isanewline |
52 ~~\isacommand{by}~intro\_classes\isanewline |
52 ~~\isacommand{by}~intro\_classes\isanewline |
53 \isacommand{defs}\isanewline |
53 \isacommand{defs}\isanewline |
54 ~~product\_bool\_def:~{"}x~{\isasymotimes}~y~{\isasymequiv}~x~{\isasymand}~y{"}% |
54 ~~product\_bool\_def:~{"}x~{\isasymOtimes}~y~{\isasymequiv}~x~{\isasymand}~y{"}% |
55 \begin{isamarkuptext}% |
55 \begin{isamarkuptext}% |
56 The definition $prod_bool_def$ becomes syntactically well-formed only |
56 The definition $prod_bool_def$ becomes syntactically well-formed only |
57 after the arity $bool :: product$ is made known to the type checker. |
57 after the arity $bool :: product$ is made known to the type checker. |
58 |
58 |
59 \medskip It is very important to see that above $\DEFS$ are not |
59 \medskip It is very important to see that above $\DEFS$ are not |
63 these definitions, which is in contrast to programming languages like |
63 these definitions, which is in contrast to programming languages like |
64 Haskell \cite{haskell-report}. |
64 Haskell \cite{haskell-report}. |
65 |
65 |
66 \medskip While Isabelle type classes and those of Haskell are almost |
66 \medskip While Isabelle type classes and those of Haskell are almost |
67 the same as far as type-checking and type inference are concerned, |
67 the same as far as type-checking and type inference are concerned, |
68 there are major semantic differences. Haskell classes require their |
68 there are important semantic differences. Haskell classes require |
69 instances to \emph{provide operations} of certain \emph{names}. |
69 their instances to \emph{provide operations} of certain \emph{names}. |
70 Therefore, its \texttt{instance} has a \texttt{where} part that tells |
70 Therefore, its \texttt{instance} has a \texttt{where} part that tells |
71 the system what these ``member functions'' should be. |
71 the system what these ``member functions'' should be. |
72 |
72 |
73 This style of \texttt{instance} won't make much sense in Isabelle, |
73 This style of \texttt{instance} won't make much sense in Isabelle's |
74 because its meta-logic has no corresponding notion of ``providing |
74 meta-logic, because there is no internal notion of ``providing |
75 operations'' or ``names''.% |
75 operations'' or even ``names of functions''.% |
76 \end{isamarkuptext}% |
76 \end{isamarkuptext}% |
77 \isacommand{end}\end{isabelle}% |
77 \isacommand{end}\end{isabelle}% |