UPDATE: envisioned feature list

[Mesabloo]

Last year, I initiated a topic (see #4) to try and discuss all planned features for the first versions of Zilch.
Initially, it was supposed to record any design progress as well as any thoughts, but it kinda quickly became inactive, and I have been thinking a lot on my own without posting about it.
I feel that the language itself has evolved quite a lot, and needs to be broken down somewhere at some point.
This is the goal of this topic.

All features will be posted in separate comments below, one by one.

[Mesabloo]

The base of the language

Zilch is a functional at core programming language, focused on low-level and performance by integrating a few features from imperative programming.

The surface language

The surface language is basically a λ-calculus extended with let and rec bindings, pattern matching and builtin types such as integers and pointers. There are also other extensions which will be described in separate comments.
Here is an example of a function computing the factorial of a given number, following this definition:

$$n! = \begin{cases*} 1 & if $n = 0$ \\ n \times (n - 1)! & otherwise \end{cases*}$$

rec fact(n : u64) : u64 ≔ 
  if n = 0 then 1 else n × fact(n - 1)

Alternatively, this could also be written

rec fact(n : u64) : u64 ≔
  match n with
    0 ⇒ 1
    _ ⇒ n × fact(n - 1)

Notice the heavy use of Unicode in the source code. It is a good idea to install WinCompose if you are on Windows, or to configure XCompose on Linux (I do not know the alternative for Mac users…sorry).
ASCII alternatives are still provided for the surface syntax, for example := instead of ≔, => instead of ⇒, etc.

Builtin types

• Numeric types:
  • uN and sN (where N is one of 8, 16, 32 and 64) represent unsigned and signed integers;
  • fN (where N is 32 or 64) is the type for floating point numbers of the specified width;
• Text-related types:
  • char is the type for 4 bytes wide characters, without a specified encoding (it may be UTF-8, UTF-32 or even just plain ASCII). Note that for ASCII text, it is better to use s8 or u8 so as not to waste space. char is actually isomorphic to u32;
• Other types:
  • bool is the type of boolean values ⊤ and ⊥;
  • ref(A, ρ) is the type of reference to values of type A in the region ρ;
  • ptr(A, ρ) is the type of pointers to values of type A in the region ρ. Note that using this type is mostly unsafe and should only be used when inter-operating with e.g. C. In such case, ρ can take the special builtin value UNMANAGED, indicating that the memory is allocated outside of a region and hence needs to be freed within the C context (i.e. must be consumed by a foreign call);
  • (@σ x : A) → B(x) is the dependent function type (also called Π-type) with an explicit argument. The argument can also be implicit and should be enclosed within {} instead of () (e.g. {@σ x : A} → B(x));
  • (@σ x : A) ⊗ B(x) is the multiplicative dependent product type (also called Σ-type). Note that a multiplicative product is consumed by consuming both its elements;
  • 𝟏 is the type for the multiplicative unit;
• Type-level types:
  • level is the type of universe levels;
  • type ℓ is the type of type at level ℓ;
  • region is the type of runtime regions (for memory management);
  • effect is the type of algebraic effects;

Currently planned builtin operations (may change)

Some operations will be implemented as primops (meaning directly written in N⋆, but having a special meaning within the compiler itself).

• Low-level primitive operations on integers:
  • +ₙ (where n is 8, 16, 32 or 64) is the addition on (un)signed integers of size n (i.e. +₆₄ : u64 → u64 → u64);
  • -ₙ is subtraction on (un)signed integers of size n;
  • ×ₙ is multiplication on (un)signed integers of size n;
  • ÷ₙ is integer division on (un)signed integers of size n, returning the quotient part;
  • modₙ is integer division on (un)signed integrs of size n, returning the remainder part;
  • &ₙ is the bitwise AND-masking operation on (un)signed integers of size n;
  • |ₙ is the bitwise OR-masking operation on (un)signed integers of size n;
  • ~ₙ is the bitwise negation (two's complement) on (un)signed integers of size n;
  • xorₙ is the bitwise XOR operation on (un)signed integers of size n;
  • shrₙ is the logical right shift on (un)signed integers of size n;
  • shlₙ is the logical left shift on (un)signed integers of size n;
• Low-level primitives operations on floatting-point numbers:
  • +.ₙ (where n is 32 or 64) is the addition on floating points numbers of size n;
  • -.ₙ is the subtraction on floating point numbers of size n;
  • ×.ₙ is the multiplication on floating point numbers of size n;
  • /.ₙ is the division on floating point numbers of size n;
• Operations on booleans:
  • if b then A else B is the destructor for boolean values b, where if ⊤ then A else B ≡ A and if ⊥ then A else B ≡ B;
  • ∧ is the conjunction (AND gate) of two boolean values, such that ⊤ ∧ ⊤ ≡ ⊤ and _ ∧ _ ≡ ⊥;
  • ∨ is the disjunction (OR gate) of two boolean values, such that ⊥ ∨ ⊥ ≡ ⊥ and _ ∨ _ ≡ ⊤;
  • ¬ is the boolean negation (NOT gate) such that ¬ ⊤ ≡ ⊥ and ¬ ⊥ ≡ ⊤;
  • ⊕ is the boolean exclusive disjunction (XOR gate) such that A ⊕ B ≡ A ≠ B;
  • ⟶ is the boolean implication such that ⊤ ⟶ ⊥ ≡ ⊥ and _ ⟶ _ ≡ ⊤ (careful, this is a Long Rightwards Arrow, not a simple Rightwards Arrow as in the type of functions);
  • ⟷ is boolean equivalence such that A ⟷ B ≡ A = B (same here, this is a Long Left Right Arrow);
• Operations on pointers:
  • deref p retrieves the value pointed by p, if p has not been freed yet. Not that unmanaged pointers cannot be dereferenced to prevent any UB related to pointers;

All these operations are builtin because they convey specific information and must be used (and compiled) differently within the type-checker.

[Mesabloo]

Dependent and quantitative types

The type system for Zilch is based on a Dependent Type Theory augmented with multiplicities to get explicit erasure and resource linearity (also known as Quantitative Type Theory, where the resource fragment contains 0, 1 and ω).
Erasure means that some arguments are erased at compile-time and are not present at runtime (e.g. type parameters). Resource linearity means that the object must be linearly threaded into function calls (i.e. the resource must be consumed exactly once).

In Zilch, the syntax for multiplicities is:

• @0 or @erased for an erased item;
• @1 or @linear for a linear runtime resource;
  Note that no syntax is actually provided for unrestricted resources (which would be denoted @ω or @unrestricted).

In the absence of explicit multiplicities, the following multiplicities are assumed:

• For parameters, @ω is the default multiplicity;
• For top-level bindings, @ω is the default multiplicity. Note that in such case, @1 is actually disallowed;
• For local bindings, @1 is the default multiplicity to avoid being able to use resources non-linearly;
• For constructors and record fields, @ω is the default multiplicity;
• For effect handlers, @ω is the default multiplicity.

[Mesabloo]

Semi-automatic memory management with (infered) regions

Regions are a model of memory management which is mostly automatic. In general, it seems to exhibit faster speeds than garbage collectors, and speeds similar to manual memory management, all while having a small runtime footprint.
In such a model, pointers are allocated within specific areas of the memory, which are automatically deallocated (along with the pointers within) when they go out of scope.

In Zilch, regions can either be constructed explicitly using the region construct (see below for an example) or implicitly, in which case the compiler infers the correct placement of region blocks.
An example of explicit region:

let my-fun() : ⟨console⟩ 𝟏 ≔ 
  region ρ 
    let r ≔ make-ref{ρ, u64}(0)
    let () ≔ ref-update(r, 1)
    ()

The newly created region ρ is then deallocated at the end of its scope, thus closely resembling C++'s RAII model.
Note that unlike C++, references and pointers cannot escape their regions. If we were to have written the following code, the compiler would complain:

let my-fun() : ⟨console⟩ ref(u64, _) ≔
  region ρ 
    let r ≔ make-ref{ρ, u64}(0)
    let () ≔ ref-update(r, 1)
    r

In this case, the hole _ in the return type cannot be infered to a valid region, because r's region (namely ρ) goes out of scope.

[Mesabloo]

Algebraic effects

Algebraic effects allow users to dynamically inject code in place of certain function calls, through the notion of “handlers”. A common example of algebraic effects are exceptions, which have been commonly found in high-level programming languages for quite a while.
With algebraic effects, such a mechanism could be implemented as:

effect exn(@0 E : type) ≔ 
  val throw(ex : E) : 𝟏

Various handlers could be defined. Here are the two most common handlers: catch and finally:

• catch handles an exception, may it arise, and provides a value to be used as replacement:

  let catch{@0 A, @0 E, @0 ε}(handler : E → ε A, act : () → ⟨exn(E) | ε⟩ A) : ε A ≔ 
    with exn∷throw(ex) ≔ handler(ex)
    act()

• finally executes an action at the end of the evaluation, even if an exception arose, and rethrows the exception:

  let finally{@0 A, @0 E, @0 ε}(handler : E → ε 𝟏, act : () → ⟨exn(E) | ε⟩ A) : ⟨exn(E) | ε⟩ A ≔ 
    with exn∷throw(ex) ≔ 
      let () ≔ handler(ex)
      exn∷throw(ex)
    act()

Writing handlers is as easy as that, as long as all the potential effects are handled (here, only throw needs to be implemented).

This approach to handling side effects is more fine-grained than what can be found in e.g. Haskell (death to IO and more general monads), and also a lot more composable (monads in Haskell must be composed with monads transformers, which induce a little bit of overhead when unwrapping every layer).

[Mesabloo]

Refinement types

Refinement types are specific kinds of types associating a base type with (a few) acceptation condition.
For example, one can define the type of (64 bits wide) natural numbers as

let @0 nat64 ≔ [x : s64 | x ⩾ 0]

The type [x : s64 | x ⩾ 0] is read as “any value of type u64 which is greater or equal to 0 is of this type”.
One could also define the type of vectors containing exactly five u64 greater than 7 as:

let @0 vec64-7 ≔ [v : vec(u64) | size(v) = 5 ∧ vec-all(λ x. x ⩾ 7, v)]

Although this last type is something that nobody actually wants, it shows that multiple conditions can be specified. Note that in fact, any boolean expression is allowed as the refinement predicate.

Verification condition are automatically generated an discharged (when possible) using standard SMT techniques, so as not to burden the users with actually having to do proofs (which would not necessarily be possible anyway, since Zilch isn't focused on that at all).

[Mesabloo]

Syntax notations

In modern programming languages (and mostly in proof assistants), it is usually common to define some syntactic elements such as custom operators.
In Zilch, an approach similar to proof assistants (e.g. Isabelle) is followed, giving the full power of mixfix notations to the user.

There are several ways to define new notations for custom operations:

• using the notation top-level construct to specify mixfix operators. Here's an example:

  notation "if x then A else B" [10, 10, 10, 30] : expr → expr → expr → expr ≔ builtin∷bool-destruct(b, A, B)

  Here, [10, 10, 10 specifies the individual parsing levels of each hole x, A and B and 30] specifies the parsing level of the overall expression.
  The default parsing level is 90.
• using the infix top-level constructor to define new infix operators along with their associativities:

  infix "+" [30, left] ≔ std∷ops∷Plus∷plus

  If unspecified, no associativity is given to the operator. The default parsing level is 90.

Note that declaring infix operators with notation prevents them from having associativities. It may be a good fit for unassociative infix operators (although infix "..." [...] ≔ ... is faster to type) only.
Also note that infix operators are not restricted to two arguments, and can contain more (which must be specified using _ in an infix notation, e.g. infix "⤙_↣" ≔ directed-graph∷labelled-edge).
And finally, note that type annotations are not allowed for infix constructs, because they are implicitly of type expr → exprⁿ → expr → expr (n being the number of holes inside). If you need more control over what can be passed to it, consider defining a notation instead.

[Mesabloo]

Datatypes, records and dictionary instances

Data in Zilch is structured using two kinds of construct:

• datatypes, also called enum in Rust, are sets of constructors (unreducible functions with extensional equality, i.e. if F x = F y then x = y) which together form some sort of type. For example, here is how one would define linked lists:

  datatype LinkedList(@0 A : type ℓ) ≔ 
    val nil : @0 A → LinkedList(A)
    val cons : {@0 A, @0 ρ} → A → *ρ. LinkedList(A) → LinkedList(A)

  Together with datatype creation, one can also pattern match on constructors. For example, here's how one would define the length of a linked list (using the datatype above):

  rec length{@0 A}(l : LinkedList(A)) : u64 ≔ 
    match l with 
      nil ⇒ 0
      cons(_, xs) ⇒ 1 + length(xs)

  Notice that operations on any A is automatically lifted to &ρ. A, so that the syntax can be uniform and there's no need to dereference a reference. One could write length (deref xs) instead.

• Multiplicative records bundle data together as sets of fields. Here is an example:

  record Range(@0 A : type ℓ) : type ℓ ≔
    constructor from-to-with
    val from : A 
    val to : A 
    val step : (A, A) → A

  Note that there are two ways one can create instances of records: either using a simple let with the constructor specified or an anonymous record @{ x ≔ e } or by using the instance construct, which additionally registers the record instance as a potential type-class instance, meaning that it can be used to fill holes of the form {{_ : ...}} (which are infered dictionary parameters).
  Instance dictionaries are very useful to model overloading of functions such as value equality or ordering. Dictionary arguments are also always given the @ω multiplicity.

[Mesabloo]

Foreign interface

Exporting functions

By default, polymorphic bindings are mangled following the Itanium C++ ABI naming conventions, but monomorphic bindings can be chosen not to be mangled, giving stable names for C interoperability (and all languages which can interoperate with C, such as C++ or Rust).

Importing functions

As for using foreign functions, note that only monomorphic functions can be called (or at least should be accepted by the compiler), so as not to expose the internal value representation.
Depending on the targetted runtime, some types may also not be accepted when importing functions (specifically thinking about references/pointers and such).
Also, functions which do not exist for the current platform (i.e. are not defined or imported) must provoke errors during compile-time.
Note that it is better for imported functions to have predictable and stable names, to minimize the necessary maintenance.