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!
Cheers to you, and I hope you're learning and having fun working on your project!
This is the first I've seen in a while where I think the offering hits a spot on the tradeoff continuum that is distinctive and where I can picture many circumstances where I would want to use this language (the soundness aspect is a big part of that).
Curious about plans for this. When Haskell use exploded I followed a lot of the blogs talking about it someday being faster than C because purity made compiler reasoning easier and stream fusion and other things were going to change the world, but as time went on idiomatic Haskell never came even close to C. Now having a lot of performance experience I think a major factor is that functional languages insist on using lists for everything, which map poorly to hardware. Looking at your screenshots, it looks like it still employs the list paradigm.
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).
Could you please point me to other approaches to inlining? I am also working on a personal language and it could be helpful.
Some specific questions about the language design: - Does your flavor of algebraic effects allow distinct effects of the same type (e.g. two separate int-valued `State`s)? I haven't seen anyone talk about this, but it seems like a potential problem with effects.
- Do you have plans for making pattern matching extensible? I've thought a lot about how this could be possible with optics (the FP construction), but haven't found a nice solution yet.
Could you give an example of what you mean by this? Multiple effects can be combined together (although I'm still working on handlers for multiple effects), for example:
effect console = input + print
fn greet_user : console ~ () = {
print("Please enter your name:")!;
let name = input!;
print("Hello, " ++ name)!;
}
I have no plans as of yet. Extensible pattern-matching seems to me to be quite hard to unify with exhaustivity. Tao supports most of the patterns that Rust/Haskell supports.
A more practical example would be having two state-like effects for use as different allocation/deallocation strategies.
# Define a new effect that yields to the caller
effect yield A = A => ()
# A generator that emits numbers
def one_two_three : yield Nat ~ () = {
yield(1)!;
yield(2)!;
yield(3)!;
}
# Print the numbers to the console
def main : io ~ () = {
one_two_three
handle yield Nat with n => print(n->show)!
}I mean a type like `yield Nat + yield Nat ~ ()`. Here's how this would occur naturally: Define
effect yield A is A => ()
fn yield_each A, B, e : (A -> e ~ B) -> [A] -> e + yield B ~ () is
| _, [] => ()
\ f, [a .. as] => a->f!->yield!; as->yield_each(f)
fn print_each A, B, e: (A -> e ~ B) -> e + print ~ () is
f, l => l->yield_each(f)
handle yield B with x => print(x->show)!
fn foo : print ~ [Nat] is
[1, 2, 3]->my_map(n => yield(n)!; n+1)
handle yield Nat with n => print("Processing " ++ n->show)!
One question: does numerical destructing require that one of the terms be a constant? What happens if I write y ~ a + b ?
Also:
> In Tao, arg:f is shorthand for f(arg)
Did you mean arg -> f ?
Yes, the general pattern is `n + K`. I'm looking to expanding this to other operations in the future too.
> Did you mean arg -> f ?
Yes. I changed the syntax recently, but forgot to change the README. Thanks for pointing this out!
OK, so what is the intended benefit of y ~ x + 1 over x = y - 1 ?
I can see an obvious benefit if I can write y ~ x + z where neither x nor z is a constant and the resulting semantics invoke some kind of mathematical constraint management system or backtracking search a la Prolog, but if I'm constrained to write things that can be trivially transformed into a binding I don't see the point.