38 |
38 |
39 On the other hand there are syntactic differences, of course. |
39 On the other hand there are syntactic differences, of course. |
40 Constants \isa{{\isasymodot}} on some type \isa{{\isasymtau}} are rejected by the |
40 Constants \isa{{\isasymodot}} on some type \isa{{\isasymtau}} are rejected by the |
41 type-checker, unless the arity \isa{{\isasymtau}\ {\isasymColon}\ product} is part of the |
41 type-checker, unless the arity \isa{{\isasymtau}\ {\isasymColon}\ product} is part of the |
42 type signature. In our example, this arity may be always added when |
42 type signature. In our example, this arity may be always added when |
43 required by means of an $\isarkeyword{instance}$ with the trivial |
43 required by means of an $\INSTANCE$ with the trivial proof |
44 proof $\BY{intro_classes}$. |
44 $\BY{intro_classes}$. |
45 |
45 |
46 \medskip Thus, we may observe the following discipline of using |
46 \medskip Thus, we may observe the following discipline of using |
47 syntactic classes. Overloaded polymorphic constants have their type |
47 syntactic classes. Overloaded polymorphic constants have their type |
48 arguments restricted to an associated (logically trivial) class |
48 arguments restricted to an associated (logically trivial) class |
49 \isa{c}. Only immediately before \emph{specifying} these constants |
49 \isa{c}. Only immediately before \emph{specifying} these constants |
60 The definition \isa{prod{\isacharunderscore}bool{\isacharunderscore}def} becomes syntactically |
60 The definition \isa{prod{\isacharunderscore}bool{\isacharunderscore}def} becomes syntactically |
61 well-formed only after the arity \isa{bool\ {\isasymColon}\ product} is made |
61 well-formed only after the arity \isa{bool\ {\isasymColon}\ product} is made |
62 known to the type checker. |
62 known to the type checker. |
63 |
63 |
64 \medskip It is very important to see that above $\DEFS$ are not |
64 \medskip It is very important to see that above $\DEFS$ are not |
65 directly connected with $\isarkeyword{instance}$ at all! We were |
65 directly connected with $\INSTANCE$ at all! We were just following |
66 just following our convention to specify \isa{{\isasymodot}} on \isa{bool} |
66 our convention to specify \isa{{\isasymodot}} on \isa{bool} after having |
67 after having instantiated \isa{bool\ {\isasymColon}\ product}. Isabelle does |
67 instantiated \isa{bool\ {\isasymColon}\ product}. Isabelle does not require |
68 not require these definitions, which is in contrast to programming |
68 these definitions, which is in contrast to programming languages like |
69 languages like Haskell \cite{haskell-report}. |
69 Haskell \cite{haskell-report}. |
70 |
70 |
71 \medskip While Isabelle type classes and those of Haskell are almost |
71 \medskip While Isabelle type classes and those of Haskell are almost |
72 the same as far as type-checking and type inference are concerned, |
72 the same as far as type-checking and type inference are concerned, |
73 there are important semantic differences. Haskell classes require |
73 there are important semantic differences. Haskell classes require |
74 their instances to \emph{provide operations} of certain \emph{names}. |
74 their instances to \emph{provide operations} of certain \emph{names}. |