Programmatic Manipulation of Common Lisp Type Specifiers

Authors

Jim Newton, Didier Verna, Maximilien Colange

Where

European Lisp Symposium

Place

Brussels, Belgium

Type

inproceedings

Projects

Climb

Keywords

Rational languages, typechecking, finite automata

Date

2017-02-06

Abstract

In this article we contrast the use of the s-expression (a ubiquitous data structure in Common Lisp) with the BDD (Binary Decision Diagram) as a data structure for programmatically manipulating Common Lisp type specifiers. The s-expression is the de facto standard surface syntax and also programmatic representation of the type specifier, but the BDD data structure offers advantages: most notably, type equivalence checks using s-expressions can be computationally intensive, whereas the type equivalence check using BDDs is a check for object identity. As an implementation and performance experiment, we define the notion of maximal disjoint type decomposition, and discuss implementations of algorithms to compute it: a brute force iteration, as a tree reduction, and as a version of the SAT problem (the satisfiability problem). The experimental implementations represent type specifiers by both aforementioned data structures, and we compare the performance observed in each approach.

Documents

• Paper

See also the Technical Report with many more details.