Tao: A statically-typed functional language

Asking as a complete newbie in this paradigm, but what's the benefit of writing factorial like this?

    fn factorial = 
        | 0 => 1
        \ y ~ x + 1 => y * factorial(x)

Instead of

        | y => y * factorial(y-1)?

Subtraction of natural numbers is non-total, and can result in negative numbers, which cannot be represented as a natural number. Most languages throw an exception, panic, etc. None of these are solutions I'm happy with.

In Tao, natural numbers don't support subtraction but you can decrement them by pattern-matching as in this example, allowing the compiler to 'check your workings' and statically prove that your program can never result in underflows.

In a similar vein, you can't index directly into a list (because indexing is a fallible operation). Instead, you must pattern-match on the list and explicitly handle the empty case (you can also write a utility function to do this for you like so)

    fn nth : Nat -> [A] -> Maybe A =
        | _, [] => None
        | 0, [x ..] => Just x
        \ n + 1, [.. tail] => tail->nth(n)

Used like:

    [1, 2, 3]->nth(1) # Evaluates to `Some 2`

> Tao or Dao is the natural order of the universe whose character one's intuition must discern to realize the potential for individual wisdom

It echoes how I feel when I write programs in languages with strong static type systems: that of the compiler almost fatalistically leading me towards a solution that naturally fits the problem space. A metaphor I like to use is that of an artist knocking away pieces of marble to reveal the statue that was always there beneath.

And, yes, it's great fun to work on! Everybody should give writing a compiler and designing a language a try!

A typeclass (or in Rust, a trait) is something that describes a set of behaviours that must be implemented by a type (in OOP languages, abstract classes are broadly equivalent).

For example, the typeclass `Eq` describes how values of a type might be compared for equality.

    class Eq =
        => eq : Self -> Self -> Bool

The typeclass requires that types conforming to it provide a function, `eq`, that takes two instances of itself and returns a bool (indicating whether the instances are equal). And member of this typeclass might look like:

    for A, B member (A, B) of Eq where
        A  eq = fn (a0, b0), (b0, b1) => a0 == a1 && b0 == b1

You can read this as "for any two types, A and B, a tuple of both can also be compared for equality provided both A and B can themselves be compared for equality"

Typeclasses become useful because they allow you to constrain generic type parameters. For example, we can now write a function that determines whether a list contains a matching value:

    fn contains A : A -> [A] -> Bool where
        A  False
        \ k, [x .. xs] => x == k || xs->contains(k)

All of this is checked at compile-time by the compiler, ensuring that the function can only be called with types that can be compared for equality.

Nice work on the README. Gets right to the point about what it look likes and what the goals are.