8890
|
1 |
|
9146
|
2 |
header {* Syntactic classes *}
|
8890
|
3 |
|
9146
|
4 |
theory Product = Main:
|
8890
|
5 |
|
8903
|
6 |
text {*
|
|
7 |
\medskip\noindent There is still a feature of Isabelle's type system
|
8907
|
8 |
left that we have not yet discussed. When declaring polymorphic
|
10140
|
9 |
constants @{text "c \<Colon> \<sigma>"}, the type variables occurring in @{text \<sigma>}
|
|
10 |
may be constrained by type classes (or even general sorts) in an
|
8907
|
11 |
arbitrary way. Note that by default, in Isabelle/HOL the declaration
|
10140
|
12 |
@{text "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} is actually an abbreviation for
|
|
13 |
@{text "\<odot> \<Colon> 'a\<Colon>term \<Rightarrow> 'a \<Rightarrow> 'a"} Since class @{text "term"} is the
|
|
14 |
universal class of HOL, this is not really a constraint at all.
|
8903
|
15 |
|
10140
|
16 |
The @{text product} class below provides a less degenerate example of
|
8903
|
17 |
syntactic type classes.
|
9146
|
18 |
*}
|
8903
|
19 |
|
8890
|
20 |
axclass
|
9146
|
21 |
product < "term"
|
8890
|
22 |
consts
|
10140
|
23 |
product :: "'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>" 70)
|
8890
|
24 |
|
8903
|
25 |
text {*
|
10140
|
26 |
Here class @{text product} is defined as subclass of @{text term}
|
|
27 |
without any additional axioms. This effects in logical equivalence
|
|
28 |
of @{text product} and @{text term}, as is reflected by the trivial
|
|
29 |
introduction rule generated for this definition.
|
8903
|
30 |
|
10140
|
31 |
\medskip So what is the difference of declaring
|
|
32 |
@{text "\<odot> \<Colon> 'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a"} vs.\ declaring
|
|
33 |
@{text "\<odot> \<Colon> 'a\<Colon>term \<Rightarrow> 'a \<Rightarrow> 'a"} anyway? In this particular case
|
|
34 |
where @{text "product \<equiv> term"}, it should be obvious that both
|
|
35 |
declarations are the same from the logic's point of view. It even
|
|
36 |
makes the most sense to remove sort constraints from constant
|
|
37 |
declarations, as far as the purely logical meaning is concerned
|
|
38 |
\cite{Wenzel:1997:TPHOL}.
|
8903
|
39 |
|
|
40 |
On the other hand there are syntactic differences, of course.
|
10140
|
41 |
Constants @{text \<odot>} on some type @{text \<tau>} are rejected by the
|
|
42 |
type-checker, unless the arity @{text "\<tau> \<Colon> product"} is part of the
|
|
43 |
type signature. In our example, this arity may be always added when
|
|
44 |
required by means of an $\isarkeyword{instance}$ with the trivial
|
|
45 |
proof $\BY{intro_classes}$.
|
8903
|
46 |
|
|
47 |
\medskip Thus, we may observe the following discipline of using
|
|
48 |
syntactic classes. Overloaded polymorphic constants have their type
|
10140
|
49 |
arguments restricted to an associated (logically trivial) class
|
|
50 |
@{text c}. Only immediately before \emph{specifying} these constants
|
|
51 |
on a certain type @{text \<tau>} do we instantiate @{text "\<tau> \<Colon> c"}.
|
8903
|
52 |
|
10140
|
53 |
This is done for class @{text product} and type @{typ bool} as
|
|
54 |
follows.
|
9146
|
55 |
*}
|
8903
|
56 |
|
9146
|
57 |
instance bool :: product
|
|
58 |
by intro_classes
|
9306
|
59 |
defs (overloaded)
|
10140
|
60 |
product_bool_def: "x \<odot> y \<equiv> x \<and> y"
|
8890
|
61 |
|
8903
|
62 |
text {*
|
10140
|
63 |
The definition @{text prod_bool_def} becomes syntactically
|
|
64 |
well-formed only after the arity @{text "bool \<Colon> product"} is made
|
|
65 |
known to the type checker.
|
8903
|
66 |
|
|
67 |
\medskip It is very important to see that above $\DEFS$ are not
|
|
68 |
directly connected with $\isarkeyword{instance}$ at all! We were
|
10140
|
69 |
just following our convention to specify @{text \<odot>} on @{typ bool}
|
|
70 |
after having instantiated @{text "bool \<Colon> product"}. Isabelle does
|
|
71 |
not require these definitions, which is in contrast to programming
|
|
72 |
languages like Haskell \cite{haskell-report}.
|
8903
|
73 |
|
|
74 |
\medskip While Isabelle type classes and those of Haskell are almost
|
|
75 |
the same as far as type-checking and type inference are concerned,
|
8907
|
76 |
there are important semantic differences. Haskell classes require
|
|
77 |
their instances to \emph{provide operations} of certain \emph{names}.
|
8903
|
78 |
Therefore, its \texttt{instance} has a \texttt{where} part that tells
|
|
79 |
the system what these ``member functions'' should be.
|
|
80 |
|
10140
|
81 |
This style of \texttt{instance} would not make much sense in
|
|
82 |
Isabelle's meta-logic, because there is no internal notion of
|
|
83 |
``providing operations'' or even ``names of functions''.
|
9146
|
84 |
*}
|
8903
|
85 |
|
9146
|
86 |
end |