Crate voile

Voile is a dependently-typed row-polymorphic programming language.

Design

Goal

The focus of Voile is extensible algebraic data types on top of dependent types. It can solve the expression problem without using any design patterns (like visitor or object-algebra in Java, or finally-tagless or DTALC in Haskell).

Features

• First-class language components
  • Sum/Record
• Dependent type goodies
  • Pi/Sigma

Extensible ADTs

Voile supports sum-types (coproduct), record-types (product) and their instances as first-class language components.

First-class record support is related to Record Calculus, or Extensible Records, or "first-class labels". The idea of "extensible record" is that the creation, manipulation and destruction of "records" can be done locally as an expression, without the need of declaring a record type globally, like:

$$ \newcommand{\Unit}[0]{\texttt{Rec} \{ \}} \newcommand{\Bool}[0]{\texttt{Sum} \{ \texttt{true}: \Unit \mid \texttt{false}: \Unit \}} \begin{alignedat}{2} &\texttt{not}&&:\Bool \\ \space & && \rarr \Bool \\ \space &\texttt{ifThenElse}&&:\forall A: \Bool \rarr A \rarr A \rarr A \end{alignedat} $$

However, we can still extract the types as global definitions for readability:

$$ \newcommand{\Unit}[0]{\texttt{Unit}} \newcommand{\Bool}[0]{\texttt{Bool}} \begin{alignedat}{2} &\Unit&&=\texttt{Rec} \{ \} \\ \space &\Bool&&=\texttt{Sum} \{ \texttt{true}: \Unit \mid \texttt{false}: \Unit \} \\ \space &\texttt{not}&&:\Bool \rarr \Bool \\ \space &\texttt{ifThenElse}&&:\forall A: \Bool \rarr A \rarr A \rarr A \end{alignedat} $$

Universal quantification should also support generalizing over a part of the records (in other words, row-polymorphism), like:

$$ \newcommand{\xx}[0]{\texttt{X}} \newcommand{\T}[0]{\texttt{Rec} \{\xx:A, ...=r\}} \begin{alignedat}{2} &\texttt{getX}&&:\forall A: \T \rarr A \\ \space &\texttt{getX}&&=\lambda s. (s.\xx) \\ \space &\texttt{setX}&&:\forall A: \T \rarr A \rarr \T \\ \space &\texttt{setX}&&= [\text{syntax undecided yet}] \end{alignedat} $$

Existing row-polymorphism implementation divides into two groups according to how they support such generalization, either by qualifying records/variants with constraints, or by introducing a standalone "row" (the type of $r$ above) kind and put all the magic into the new kind.

The study on extensible records has a long history, but there isn't much research and implementations on the combination of bidirectional type-checking and row-polymorphism yet.
Currently, there are some programming languages, such as MLPolyR (there's a language spec, a paper first-class cases, a PhD thesis type-safe extensible programming and an IntelliJ plugin) or Rose, whose case-split are first class (in the papers it's called "first-class cases").

Row polymorphism is useful because it solves the expression problem at language level, which means that library authors can split the library features into several sub-libraries -- one core library with many extensions. Library users can combine the core with extensions they want like a Jigsaw and exclude everything else (to avoid unwanted dependencies) or create their own extensions without touching the original codebase.

Extensible variant type is also useful for simulating exception-handling.

Implementation

Voile's implementation is inspired from Agda, mlang and its prototype, minitt. The language design has been influenced by the Trex Haskell extension.

About the name, Voile

This name is inspired from a friend whose username is Voile (or Voileexperiments). However, this is also the name of a library in the Scarlet Devil Mansion.

The librarian of Voile, the Magic Library

Modules

check	Type-Checking module.
syntax	Abstract syntax, surface syntax, parser and well-typed terms (core language).
util	Tool functions.

Macros

define_parse_str
next_rule
tik_tok