Tao: A statically-typed functional language
github.com
github.com
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.
The thing I loved about golang was that it’s just “good enough” in lots of areas instead of being the best or perfect. That allowed more time ti works on other parts of an ecosystem.
But since Tao is an hobby project, i just hope the author goes nuts and enjoy working on all those things. It is indeed a cool lang.
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.
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...)
fn show_negative A : A -> Str where
A < Neg,
A.Output < Neg,
A.Output.Output < Neg,
A.Output.Output.Output < Neg,
A.Output.Output.Output.Output < Show,
=
a => (----a)->show
In terms of implementation, the function is quite simple: it just negates the input value a bunch of time and then `show`s it as a string using the `Show` typeclass (equivalent to Haskell's `show`: https://hackage.haskell.org/package/base-4.16.1.0/docs/Prelu...).
Arithmetic operations such as negation are defined using typeclasses. Here's the definition of `Neg`:
class Neg =
=> Output
=> neg : Self -> Self.Output
member Nat of Neg =
=> Output = Int
=> neg = fn x => (implementation omitted because it's a built-in intrinsic)
The `where` clauses on the `show_negative` just constrains the output type of negating the `A` in such a way that its output type is also constrained, in a chain, with the final type in the chain being `show`-able.
Seems very ML/Haskell inspired.
All tuples seem to require parenthesis.
Definitely not ergonomic on a qwertz layout (Altough, what language is?)
No current plans for an interactive/repl version it seems
No dependant types either.
Overall, pretty interesting. Definitely warrants a closer look.
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
https://docs.microsoft.com/en-us/dotnet/fsharp/language-refe...
You're funny
Best of luck. Dhall is a current language with totality, but it runs into impossibly high memory requirements as a result. We had CI workers with 16 GB RAM run into out-of-memory issues because of the sheer size of the totally expanded type space (sum types of types which are themselves sum types of types which are themselves sum types etc... Exponential growth is easy).
I appreciate that this is scoped as a hobby project for now, not recommended for production, so like I said, best of luck :)
Totality shouldn't have any special impact on memory usage as far as I know. It just restricts the kind of recursive functions and data types you can write.
Can someone explain?
For example, the typeclass `Eq` describes how values of a type might be compared for equality.
class Eq =
=> eq : Self -> Self -> Bool
for A, B member (A, B) of Eq where
A < Eq,
B < Eq,
=
=> eq = fn (a0, b0), (b0, b1) => a0 == a1 && b0 == b1
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)
So, the typeclass itself is like an interface, but rather than having classes that implement that interface directly, you have typeclass instances which are like an adapter between a value (struct) and the interface - or like a virtual function table. You know how a class instance is essentially a struct + a (pointer to a) virtual function table? Imagine making those two pieces more distinct in code - the typeclass instance is the stanadlone virtual function table.
So your object state is more exposed - you can't really have private fields in this paradigm since your state is just a struct value. But it's clearer what's what, and it's much easier to adapt types to interfaces even when the authors didn't know about each other, since the typeclass instance can be defined separately from both the typeclass and the value type (although there are possible inference problems with this). So lots of secondary cross-cutting functionality problems where OO languages tend to end up with an ad-hoc type registry (e.g. serialization or database mapping - just look at what projects like jackson-datatype-joda or joda-time-hibernate have to do to get themselves registered) are easier to solve in this model.
fn factorial =
| 0 => 1
\ y ~ x + 1 => y * factorial(x)
| y => y * factorial(y-1)?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)
[1, 2, 3]->nth(1) # Evaluates to `Some 2`I was not completely clear on your definition of totality. But I am all for not Turing-complete models of computation that still do useful things.
I go a bit dissappointed with Haskell, but right now I'm reading Tao's README and this looks like everything I've ever wanted ! I'm gonna try it out right now.
a) doing a `front page` type thing laid out like the why-Koka page for the Koka language [1]. (essentially a brief section about each foundational theoretical aspect) Then having links put in for more theoretical/formal information as I write it up.
b) just doing narrative style ‘blog’ post writings about whatever concepts people may want to hear about.
I’m leaning towards option A, but without quite such a strong emphasis on how to use the language and more focus on what the language is. But if you think it would be more informative to just read randomly connected blogs let me know. I’ve never done this before so I don’t have a clue what other people find interesting.
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.
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...
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...
As a side effect, it might also be a good way to keep your compile times down.
Is the namesake "tao" meaning "the way"? Or perchance a nod to Terry Tao?
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!
There is no module system yet (only a temporary C-like #include system): that's on my list of things to work on!