Previous Version

See the tag 2022.09.

Continuing Motivation

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-type and no longer needs to define the subtypep and intersect-type-p for such types. Examples of these types include %array complex cons %symbol %char in 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 rational in 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 define-specializing-type.

Comparison 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.

Dependent 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.

Function Types

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.

Usage

:use the extensible-compound-types-cl package after loading the system with the same name.

Examples

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 subtypep and intersect-type-p relations for your types. Examples of these can be found in src/basic-types/cl-compound-types.lisp.

Both define-orthogonally-specializing-type and 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.

Basic API

Working with existing types

typep, subtypep, intersect-type-p, supertypep
upgraded-cl-type
deftype
type-specifier-p
typexpand, typexpand-1
intersection-null-p
the
check-type

Defining new types

define-orthogonally-specializing-type
define-specializing-type
define-compound-type
define-subtypep-lambda
define-intersect-type-p-lambda
define-cl-type-for-extype

Other shadowed symbols

type
extype
ftype
exftype

Interface types

For examples, see the .lisp files in src/interfaces.

(define-interface name &rest interface-function-names)
(define-interface-instance interface-name type &rest function-definitions)

Example of parametric type does not work

Hi! I am trying an example which defines pair type. It does not work for me. My SBCL is 2.2.8. This is what I try:

Firstly I create a file with the following content:

(defpackage parametric-types-demo
  (:use #:extensible-compound-types-cl
        #:polymorphic-functions))

(in-package :parametric-types-demo)

(defstruct pair a b)

(define-compound-type pair (o &optional (type-a 'cl:*) (type-b 'cl:*))
  "A user-defined compound-type that allows the specification of the
types of the values stored in slots A and B of the structure-class
PAIR."
  (and (cl:typep o 'pair)
       (with-slots (a b) o
         (and (if (eq 'cl:* type-a)
                  t
                  (cl:typep a type-a))
              (if (eq 'cl:* type-b)
                  t
                  (cl:typep b type-b))))))

Secondly, in the REPL I do the following:

* (push :extensible-compound-types cl:*features*)
(:EXTENSIBLE-COMPOUND-TYPES :QUICKLISP :ASDF3.3 :ASDF3.2 :ASDF3.1 :ASDF3 :ASDF2
 :ASDF :OS-UNIX :NON-BASE-CHARS-EXIST-P :ASDF-UNICODE :SINGLE-FLOAT-TRAN
 :X86-64 :GENCGC :64-BIT :ANSI-CL :BSD :COMMON-LISP :ELF :FREEBSD
 :IEEE-FLOATING-POINT :LITTLE-ENDIAN :PACKAGE-LOCAL-NICKNAMES
 :SB-CORE-COMPRESSION :SB-LDB :SB-PACKAGE-LOCKS :SB-THREAD :SB-UNICODE :SBCL
 :UNIX)
*
(ql:quickload :polymorphic-functions)
To load "polymorphic-functions":
  Load 1 ASDF system:
    polymorphic-functions
; Loading "polymorphic-functions"
..................................................
[package polymorphic-functions.defpackage]........
[package polymorphic-functions.extended-types]....
[package polymorphic-functions.nonuser]...........
[package polymorphic-functions]...................
.................................
(:POLYMORPHIC-FUNCTIONS)
* (ql:quickload :extensible-compound-types)
To load "extensible-compound-types":
  Load 1 ASDF system:
    extensible-compound-types
; Loading "extensible-compound-types"

(:EXTENSIBLE-COMPOUND-TYPES)
* (ql:quickload :extensible-compound-types-cl)
To load "extensible-compound-types-cl":
  Load 1 ASDF system:
    extensible-compound-types-cl
; Loading "extensible-compound-types-cl"

(:EXTENSIBLE-COMPOUND-TYPES-CL)
* (compile-file "~/testext.lisp")
; compiling file "~/testext.lisp" (written 08 SEP 2022 07:54:13 PM):
; processing (DEFPACKAGE PARAMETRIC-TYPES-DEMO ...)
; processing (IN-PACKAGE :PARAMETRIC-TYPES-DEMO)
; processing (DEFSTRUCT PAIR ...)
; processing (DEFINE-COMPOUND-TYPE PAIR ...)
; file: ~/testext.lisp
; in: DEFINE-COMPOUND-TYPE PAIR
;     (EXTENSIBLE-COMPOUND-TYPES:DEFINE-COMPOUND-TYPE PARAMETRIC-TYPES-DEMO::PAIR
;         (PARAMETRIC-TYPES-DEMO::O &OPTIONAL (PARAMETRIC-TYPES-DEMO::TYPE-A '*)
;          (PARAMETRIC-TYPES-DEMO::TYPE-B '*))
;       "A user-defined compound-type that allows the specification of the
;   types of the values stored in slots A and B of the structure-class
;   PAIR."
;       (AND (TYPEP PARAMETRIC-TYPES-DEMO::O 'PARAMETRIC-TYPES-DEMO::PAIR)
;            (EXTENSIBLE-COMPOUND-TYPES-CL:WITH-SLOTS (PARAMETRIC-TYPES-DEMO::A
;                                                      PARAMETRIC-TYPES-DEMO::B)
;                PARAMETRIC-TYPES-DEMO::O
;              (AND
;               (IF #
;                   T
;                   #)
;               (IF #
;                   T
;                   #)))))
; --> DEFTYPE PROGN EVAL-WHEN
; ==>
;   (SB-IMPL::%DEFTYPE 'PARAMETRIC-TYPES-DEMO::PAIR
;                      (SB-INT:NAMED-LAMBDA (SB-IMPL::TYPE-EXPANDER
;                                            PARAMETRIC-TYPES-DEMO::PAIR)
;                          (#:EXPR &AUX (#:FORM0 #:EXPR))
;                        (DECLARE (SB-C::LAMBDA-LIST (&OPTIONAL # #)))
;                        (SB-INT:NAMED-DS-BIND (:MACRO
;                                               PARAMETRIC-TYPES-DEMO::PAIR
;                                               . DEFTYPE)
;                            (&OPTIONAL (PARAMETRIC-TYPES-DEMO::TYPE-A '*)
;                             (PARAMETRIC-TYPES-DEMO::TYPE-B '*))
;                            (CDR #:EXPR)
;                          (DECLARE
;                           (SB-C::CONSTANT-VALUE PARAMETRIC-TYPES-DEMO::TYPE-A
;                                                 PARAMETRIC-TYPES-DEMO::TYPE-B))
;                          (DECLARE
;                           (IGNORE PARAMETRIC-TYPES-DEMO::TYPE-A
;                            PARAMETRIC-TYPES-DEMO::TYPE-B))
;                          (BLOCK PARAMETRIC-TYPES-DEMO::PAIR
;                            (EXTENSIBLE-COMPOUND-TYPES:UPGRADED-CL-TYPE
;                             #:FORM0))))
;                      NIL)
;
; caught WARNING:
;   The class PAIR is being redefined to be a DEFTYPE.

A call to compile-file does not return, it just does some work so I have to interrupt it. Any ideas what's wrong?

digikar99 / extensible-compound-types Goto Github PK

extensible-compound-types's Introduction

Previous Version

Continuing Motivation

Comparison with Hindley-Milner and/or Coalton Data Types

Dependent Types, Common Lisp Types, The Ugly Parts

Function Types

Usage

Examples

Basic API

Working with existing types

Defining new types

Other shadowed symbols

Interface types

extensible-compound-types's People

Contributors

Stargazers

Watchers

extensible-compound-types's Issues

Recommend Projects

Recommend Topics

Recommend Org