1297   Free and schematic variables may be annotated with sorts. Sorts are lists

  1297   Type classes are formal names in the type system which are linked to

  1298   of strings, whereby each string stands for a class. Sorts classify types.

  1298   predicates on of one type variable (via the axclass mechanism) and thereby

  1299 

  1299   express extra properties on types to be propagated by the type system.

  1300   The type-in-class judgement is defined

  1301   over a simple logic based on implication and schematic quantification.

  1302   The signature of this logic is called an order-sorted algebra (see Schmidt-Schauss)

  1303   and consists of an acyclic subclass relation and a set of image

  1304   declarations for type constructors, called arities.

  1305 

  1306   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   (for context-management reasons)

  1309   and may use so-called type class parameters which are implemented as overloaded

  1310   constants. Overloading a constant means specifying its type-indexed value based on

  1311   a well-founded reduction towards other constants. When instantiating type classes

  1312   (i.e. proving arities) you are specifying overloading via primitive recursion.

  1313 

  1314   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

  1316   inhabited by all types and is called the topsort.

  1317 

  1318   Free and schematic type variables may be annotated with sorts, thereby restricting

  1319   the domain of types they quantify over and corresponding to an implicit hypothesis

  1320   about the type variable.

  1309   @{ML_file "Pure/sign.ML"}

  1330   @{ML_file "Pure/sorts.ML"} contains comparison and normalization functionality for sorts,

  1310   @{ML_file "Pure/sorts.ML"}

  1331     manages the order sorted algebra and offers an interface for reinterpreting

  1311   @{ML_file "Pure/axclass.ML"}

  1332     derivations of type in class judgements

  1333   @{ML_file "Pure/defs.ML"} manages the constant definition dependency graph and keeps it well-founded

  1334     (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

  1336     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

  1338     (especially names, constants, paths, type classes) a

  1339     theory acquires by theory extension mechanisms and manages associated certification

  1340     functionality.

  1341     It also provides the most needed functionality from individual underlying modules.