Draft:Coalton (programming language)

Robert Smith started designing Coalton in 2018^[3] to import the benefits of ML-like static typing into the interactive, incremental programming environment of Common Lisp. Coalton was further developed by a team led by Smith and was officially announced in 2021.^[4] Coalton has since been used for quantum computing research, the implementation of the Quil compiler,^[5] and defense applications.

Coalton is used at HRL Laboratories to build software for qubits based on exchange-only silicon quantum dots.^[6]

• Static typing with global type inference and optional type declarations.
• Parametric algebraic data types, pattern matching, and compile-time exhaustiveness checking.
• Multi-parameter type classes with functional dependencies.
• Strictly evaluated with lazy iterators.
• Advanced immutable data structures including hash array mapped tries and relaxed radix balanced trees.
• Machine code compilation (on Lisp hosts that support it).
• Compiler optimizations including heuristic inlining and user-controllable inlining with the inline directive.
• User-controllable function monomorphization with the monomorphize directive.
• User-controllable data type representation control with the repr directive.
• Separate development and release modes. Release mode enables greater compiler optimization opportunities at the expense of development interactivity.
• Non-allocating Optional data type (cf. Haskell's Maybe or OCaml's Option).
• Exception handling with resumptions.
• Inline Common Lisp code with the lisp operator.
• Metaprogramming via ordinary defmacro.
• Advanced numerical data types including dual numbers, hyper-dual numbers, computable real numbers, and arbitrary-precision floating-point numbers.

When Coalton is written in a Lisp file, Coalton code is wrapped in coalton-toplevel:

(coalton-toplevel
  ;; ...definition forms...
  )

In the following examples, we elide the coalton-toplevel form.

Expressions are written in Lisp's prefix style:

(define pi-approx (/ 355.0 113.0))
(define earth-diameter-km 12756.0)
(define earth-circumference-km (* pi-approx earth-diameter-km))

Functions are defined with define:

(define (square-area width height)
  (* width height))

Algebraic data types are defined with define-type and can be pattern matched:

(define-type (Shape :t)
  (Rect :t :t)  ; width x height
  (Circle :t))  ; radius

(define (area s)
 (match s
   ((Rect width height) (* width height))
   ((Circle radius)     (* coalton-library/math:pi (^ radius 2)))))

The type of area is automatically inferred as (Num :t) (Trigonometric :t) ⇒ (Shape :t → :t), which means that areas can be computed on shapes whose dimensions are specified to be numerical and trigonometric.

Type classes can be defined with define-type. A mathematical Group type class may be written like:

(define-class (Group :t)
  (identity-element (:t))
  (invert-element   (:t -> :t))
  (group-operation  (:t -> :t -> :t)))

We may then define the additive group of integers ${\displaystyle (\mathbb {Z} ,+)}$ by defining an instance of the type class on Integer:

(define-instance (Group Integer)
  (define identity-element 0)

  (define (invert-element x)
    (negate x))

  (define (group-operation x y)
    (+ x y)))

Saving an executable is done via the host Lisp compiler. A "Hello World" executable can be made by creating a file hello.lisp:

(coalton-toplevel
  (define (main)
    (trace "Hello, world!")))

With a Common Lisp compiler like SBCL, an executable called hello can be produced with:

sbcl --eval '(asdf:load-system "coalton")' \
     --load hello.lisp \
     --eval '(sb-ext:save-lisp-and-die "hello"
               :executable t
               :toplevel (lambda () (coalton:coalton (coalton-user::main))))' \
     --quit

Running the executable produces the expected output:

% ./hello
Hello, world!

When Coalton is written as a part of .lisp files, it requires wrapping the Coalton code in coalton or coalton-toplevel macros. This detracts from the incremental development style of Common Lisp.^[7]

A more serious criticism is that Hindley-Milner type systems are unsound when mutation is allowed,^[8] and Coalton allows mutation. Several fixes to the type inference algorithm have been proposed.^[9]