Lib.rs

The Quail Language

• Introduction
• Getting Started
• Basics
• Vim Highlighting

Introduction

Quail is a programming inspired by Haskell, Idris, and Elm. It aims to explore the potential of language design when no compromises are made against the fundamental notions of purity and totality.

Purity is the idea that the evaluation of an expression never produces any side-effect observable to the runtime. In Quail, all expressions represent constant values. A variable, once defined, will never change its value, and so may always be substituted for its definition. Purity demands that the author be disciplined about the flow of data in his code. And dually, the maintainer is freed from worrying about non-local behavior of a program.

Totality is the idea that evaluating any expression eventually results in a value of the expected type. In Quail, match statements must cover all possible cases. There is no notion of exceptions. Programs must not get stuck in infinite loops. Recursion must always be well-founded. Totality allows Quail to avoid the need for a preferred evaluation order (eg, strict vs lazy). It also permits a meaningful distinction between inductive data (such as lists) and coinductive data (such as streams).

Quail is meant to be a beginner-friendly language. Because of their academic origins, functional programming languages have a reputation for being esoteric and difficult to learn. This is unfortunate because the advantages of functional programming are afforded by the basic ideas, such as strong typing, immutability, pattern-matching, and the overall principled design of the lambda calculus. Quail designed to be minimal, elegant, and above all else, easy to learn.

Getting started

To get started, clone the repository, then run one of the example programs:

$ git clone https://github.com/tac-tics/quail
$ cd quail
$ cargo run --release examples/primes.ql
Finished dev [unoptimized + debuginfo] target(s) in 0.02s
     Running `target/debug/quail examples/primes.ql`
     2
     3
     5
     7
     11
     13

Basics

The most basic type in Quail is Nat, short for natural number. Nats are constructed through the constructors zero and succ. The number zero should be familiar to you. The function succ is short for "successor". It means "one more than", and since it is a function, it must be applied to another Nat. So the number one can be expressed as succ zero. And the number two can be expressed as succ (succ zero).

Every natural number can be expressed this way. There are no number literals, so you can't write something like 3. Instead, you have to construct the number you want explicitly: succ (succ (succ zero)).

When you want to print a number to the screen, you can use the builtin show function, which turns a Nat into a Str, and the println function, which prints a Str to the screen.

Here is a short program in Quail to get started with Nats:

# tutorial.ql
def main : Top = println (show (succ (succ (succ zero))))

You can save this to the file tutorial.ql and then run it like this:

$ quail tutorial.ql
3

And you see the number 3 was printed to the console.

You can define a variable using the def keyword. So perhaps we want to define the first few naturals so we don't have to type them over and over again:

# tutorial.ql
def one : Nat = succ zero
def two : Nat = succ one
def three : Nat = succ two

def main : Top = println (show three)

Saving and running it again will show the same result.

Notice that one, two, and three all have : Nat written after them. The syntax : is pronounced "has the type". So when we write def three : Nat = ..., we are defining a new variable three which has the type Nat. In Quail, all top level definitions must be annotated with their type.

To make decisions in Quail, we use match statements. A match statement will look at a value we give it and then determine what action to take from there. For instance, if we want to see if a number is zero or not, we can write this:

# tutorial.ql
def one : Nat = succ zero
def two : Nat = succ one
def three : Nat = succ two

def main : Top = match three
    with zero => println "is zero"
    with succ n => println "is not zero"

Underneath the match statement, we have two lines that start with the keyword with. The with keyword is always followed by a pattern, and the pattern is what we are trying to match against. Lastly, we have a fat arrow => followed by the expression we want in the case of a match.

The first with clause says, "when we match with zero, print is zero to the screen". The other says "when we match with succ, print is not zero to the screen". The variable n after succ is not used in this example, but it is there to tell us that the pattern match creates a new variable n which would tell us what Nat you need to call succ on to get three, the value we're matching against.

One funny thing about Quail is that while zero and succ are built into the language, the familiar operation of addition is not. In order to perform addition, we must first define it. The way we do that is by using match togethr with a technique known as recursion:

# tutorial.ql
def one : Nat = succ zero
def two : Nat = succ one
def three : Nat = succ two

def add : Nat -> Nat -> Nat =
     fun n m => match n
        with zero => m
        with succ n' => succ (add n' m)

def main : Top = println (show (add two three))

Here, we have defined a new function add. You can see it has type Nat -> Nat -> Nat, meaning that it takes two Nats as arguments and returns a Nat as a result. It is defined as a function using the fun keyword and we name its two arguments n and m respectively.

Once we have taken the two numbers as inputs, we proceed by matching on n. This allows us to break n apart and look at the pieces. We can then think about how addition would work in either of the two cases that make up Nat: zero and succ.

When n matches with zero, we think about what the value of add zero m should be. That seems easy enough: adding zero to anything should just give us that thing unchanged. And so we have with zero => m telling us exactly that.

The next line is a little more difficult. First, when we match n against the pattern succ n', we get a new variable to work with: n'. Because we are matching n with succ n', these two expressions are equal: n = succ n'. If you think about this for a moment, that means that n' is the number one smaller than n.

Lastly, we make a recursive call to add. This means that add is going to be defined in terms of itself. You might think that this creates a kind of circular logic. But as long as we are careful, we can avoid any true circularity. We call add with the argument n' and m, and since n' is always going to be smaller than n, the repeated calls to add will eventually bring n down to zero, and our recursion will terminate.

You can see more examples of the Nat in nat.ql.

Vim Highlighting

If you use vim, you can install the syntax highlighting like this:

$ cp -r quail.vim/ ~/.vim/bundle/