The Quail Language
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.
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
The most basic type in Quail is
Nat, short for natural number.
Nats are constructed through the
succ. The number
zero should be familiar to you. The function
short for "successor". It means "one more than", and since it is a function, it must be applied to
Nat. So the number one can be expressed as
succ zero. And the number two can be
succ (succ zero).
Every natural number can be expressed this way. There are no number literals, so you can't write
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
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
# 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.
three all have
: Nat written after them. The syntax
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
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"
match statement, we have two lines that start with the keyword
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
is zero to the screen". The other
says "when we match with
is not zero to the screen". The variable
is not used in this example, but it is there to tell us that the pattern match creates a new
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
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
fun keyword and we name its two arguments
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
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
succ n', these two
expressions are equal:
n = succ n'. If you think about this for a moment, that means that
the number one smaller than
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
m, and since
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.
If you use vim, you can install the syntax highlighting like this:
$ cp -r quail.vim/ ~/.vim/bundle/