(version: development)

2 Architecture of Cedille

Cedille is implemented in around 13kloc of elisp + Agda. There is an emacs Cedille mode for reading and writing Cedille code using unicode shortcuts. Most importantly, from Cedille mode one can request that the Cedille backend process the current Cedille source buffer, and enter Cedille navigation mode. In Cedille navigation mode, a rich amount of type information computed from the backend is available and can be viewed node by node of the abstract syntax tree for the text of the buffer. One navigates this tree using individual keystrokes (in Cedille navigation mode) like p and n. One can also issue interactive commands, even use a beta-reduction explorer. See cedille mode commands There are several extra buffers available to display information about the current node (the inspect buffer), current typing context, meta-variable solutions, and summary information for the source file.

Additionally, one can request that Cedille elaborate a given source buffer and its dependencies to Cedille Core, a much more minimalistic core type theory lacking many of the nice features of Cedille, especially spine-local type inference. core contains an implementation of Cedille Core in Haskell. There is a specification of Cedille Core here. To elaborate a source file and its dependencies, use keystroke “E” in Cedille navigation mode. You will be prompted for the name of a directory into which to store the elaborated files. These are written as .cdle files. Opening a .cdle file in emacs (with Cedille installed) will initiate a cdle emacs mode, whose main purpose is to support typing “Meta-s” to check the cdle file with the Cedille Core checker. At present, the elaborated files are rather big and generally will not be checkable all at once in regular Cedille. Cedille Core is a subset of Cedille, though, and so you can check selections from these files directly in Cedille (not just in Cedille Core).

2.1 Spans

The frontend (i.e., the emacs mode) sends request to the backend in a simple text format. The backend replies with spans, which consist of a starting and ending character position in the file, a name for the node, and a list of attribute-value pairs. The inspect buffer, which one views with keystroke i when a span is highlighted (with p), shows this information. Some of the attribute-value pairs are suppressed by default, because they are intended just for use by the frontend. You can see them if you wish by changing the setting of the Cedille Mode Debug customization variable; to do this, use keystroke $ from Cedille navigation mode to see customization options, or do customize-group cedille.

Spans for file F are cached in a F.cede file written to a .cedille subdirectory of F’s directory. Spans are stored and transmitted to the frontend in JSON format. Hence, one can easily read the span data directly – but you will find that it is very verbose and much easier to understand through the emacs mode.

The se-mode (“structured editing”, though it is really just structured navigation) part of the elisp code is concerned with processing the spans and assembly an abstract syntax tree based on span containment. se-mode is generic, and can be used as the basis for structured navigation for other languages. se-mode was proposed, designed, and implemented by (then) U. Iowa undergraduate Carl Olson, before the current Cedille implementation began.

2.2 Spine-local type inference

Cedille implements a novel form of local type inference due to Chris Jenkins, called spine-local type inference. Cedille will try to fill in omitted values for type variables via first-order matching (not unification). There is currently some heuristic support for second-order matching, but a complete second-order matcher (note that second-order matching is decidable, unlike second-order unification) is planned for after the 1.0 release. The inference is local in the sense that type meta-variables are never propagated out of a locale, which is an application spine (i.e., head applied to arguments). Spine-local type inference also uses the expected type for a locale to fill in missing values for type variables used in the type of the locale. For more information, see the paper on ArXiv. See also some examples in language-overview/type-inference.ced. When in Cedille navigation mode, use keystroke m to view the meta-variables buffer, where information on meta-variables and their current solutions (if any) is shown; when this buffer is shown, the locale will also be highlighted in the Cedille source buffer.

2.3 File structure and modules

A Cedille source file consists first of a header consisting of optional module imports (import X.), then a module declaration for the file (module X(params)), and then more optional imports. The parameters can be term- or type-level, and one can indicate erased term-level parameters with curly braces. For an example of a module parametrized by a type of natural numbers mod 2:

module X(A : ★)(z : A)(s : A ➔ A){p : { z ≃ s (s z) }} .

After the header, the file consists of term, type, or kind definitions.

Modules may be partially applied.