Type-Checking of Heterogeneous Sequences in Common Lisp

Authors: Jim Newton, Akim Demaille, Didier Verna
Where: European Lisp Symposium
Place: Kraków, Poland
Type: inproceedings
Projects: Climb
Keywords: Rational languages, typechecking, finite automata
Date: 2016-03-25

Abstract

We introduce the abstract concept of rational type expression and show its relationship to rational language theory. We further present a concrete syntax, regular type expression, and a Common Lisp implementation thereof which allows the programmer to declaratively express the types of heterogeneous sequences in a way which is natural in the Common Lisp language. The implementation uses techniques well known and well founded in rational language theory, in particular the use of the Brzozowski derivative and deterministic automata to reach a solution which can match a sequence in linear time. We illustrate the concept with several motivating examples, and finally explain many details of its implementation.

Documents

Paper

Slides

Efficient Dynamic Type-checking of Heterogeneous Sequences

Authors

Jim Newton, Akim Demaille, Didier Verna

Article submitted to ELS 9 2016

ELS 2016 Article Presentation Slides

Project Report

Report

Source code

You may download the source code from LRDE gitlab mirror

Bibtex (lrde.bib)

@InProceedings{	  newton.16.els,
  author	= {Jim Newton and Akim Demaille and Didier Verna},
  title		= {Type-Checking of Heterogeneous Sequences in {C}ommon
		  {L}isp},
  booktitle	= {European Lisp Symposium},
  year		= 2016,
  doi		= {10.5555/3005729.3005731},
  address	= {Krak{\'o}w, Poland},
  month		= may,
  abstract	= {We introduce the abstract concept of rational type
		  expression and show its relationship to rational language
		  theory. We further present a concrete syntax, regular type
		  expression, and a Common Lisp implementation thereof which
		  allows the programmer to declaratively express the types of
		  heterogeneous sequences in a way which is natural in the
		  Common Lisp language. The implementation uses techniques
		  well known and well founded in rational language theory, in
		  particular the use of the Brzozowski derivative and
		  deterministic automata to reach a solution which can match
		  a sequence in linear time. We illustrate the concept with
		  several motivating examples, and finally explain many
		  details of its implementation.}
}