zesterer

I think it was "value judgement" (dependent types allow dispatching over a value in the type system)

Rust gives each closure a unique type (see the `Fn` trait: https://doc.rust-lang.org/core/ops/trait.Fn.html), allowing the compiler to always statically dispatch to the exact function body at compile-time. That said, this is a rather more explicit approach that won't necessarily fit everything.

So... I want to preface this by saying that I'm very, very far from being an expert on this topic. Although Tao's compiler has a MIR optimiser, it only covers the basics (inlining, constant folding + symbolic execution, etc.).

I think one of the main reasons that Haskell failed to solve this is actually the same reason that many lower level languages failed: it places too many requirements on data representation. In the case of C/C++ and even (to a lesser extent) modern languages like Rust and Swift, this is because they make promises about representation to the programmer that allow you to circumvent aspects of the language and still write correct code: be it transmutation, casting, field offsets, etc. In the case of Haskell, lists have an entirely arbitrary length and the language makes no effort to constrain this requirement in the type system, meaning that the compiler can only speculatively optimise a list into an unboxed array. In a language with dependent types, it should be possible to constrain the size of a list with the type system, allowing the optimiser to do its job without need for speculative whole-program analysis.

The other reason Haskell doesn't quite succeed is monomorphisation (or lack thereof). Haskell's support for first-class higher-ranked types means that the language can't feasibly make promises about monomorphisation, and as a result it needs to revert to boxing and dynamic dispatch far more than it really should. Conversely, Tao is designed to monomorphise in all cases from the start.

Rust demonstrates that functional programming (and in particular, programming with higher-order functions) is more than possible to optimise very well, and it does this by promising monomorphisation through the type system, allowing the compiler to aggressively perform static dispatch and inlining.

From what I've seen, GHC also fails to pick a lot of low-hanging fruit. The last time I checked (perhaps this has since changed) GHC often struggles with things like TCO and inlining in relatively simple cases as a byproduct of its design (all functions are dynamically dispatched by default, with inlining being a speculative optimisation).

I need to do a little more writing about exactly what ideas I have for Tao, but other languages of similar ilk demonstrate that Haskell is very far from the pinnacle of what is possible (for example, Koka's Perceus reference reuse: https://koka-lang.github.io/koka/doc/book.html#why-perceus).

They are made by a Rust library, but it's a library I wrote for this project (now used by others too): https://github.com/zesterer/ariadne

Thanks!

Go for it! IIRC it was suggested by someone else in the #langdev channel on the Rust Community Discord, so I can't claim to own the idea.

Good luck! Feel free to open a discussion topic or issue if you have any questions!

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,
        B < Eq,
    =
        => 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 < Eq,
    =
        | _, [] => 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.

> 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!

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`

Fast enough for this approach to work for small examples. For longer examples, I'm less confident: I've yet to implement a proper module system (other than a slightly more principled version of C's #include) so this currently means compiling the entire standard library on every REPL line. Thankfully, the compiler can still handle this within about 100 milliseconds on my machine. Perhaps when I have a more rugged module system I can look into this more, thanks for the suggestion!

> Curious how Tao is pushing the limits on that front?

I don't want to put emphasis on "pushing the limits" because I'm still very new to language design and mostly self-taught. There are bigger and better languages pushing the envelope further than Tao!

That said, I've been experimenting with:

- Expressing totality and type inhabitance in the type system

- Effect systems (including user-defined effects, effect handling, parametric effects, lowering to monadic IO, etc.)

- Typeclass inference via typeclass variables (Tao can handle several cases that are ambiguous even in Rust, such as the following: https://github.com/zesterer/tao/blob/master/examples/debug.t...)

Thanks for your kind words :)

In a previous revision of the language, I did! (https://github.com/zesterer/tao/tree/old). I decided against it because, in short, I find the trailing delimiters to be quite ugly.

Because this is purely a personal project, I'm thankfully not constrained by such mundane concerns as "ergonomics" (unless such concerns relate to me while I'm working with it). I think Pythonic syntax is probably the way to go long-term though...

Yes! As you say, the do notation + monads covers this, but I'm planning to remove it in favour of a slightly more general 'effect basin' syntax that I'm currently working on (syntactically similar to Rust's async + await, but generalised to all effectful operations like mutation, IO, etc.). Example here: https://github.com/zesterer/tao/blob/master/examples/mutate....

Iosevka Fixed Slab Semibold

Yes. This is something I've been thinking about a lot, as it happens! In particular, one of the great benefits of pure languages from an optimisation standpoint is that unused values can always be optimised away, but this is not the case if we treat termination (or non-termination) as a side effect! For now, I'm treating it as not being a side-effect (as does C++, although C++ goes a step further and treats it as straight-up UB in certain conditions). This is something I've still yet to nail down semantically.

Pretty much!

The language does support limited sugar for tuples without parentheses in some specific cases, such as `match` and `let`:

    let x, y = 5, 4 in
    ...

    match x, y in
        | 4, 7 => None
        \ _, y => Just y

However, these cases only incidentally lower to tuple pattern matching, and deliberately hide the fact that tuples are used internally.

They're more akin to 'destructuring' natural numbers into successors. Consider:

data Nat = Zero | Succ Nat

You could pattern match on this Nat, fetching the inner Nat, allowing the type system to prove that all cases are handled exhaustively. Arithmetic patterns just extend this notion to the built-in Nat type.

Full dependent typing is something I'd like to experiment with in time, but I'm not there yet.

For now, just total (i.e: functions can't panic, throw exceptions, etc.). I'd like to explore termination analysis in the future though!

Hey, author here. I definitely didn't expect to see Tao on Hacker News. As is probably obvious, the language is extremely early in its life, and it's not practical to write anything but trivial examples in it yet. Please don't judge!

REPLs are often difficult to reconcile with AoT compilation and static analysis, particularly in the context of things like type inference (at least, in a way that preserves semantics). It's on my mental todo list, but not a priority for me.

Tao isn't indentation-sensitive, so nested `match` expressions are ambiguous without the trailing \ branch.

I don't know whether I'll keep this syntax though. I'm increasingly wondering whether it's better to just bite the bullet and go all in with indentation sensitivity.

That said, the existing \ syntax can be quite nice to read: https://github.com/zesterer/tao/blob/master/lib/parse.tao#L5...

I am indeed "going nuts"!

As mentioned in the README, I don't see Tao as a production-quality language (at least, for the foreseeable future). I'll leave that to the experts. Instead, I'm more interested in exploring the limits of new language design ideas (effect systems in particular). There are already a few interesting things Tao does that I've not seen elsewhere.

Channels are most definitely not easy to reason about in the slightest. Superficially, they might appear to be on the surface: but they're really not and have innumerable subtle cases and behaviours in the face of various kinds external conditions, scheduling behaviours, etc. They only start to become 'easy' in a language that utterly ignores all other paradigms, interoperability, and performance concerns as in Go.

I have some thoughts about this: https://github.com/zesterer/chumsky/issues/20#issuecomment-9...

TL;DR: The best approach, in my view, is to detect whitespace in the lexer and emit fake delimiter tokens for the parser so that the parser-level syntax is still context-free.

As the author of the library, I'd like to note that I consider some of Chomsky's views to be... questionable. The choice of name was largely down to his work in the world of linguistics and parser theory.

My advice has always been: 'Write at least one parser by hand before using parser combinators. Then, never write parsers by hand ever again'.

I've been developing both throughout the development of Tao, my own hobby language. It's since developed quite an extensive syntax (see here for an example: https://github.com/zesterer/tao/blob/master/examples/99.tao), so you can count it as evidence that chumsky scales to complex grammars: https://github.com/zesterer/tao

The main points of focus for chumsky, beyond nom, are:

- Ease of use + ergonomics

- Backtracking 'by default'

- High quality errors and error recovery

Nom is very specifically designed for parsing input not intended to be read by humans, and that focus is evident in the things is prioritises.