84 |
84 |
85 Indeed, type classes not only allow for simple overloading |
85 Indeed, type classes not only allow for simple overloading |
86 but form a generic calculus, an instance of order-sorted |
86 but form a generic calculus, an instance of order-sorted |
87 algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}. |
87 algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}. |
88 |
88 |
89 From a software engineering point of view, type classes |
89 From a software engeneering point of view, type classes |
90 correspond to interfaces in object-oriented languages like Java; |
90 roughly correspond to interfaces in object-oriented languages like Java; |
91 so, it is naturally desirable that type classes do not only |
91 so, it is naturally desirable that type classes do not only |
92 provide functions (class parameters) but also state specifications |
92 provide functions (class parameters) but also state specifications |
93 implementations must obey. For example, the \isa{class\ eq} |
93 implementations must obey. For example, the \isa{class\ eq} |
94 above could be given the following specification, demanding that |
94 above could be given the following specification, demanding that |
95 \isa{class\ eq} is an equivalence relation obeying reflexivity, |
95 \isa{class\ eq} is an equivalence relation obeying reflexivity, |
739 Isabelle locales support a concept of local definitions |
739 Isabelle locales support a concept of local definitions |
740 in locales:% |
740 in locales:% |
741 \end{isamarkuptext}% |
741 \end{isamarkuptext}% |
742 \isamarkuptrue% |
742 \isamarkuptrue% |
743 \ \ \ \ \isacommand{primrec}\isamarkupfalse% |
743 \ \ \ \ \isacommand{primrec}\isamarkupfalse% |
744 \ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\isanewline |
744 \ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
745 \ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
746 \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline |
745 \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline |
747 \ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}% |
746 \ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}% |
748 \begin{isamarkuptext}% |
747 \begin{isamarkuptext}% |
749 \noindent If the locale \isa{group} is also a class, this local |
748 \noindent If the locale \isa{group} is also a class, this local |
750 definition is propagated onto a global definition of |
749 definition is propagated onto a global definition of |
804 When using this interpretation pattern, it may also |
803 When using this interpretation pattern, it may also |
805 be appropriate to map derived definitions accordingly:% |
804 be appropriate to map derived definitions accordingly:% |
806 \end{isamarkuptext}% |
805 \end{isamarkuptext}% |
807 \isamarkuptrue% |
806 \isamarkuptrue% |
808 \ \ \ \ \isacommand{fun}\isamarkupfalse% |
807 \ \ \ \ \isacommand{fun}\isamarkupfalse% |
809 \isanewline |
808 \ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ list\ {\isasymRightarrow}\ {\isasymalpha}\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
810 \ \ \ \ \ \ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ list\ {\isasymRightarrow}\ {\isasymalpha}\ list{\isachardoublequoteclose}\isanewline |
|
811 \ \ \ \ \isakeyword{where}\isanewline |
|
812 \ \ \ \ \ \ {\isachardoublequoteopen}replicate\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline |
809 \ \ \ \ \ \ {\isachardoublequoteopen}replicate\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline |
813 \ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline |
810 \ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline |
814 \isanewline |
811 \isanewline |
815 \ \ \ \ \isacommand{interpretation}\isamarkupfalse% |
812 \ \ \ \ \isacommand{interpretation}\isamarkupfalse% |
816 \ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isacharat}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isakeyword{where}\isanewline |
813 \ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isacharat}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isakeyword{where}\isanewline |
820 \ \ \ \ % |
817 \ \ \ \ % |
821 \endisadelimproof |
818 \endisadelimproof |
822 % |
819 % |
823 \isatagproof |
820 \isatagproof |
824 \isacommand{proof}\isamarkupfalse% |
821 \isacommand{proof}\isamarkupfalse% |
825 \isanewline |
822 \ {\isacharminus}\isanewline |
826 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% |
823 \ \ \ \ \ \ \isacommand{interpret}\isamarkupfalse% |
827 \ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline |
824 \ monoid\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isacharat}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
825 \isanewline |
828 \ \ \ \ \ \ \isacommand{show}\isamarkupfalse% |
826 \ \ \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
827 \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline |
|
828 \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse% |
|
829 \isanewline |
|
830 \ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% |
|
831 \ n\isanewline |
|
832 \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse% |
829 \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline |
833 \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline |
830 \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse% |
834 \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse% |
831 \ {\isacharparenleft}induct\ n{\isacharparenright}\ auto\isanewline |
835 \ {\isacharparenleft}induct\ n{\isacharparenright}\ auto\isanewline |
|
836 \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse% |
|
837 \isanewline |
832 \ \ \ \ \isacommand{qed}\isamarkupfalse% |
838 \ \ \ \ \isacommand{qed}\isamarkupfalse% |
833 % |
839 \ intro{\isacharunderscore}locales% |
834 \endisatagproof |
840 \endisatagproof |
835 {\isafoldproof}% |
841 {\isafoldproof}% |
836 % |
842 % |
837 \isadelimproof |
843 \isadelimproof |
838 % |
844 % |
1004 \ \ \ \ \ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}% |
1010 \ \ \ \ \ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}% |
1005 \begin{isamarkuptext}% |
1011 \begin{isamarkuptext}% |
1006 \noindent This maps to Haskell as:% |
1012 \noindent This maps to Haskell as:% |
1007 \end{isamarkuptext}% |
1013 \end{isamarkuptext}% |
1008 \isamarkuptrue% |
1014 \isamarkuptrue% |
1009 \isacommand{export{\isacharunderscore}code}\isamarkupfalse% |
1015 % |
1010 \ example\ \isakeyword{in}\ Haskell\ \isakeyword{module{\isacharunderscore}name}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}{\isachardoublequoteclose}% |
1016 \isadelimquoteme |
1011 \begin{isamarkuptext}% |
1017 % |
1012 \lsthaskell{Thy/code_examples/Classes.hs} |
1018 \endisadelimquoteme |
1013 |
1019 % |
1014 \noindent The whole code in SML with explicit dictionary passing:% |
1020 \isatagquoteme |
1015 \end{isamarkuptext}% |
1021 % |
1016 \isamarkuptrue% |
1022 \begin{isamarkuptext}% |
1017 \isacommand{export{\isacharunderscore}code}\isamarkupfalse% |
1023 \isaverbatim% |
1018 \ example\ \isakeyword{in}\ SML\ \isakeyword{module{\isacharunderscore}name}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}classes{\isachardot}ML{\isachardoublequoteclose}% |
1024 \noindent% |
1019 \begin{isamarkuptext}% |
1025 \verb|module Example where {|\newline% |
1020 \lstsml{Thy/code_examples/classes.ML}% |
1026 \newline% |
1021 \end{isamarkuptext}% |
1027 \newline% |
1022 \isamarkuptrue% |
1028 \verb|data Nat = Suc Nat |\verb,|,\verb| Zero_nat;|\newline% |
|
1029 \newline% |
|
1030 \verb|nat_aux :: Integer -> Nat -> Nat;|\newline% |
|
1031 \verb|nat_aux i n = (if i <= 0 then n else nat_aux (i - 1) (Suc n));|\newline% |
|
1032 \newline% |
|
1033 \verb|nat :: Integer -> Nat;|\newline% |
|
1034 \verb|nat i = nat_aux i Zero_nat;|\newline% |
|
1035 \newline% |
|
1036 \verb|class Semigroup a where {|\newline% |
|
1037 \verb| mult :: a -> a -> a;|\newline% |
|
1038 \verb|};|\newline% |
|
1039 \newline% |
|
1040 \verb|class (Semigroup a) => Monoidl a where {|\newline% |
|
1041 \verb| neutral :: a;|\newline% |
|
1042 \verb|};|\newline% |
|
1043 \newline% |
|
1044 \verb|class (Monoidl a) => Monoid a where {|\newline% |
|
1045 \verb|};|\newline% |
|
1046 \newline% |
|
1047 \verb|class (Monoid a) => Group a where {|\newline% |
|
1048 \verb| inverse :: a -> a;|\newline% |
|
1049 \verb|};|\newline% |
|
1050 \newline% |
|
1051 \verb|inverse_int :: Integer -> Integer;|\newline% |
|
1052 \verb|inverse_int i = negate i;|\newline% |
|
1053 \newline% |
|
1054 \verb|neutral_int :: Integer;|\newline% |
|
1055 \verb|neutral_int = 0;|\newline% |
|
1056 \newline% |
|
1057 \verb|mult_int :: Integer -> Integer -> Integer;|\newline% |
|
1058 \verb|mult_int i j = i + j;|\newline% |
|
1059 \newline% |
|
1060 \verb|instance Semigroup Integer where {|\newline% |
|
1061 \verb| mult = mult_int;|\newline% |
|
1062 \verb|};|\newline% |
|
1063 \newline% |
|
1064 \verb|instance Monoidl Integer where {|\newline% |
|
1065 \verb| neutral = neutral_int;|\newline% |
|
1066 \verb|};|\newline% |
|
1067 \newline% |
|
1068 \verb|instance Monoid Integer where {|\newline% |
|
1069 \verb|};|\newline% |
|
1070 \newline% |
|
1071 \verb|instance Group Integer where {|\newline% |
|
1072 \verb| inverse = inverse_int;|\newline% |
|
1073 \verb|};|\newline% |
|
1074 \newline% |
|
1075 \verb|pow_nat :: forall a. (Monoid a) => Nat -> a -> a;|\newline% |
|
1076 \verb|pow_nat Zero_nat x = neutral;|\newline% |
|
1077 \verb|pow_nat (Suc n) x = mult x (pow_nat n x);|\newline% |
|
1078 \newline% |
|
1079 \verb|pow_int :: forall a. (Group a) => Integer -> a -> a;|\newline% |
|
1080 \verb|pow_int k x =|\newline% |
|
1081 \verb| (if 0 <= k then pow_nat (nat k) x|\newline% |
|
1082 \verb| else inverse (pow_nat (nat (negate k)) x));|\newline% |
|
1083 \newline% |
|
1084 \verb|example :: Integer;|\newline% |
|
1085 \verb|example = pow_int 10 (-2);|\newline% |
|
1086 \newline% |
|
1087 \verb|}|% |
|
1088 \end{isamarkuptext}% |
|
1089 \isamarkuptrue% |
|
1090 % |
|
1091 \endisatagquoteme |
|
1092 {\isafoldquoteme}% |
|
1093 % |
|
1094 \isadelimquoteme |
|
1095 % |
|
1096 \endisadelimquoteme |
|
1097 % |
|
1098 \begin{isamarkuptext}% |
|
1099 \noindent The whole code in SML with explicit dictionary passing:% |
|
1100 \end{isamarkuptext}% |
|
1101 \isamarkuptrue% |
|
1102 % |
|
1103 \isadelimquoteme |
|
1104 % |
|
1105 \endisadelimquoteme |
|
1106 % |
|
1107 \isatagquoteme |
|
1108 % |
|
1109 \begin{isamarkuptext}% |
|
1110 \isaverbatim% |
|
1111 \noindent% |
|
1112 \verb|structure Example = |\newline% |
|
1113 \verb|struct|\newline% |
|
1114 \newline% |
|
1115 \verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline% |
|
1116 \newline% |
|
1117 \verb|fun nat_aux i n =|\newline% |
|
1118 \verb| (if IntInf.<= (i, (0 : IntInf.int)) then n|\newline% |
|
1119 \verb| else nat_aux (IntInf.- (i, (1 : IntInf.int))) (Suc n));|\newline% |
|
1120 \newline% |
|
1121 \verb|fun nat i = nat_aux i Zero_nat;|\newline% |
|
1122 \newline% |
|
1123 \verb|type 'a semigroup = {mult : 'a -> 'a -> 'a};|\newline% |
|
1124 \verb|fun mult (A_:'a semigroup) = #mult A_;|\newline% |
|
1125 \newline% |
|
1126 \verb|type 'a monoidl =|\newline% |
|
1127 \verb| {Classes__semigroup_monoidl : 'a semigroup, neutral : 'a};|\newline% |
|
1128 \verb|fun semigroup_monoidl (A_:'a monoidl) = #Classes__semigroup_monoidl A_;|\newline% |
|
1129 \verb|fun neutral (A_:'a monoidl) = #neutral A_;|\newline% |
|
1130 \newline% |
|
1131 \verb|type 'a monoid = {Classes__monoidl_monoid : 'a monoidl};|\newline% |
|
1132 \verb|fun monoidl_monoid (A_:'a monoid) = #Classes__monoidl_monoid A_;|\newline% |
|
1133 \newline% |
|
1134 \verb|type 'a group = {Classes__monoid_group : 'a monoid, inverse : 'a -> 'a};|\newline% |
|
1135 \verb|fun monoid_group (A_:'a group) = #Classes__monoid_group A_;|\newline% |
|
1136 \verb|fun inverse (A_:'a group) = #inverse A_;|\newline% |
|
1137 \newline% |
|
1138 \verb|fun inverse_int i = IntInf.~ i;|\newline% |
|
1139 \newline% |
|
1140 \verb|val neutral_int : IntInf.int = (0 : IntInf.int);|\newline% |
|
1141 \newline% |
|
1142 \verb|fun mult_int i j = IntInf.+ (i, j);|\newline% |
|
1143 \newline% |
|
1144 \verb|val semigroup_int = {mult = mult_int} : IntInf.int semigroup;|\newline% |
|
1145 \newline% |
|
1146 \verb|val monoidl_int =|\newline% |
|
1147 \verb| {Classes__semigroup_monoidl = semigroup_int, neutral = neutral_int} :|\newline% |
|
1148 \verb| IntInf.int monoidl;|\newline% |
|
1149 \newline% |
|
1150 \verb|val monoid_int = {Classes__monoidl_monoid = monoidl_int} :|\newline% |
|
1151 \verb| IntInf.int monoid;|\newline% |
|
1152 \newline% |
|
1153 \verb|val group_int =|\newline% |
|
1154 \verb| {Classes__monoid_group = monoid_int, inverse = inverse_int} :|\newline% |
|
1155 \verb| IntInf.int group;|\newline% |
|
1156 \newline% |
|
1157 \verb|fun pow_nat A_ Zero_nat x = neutral (monoidl_monoid A_)|\newline% |
|
1158 \verb| |\verb,|,\verb| pow_nat A_ (Suc n) x =|\newline% |
|
1159 \verb| mult ((semigroup_monoidl o monoidl_monoid) A_) x (pow_nat A_ n x);|\newline% |
|
1160 \newline% |
|
1161 \verb|fun pow_int A_ k x =|\newline% |
|
1162 \verb| (if IntInf.<= ((0 : IntInf.int), k)|\newline% |
|
1163 \verb| then pow_nat (monoid_group A_) (nat k) x|\newline% |
|
1164 \verb| else inverse A_ (pow_nat (monoid_group A_) (nat (IntInf.~ k)) x));|\newline% |
|
1165 \newline% |
|
1166 \verb|val example : IntInf.int =|\newline% |
|
1167 \verb| pow_int group_int (10 : IntInf.int) (~2 : IntInf.int);|\newline% |
|
1168 \newline% |
|
1169 \verb|end; (*struct Example*)|% |
|
1170 \end{isamarkuptext}% |
|
1171 \isamarkuptrue% |
|
1172 % |
|
1173 \endisatagquoteme |
|
1174 {\isafoldquoteme}% |
|
1175 % |
|
1176 \isadelimquoteme |
|
1177 % |
|
1178 \endisadelimquoteme |
1023 % |
1179 % |
1024 \isadelimtheory |
1180 \isadelimtheory |
1025 % |
1181 % |
1026 \endisadelimtheory |
1182 \endisadelimtheory |
1027 % |
1183 % |