1293 |
1293 |
1294 section {* Sorts (TBD) *} |
1294 section {* Sorts (TBD) *} |
1295 |
1295 |
1296 text {* |
1296 text {* |
1297 Type classes are formal names in the type system which are linked to |
1297 Type classes are formal names in the type system which are linked to |
1298 predicates on of one type variable (via the axclass mechanism) and thereby |
1298 predicates of one type variable (via the axclass mechanism) and thereby |
1299 express extra properties on types to be propagated by the type system. |
1299 express extra properties on types, to be propagated by the type system. |
1300 The type-in-class judgement is defined |
1300 The type-in-class judgement is defined |
1301 over a simple logic based on implication and schematic quantification. |
1301 via a simple logic over types, with inferences solely based on |
1302 The signature of this logic is called an order-sorted algebra (see Schmidt-Schauss) |
1302 modus ponens, instantiation and axiom use. |
1303 and consists of an acyclic subclass relation and a set of image |
1303 The declared axioms of this logic are called an order-sorted algebra (see Schmidt-Schauss). |
|
1304 It consists of an acyclic subclass relation and a set of image containment |
1304 declarations for type constructors, called arities. |
1305 declarations for type constructors, called arities. |
1305 |
1306 |
1306 A well-behaved high-level view on type classes has long been established |
1307 A well-behaved high-level view on type classes has long been established |
1307 (cite Haftmann-Wenzel): the predicate behind a type class is the basis for a locale |
1308 (cite Haftmann-Wenzel): the predicate behind a type class is the foundation |
1308 (for context-management reasons) |
1309 of a locale (for context-management reasons) |
1309 and may use so-called type class parameters which are implemented as overloaded |
1310 and may use so-called type class parameters. These are type-indexed constants |
1310 constants. Overloading a constant means specifying its type-indexed value based on |
1311 dependent on the sole type variable and are implemented via overloading. |
1311 a well-founded reduction towards other constants. When instantiating type classes |
1312 Overloading a constant means specifying its value on a type based on |
|
1313 a well-founded reduction towards other values of constants on types. |
|
1314 When instantiating type classes |
1312 (i.e. proving arities) you are specifying overloading via primitive recursion. |
1315 (i.e. proving arities) you are specifying overloading via primitive recursion. |
1313 |
1316 |
1314 Sorts are finite intersections of type classes and are implemented as lists |
1317 Sorts are finite intersections of type classes and are implemented as lists |
1315 of type class names. The empty intersection, i.e. the empty list, is therefore |
1318 of type class names. The empty intersection, i.e. the empty list, is therefore |
1316 inhabited by all types and is called the topsort. |
1319 inhabited by all types and is called the topsort. |
1317 |
1320 |
1318 Free and schematic type variables may be annotated with sorts, thereby restricting |
1321 Free and schematic type variables are always annotated with sorts, thereby restricting |
1319 the domain of types they quantify over and corresponding to an implicit hypothesis |
1322 the domain of types they quantify over and corresponding to an implicit hypothesis |
1320 about the type variable. |
1323 about the type variable. |
1321 *} |
1324 *} |
1322 |
1325 |
1323 |
1326 |
1328 Classes, sorts and arities are defined in @{ML_file "Pure/term.ML"}. |
1331 Classes, sorts and arities are defined in @{ML_file "Pure/term.ML"}. |
1329 |
1332 |
1330 @{ML_file "Pure/sorts.ML"} contains comparison and normalization functionality for sorts, |
1333 @{ML_file "Pure/sorts.ML"} contains comparison and normalization functionality for sorts, |
1331 manages the order sorted algebra and offers an interface for reinterpreting |
1334 manages the order sorted algebra and offers an interface for reinterpreting |
1332 derivations of type in class judgements |
1335 derivations of type in class judgements |
1333 @{ML_file "Pure/defs.ML"} manages the constant definition dependency graph and keeps it well-founded |
1336 @{ML_file "Pure/defs.ML"} manages the constant dependency graph and keeps it well-founded |
1334 (its define function doesn't terminate for complex non-well-founded dependencies) |
1337 (its define function doesn't terminate for complex non-well-founded dependencies) |
1335 @{ML_file "Pure/axclass.ML"} manages the theorems that back up subclass and arity relations |
1338 @{ML_file "Pure/axclass.ML"} manages the theorems that back up subclass and arity relations |
1336 and provides basic infrastructure for establishing the high-level view on type classes |
1339 and provides basic infrastructure for establishing the high-level view on type classes |
1337 @{ML_file "Pure/sign.ML"} is a common interface to all the type-theory-like declarations |
1340 @{ML_file "Pure/sign.ML"} is a common interface to all the type-theory-like declarations |
1338 (especially names, constants, paths, type classes) a |
1341 (especially names, constants, paths, type classes) a |