Crate voile

Voile is a dependently-typed programming language evolved from minitt.

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

We're pretty much inspired by the coexistence of guarded recursion, coinductive data types, sized types and inductive types in Agda, which is nice to have all of them but they do not work very well as we can see in a discussion here about guarded recursion checker or in a GitHub issue about the incompatibility between size and guarded recursion. We can observe that sums, records, and (dependent) pattern matching in Agda only work well when being top-level bindings.

Features

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

Extensible ADTs

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

First-class record support is known as Record Calculus, or Row Polymorphism, 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. In other words, the "record type" itself is a kind of expression.

The study on extensible records has a long history.

However, there isn't much research and implementations on extensible sums yet. Extensible sums are quite complicated because it probably requires:

• First-class pattern matching
• Subtyping on Sums

While currently, I can only find one programming language, MLPolyR (there's a language spec, a paper first-class cases, a PhD thesis type-safe extensible programming and an IntelliJ plugin), whose pattern matching is first-class (in the papers it's called "first-class cases").

It is quite obvious that sums and records are dual to each other -- destructing a sum requires listing all the cases and so does constructing a record; constructing a sum only need one element to be mentioned and so does projecting a record element as well. The name, product and coproduct also expresses such duality. Duality is a very nice property to have because it implies similar implementations.

Since first-class pattern matching solves the expression for free, we can split our feature into several libraries -- one core with many extensions. Library users can combine the extensions they want like a Jigsaw and exclude everything else (to avoid unwanted dependencies) or create their own extensions without touching the original codebase.

Exceptions (undecided yet)

MLPolyR exploits first-class sums in error-handling -- exceptions are treated as first-class sums while try-catch clauses are pattern matching on them ("consumes" a variant in a sum). This is like Java's checked exceptions, but with full type-inference. However, without the help of dependent types, there can be false positives such as conditional exceptions -- consider a function f like this:

fun f a = if a then throw bla else 0

Invoking it with f false will still enrage the compiler, treating this expression as exception-throwing. In the industry of dependent types, there isn't much development on exceptions. We might have a try here.

Induction and Coinduction

According to elementary-school discrete math, induction has something to do with recursion. However, recursion on sum types is a huge problem against the design of first-class sum types.

In the cliché programming languages with non-first-class sums (where the sum types need to be declared globally before usage), type-checking against recursive sums can be easily supported because the types are known to the type-checker -- there's no need of reduction on an already-resolved sum type. Once a term is known to be some sum type, it becomes a canonical value.

For Voile, arbitrary expressions can appear inside of a sum type term, which means reduction is still needed before checking some other terms against this sum-type-term. If there's recursion on a sum-type-term, like the natural number definition:

Nat = 'Zero | 'Suc Nat

The type-checker will infinitely loop on its reduction.

The above definition will actually be rejected by the termination checker, but recursion on sum-types have to be supported because we have been using it for a long time -- we shouldn't sacrifice this fundamental language feature.

TODO This chapter is not finished.

Implementation

Voile's implementation is inspired from Agda, mlang, MiniAgda and its prototype, minitt.

MiniAgda supports induction, coinduction with sized types.

TODO Something needs to be written here.

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

Macros

define_parse_str
next_rule
tik_tok