EXTENSIBLE-COMPOUND-TYPES for user-defined compound-types like (array &optional element-type dimension-spec)
See the tag 2022.09.
After a maintainably-failed attempt at a previous version of extensible-compound-types, and some learnt lessons, here is the second attempt for extensible-compound-types.
The primary motivation for this library has been to provide a way to express a
(custom-array element-type dimensions/rank) just like these can be expressed for the built-in type
cl:array. The more general version of these types are what CLHS calls Compound Types.
However, for a good subtypep, this requires defining subtypep (as well as intersect-type-p) relations for every pair of primitive types. In other words, the number of subtypep and intersect-type-p methods required for a good subtypep grows quadratically with the number of primitive types, and this becomes unmaintainable quickly.
However, several observations help in managing the complexity:
- The first is noting that for several types, each type parameter specializes independently - or orthogonally - of the other type parameters. For example, in (cl:array element-type dim/rank), the element-type parameter specializes independently of the dim/rank parameter. Not all types follow this convention, in (integer low high), low and high are not independent of each other. In the current version, such types are defined in terms of a single primitive compound type
specializing. Thus, the user only needs to define the type's "slots" using
define-orthogonally-specializing-typeand no longer needs to define the subtypep and intersect-type-p for such types. Examples of these types include
%array complex cons %symbol %charin src/basic-types/cl-compound-types.lisp.
- Even in cases when orthogonal specialization is not possible, it is possible to play nice with subtypep by using the class hierarchy. We note that these types are always associated with a class. Examples of such types include
integer single-float double-float rationalin src/basic-types/cl-compound-types.lisp. Such types require defining subtypep and intersect-type-p relations, but only within the same types. It is reasonably doable to infer the subtypep or intersect-type-p relations with other types without additional effort. While earlier, this observation was incorporated into the subtypep and intersect-type-p functions at the top level itself, in this attempt of extensible-compound-types, these are better abstracted out through the
2.1Comparison with Hindley-Milner and/or Coalton Data Types
Coalton provides full type inference through the well-developed theory of the Hindley-Milner type system; however, HM does not allow one to express types that depend on values. And while it is possible to express some dependent types through HM, this is not possible in the general case. In essence, expressing
(float -1.0 1.0) or
(integer 0 255) is possible in Common Lisp Type System, but not in Hindley-Milner Type System.
In the general case, I'd love to be able to express parametric dependent types that also play nice with Common Lisp's subtyping system. subtyping is important in order to express relations like "upper-triangular-array is a subtype of array", which can enable better specialization dispatch in a numerical computing library.
2.2Dependent Types, Common Lisp Types, The Ugly Parts
In its current state,
extensible-compound-types is far from a proper dependently typed system. However, even if a proper dependently typed system is developed, one has to do the ugly work of bridging it with the builtin Common Lisp types, especially
and or not eql satisfies, and indeed, the ugliest parts of extensible-compound-types reside in src/basic-types/compound-only-subtypep.lisp and src/basic-types/compound-only-intersect-type-p.lisp. Thus, any proper dependently typed system that integrates well into the Common Lisp type system has to deal with these ugly parts.
Coupled with cl-form-types and closer-mop:funcallable-standard-class,
extensible-compound-types does seem to be more general than a proper dependently typed system. In other words, the task of converting extensible-compound-types to a proper dependently typed system lies in constraining it correctly.
Currently, extensible-compound-types does not provide any additional support for parametric functions beyond what the builtin type system provides. Doing so involves at the least two pieces of work:
- subclassing closer-mop:funcallable-standard-class to create a function class that stores the types of its instances. Common Lisp builtin function objects provide no facility for storing their types within them.
- Thinking about what a good or useful subtypep or intersect-type-p relation might look like.
To actually support parametric polymorphism and dependent types will require even more work.
extensible-compound-types-cl package after loading the system with the same name.
Much of the code in src/basic-types can be used as the starting point. A bird's eye view goes as follows.
If you want to express types as something that "specializes" a class, just like how the builtin type
(cl:array element-type dim/rank) specializes the class
array, then try to use the
define-orthogonally-specializing-type macro. This enables the type to play nice with respect to subtypep and intersect-type-p without any additional work on your part. However, if
define-orthogonally-specializing-type becomes insufficient for your needs, then try using the
define-specializing-type macro. This will require you to define
intersect-type-p relations for your types. Examples of these can be found in src/basic-types/cl-compound-types.lisp.
define-specializing-type are better than
define-compound-type. The latter should only be used for the most generic types, and putting it to good use requires one to define subtypep and intersect-type-p methods for all the rest of the primitive compound types. See the rest of the files in src/basic-types for examples on this.
TODO: Add examples on this page itself.
5.1Working with existing types
- typep, subtypep, intersect-type-p, supertypep
- typexpand, typexpand-1
5.2Defining new types
5.3Other shadowed symbols