https://github.com/zesterer/tao Skip to content Sign up * Product + Features + Mobile + Actions + Codespaces + Copilot + Packages + Security + Code review + Issues + Integrations + GitHub Sponsors + Customer stories * Team * Enterprise * Explore + Explore GitHub + Learn and contribute + Topics + Collections + Trending + Skills + GitHub Sponsors + Open source guides + Connect with others + The ReadME Project + Events + Community forum + GitHub Education + GitHub Stars program * Marketplace * Pricing + Plans + Compare plans + Contact Sales + Education [ ] * # In this repository All GitHub | Jump to | * No suggested jump to results * # In this repository All GitHub | Jump to | * # In this user All GitHub | Jump to | * # In this repository All GitHub | Jump to | Sign in Sign up {{ message }} zesterer / tao Public * Notifications * Fork 15 * Star 512 A statically-typed functional language with generics, typeclasses, sum types, pattern-matching, first-class functions, currying, algebraic effects, associated types, good diagnostics, etc. 512 stars 15 forks Star Notifications * Code * Issues 4 * Pull requests 2 * Actions * Projects 0 * Wiki * Security * Insights More * Code * Issues * Pull requests * Actions * Projects * Wiki * Security * Insights zesterer/tao This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository. master Switch branches/tags [ ] Branches Tags Could not load branches Nothing to show {{ refName }} default View all branches Could not load tags Nothing to show {{ refName }} default View all tags 7 branches 0 tags Code Latest commit @zesterer zesterer Added support for multi-effect handlers (changes still required!) ... f52cfbe Jul 5, 2022 Added support for multi-effect handlers (changes still required!) f52cfbe Git stats * 318 commits Files Permalink Failed to load latest commit information. Type Name Latest commit message Commit time analysis Added support for multi-effect handlers (changes still required!) Jul 5, 2022 compiler Changed import system to use relative paths Apr 28, 2022 examples Added support for multi-effect handlers (changes still required!) Jul 5, 2022 lib Added support for multi-effect handlers (changes still required!) Jul 5, 2022 middle Added support for multi-effect handlers (changes still required!) Jul 5, 2022 misc Updated README examples Jul 5, 2022 syntax Added support for multi-effect handlers (changes still required!) Jul 5, 2022 util Allow implied members to specify a real member Apr 8, 2022 vm Added support for multi-effect handlers (changes still required!) Jul 5, 2022 .gitignore Add JetBrains directory to .gitignore Feb 25, 2022 .gitmodules Fix submodule url May 25, 2020 Cargo.lock Allow implied members to specify a real member Apr 8, 2022 Cargo.toml Allow implied members to specify a real member Apr 8, 2022 README.md Updated README examples Jul 5, 2022 rust-toolchain.toml Made Eq a lang item Mar 22, 2022 View code [ ] Tao Goals Features Current working on Planned features Interesting features Arithmetic patterns All functions are lambdas and permit pattern matching Exhaustive pattern matching Very few delimiters, but whitespace isn't semantic Currying and prefix calling Useful, user-friendly error diagnostics Commands Compiler arguments README.md Tao A statically-typed functional language with polymorphism, typeclasses, sum types, pattern-matching, first-class functions, currying, good diagnostics, and much more! Demo of Tao's features For more example programs, see... * examples/hello.tao: Hello world in Tao * examples/adventure.tao: A text adventure game written in Tao * examples/brainfuck.tao: A brainfuck interpreter written in Tao Goals Right now, Tao is a hobby project and I have no plans to turn it into a production-worthy language. This may change as the project evolves, but I'd rather spend as much time experimenting with new language features for now. That said, I do have a few goals for the language itself: * Totality + All programs must explicitly handle all inputs. There are no mechanisms for panicking, exceptions, etc. The goal is to build a type system that's expressive enough to prove the totality of a wide range of programs. + In time, I'd like to see the language develop support for termination analysis techniques like Walther recursion. * Extreme optimisation + A rather dogged and obnoxious opinion of mine is that the 'optimisation ceiling' for statically-typed, total functional programming languages is significantly higher than traditional imperative languages with comparably weak type systems. I want Tao to be a practical example of this that I can point to rather than deploying nebulous talking points about invariants. + I've deliberately made sure that the core MIR of Tao has a very small surface area, making it amenable to a variety of optimisations and static analyses. * Learning + I have only a high-school knowledge of mathematics. I want to use Tao as a test bench to help me learn more about mathematics, proofs, type systems, logic, and computation. + In addition, I hope that Tao can serve as a useful tool for others looking to get into language design, compiler development, or simply functional programming in general. Features * [*] Hindley-Milner type inference * [*] Useful error messages * [*] Algebraic data types + [*] Sum types + [*] Record types + [*] Generic data types + [*] Nominal aliases (i.e: data Metres = Real) * [*] Type aliases * [*] Type polymorphism via generics + [*] Class constraints + [*] Associated type equality constraints + [*] Arbitrary where clauses (including associated type equality) + [*] Lazy associated item inference (Foo.Bar.Baz.Biz lazily infers the class at each step!) + [*] Type checker is Turing-complete (is this a feature? Probably not...) * [*] Pattern matching + [*] Destructuring and binding + [*] ADT patterns + [*] List patterns ([a, b, c], [a, b .. c], etc.) + [*] Arithmetic patterns (i.e: n + k) + [*] Inhabitance checks (i.e: None exhaustively covers Maybe Never) + [*] Recursive exhaustivity checks + [*] let does pattern matching * [*] First-class functions + [*] Functions support pattern-matching + [*] Currying * [*] Typeclasses + [*] Type parameters + [*] Associated types + [*] Operators are implemented as typeclasses * [*] Monadic IO (due for removal in favour of effect-based IO) + [*] do notation * [*] Algebraic effects + [*] Effect objects (independent of functions, unlike some languages) + [*] Basin and propagation syntax (equivalent to Haskell's do notation, or Rust's async blocks) + [*] Generic effects + [*] Effect handlers (including stateful handlers, allowing expressing effect-driven IO in terms of monadic IO) * [*] Built-in lists + [*] Dedicated list construction syntax ([a, b, c], [a, b .. c, d], etc.) * [*] Explicit tail call optimisation * [*] MIR optimiser + [*] Monomorphisation of generic code + [*] Inlining + [*] Const folding + [*] Symbolic execution + [*] Dead code removal + [*] Exhaustive pattern flattening + [*] Unused function pruning * [*] Bytecode compiler * [*] Bytecode virtual machine Current working on * [ ] Pattern exhaustivity checking (sound, but unnecessarily conservative) * [ ] Arithmetic patterns (only nat addition is currently implemented) * [ ] Typeclasses + [ ] Coherence checker * [ ] MIR optimiser + [ ] Unboxing + [ ] Automatic repr changes for recursive types o [ ] Transform data Nat = Succ Nat | Zero into a runtime integer o [ ] Transform data List A = Cons (A, List A) | Nil into a vector * [ ] Algebraic effects + [ ] Effect sets + [ ] Effect aliases + [ ] Higher-ranked effects (needed for async, etc.) + [ ] Arbitrary resuming/suspending of effect objects + [ ] Full monomorphisation of effect objects Planned features * [ ] Better syntax * [ ] Module system (instead of import copy/paste) * [ ] LLVM/Cranelift backend Interesting features Here follows a selection of features that are either unique to Tao or are uncommon among other languages. Arithmetic patterns Tao's type system is intended to be completely sound (i.e: impossible to trigger runtime errors beyond 'implementation' factors such as OOM, stack overflow, etc.). For this reason, subtraction of natural numbers yields a signed integer, not a natural number. However, many algorithms still require that numbers be counted down to zero! To solve this problem, Tao has support for performing arithmetic operations within patterns, binding the result. Because the compiler intuitively understands these operations, it's possible to statically determine the soundness of such operations and guarantee that no runtime errors or overflows can ever occur. Check out this 100% sound factorial program! fn factorial = | 0 => 1 \ y ~ x + 1 => y * factorial(x) All functions are lambdas and permit pattern matching Excluding syntax sugar (like type aliases), Tao has only two high-level constructs: values and types. Every 'function' is actually just a value that corresponds to an line lambda, and the inline lambda syntax naturally generalises to allow pattern matching. Multiple pattern arguments are permitted, each corresponding to a parameter of the function. def five = let identity = fn x => x in identity(5) Exhaustive pattern matching Tao requires that pattern matching is exhaustive and will produce errors if patterns are not handled. Very few delimiters, but whitespace isn't semantic In Tao, every value is an expression. Even let, usually a statement in most languages, is an expression. Tao requires no semicolons and no code blocks because of this fact. Currying and prefix calling In Tao, arg:f is shorthand for f(arg) (function application). Additionally, this prefix syntax can be chained, resulting in very natural, first-class pipeline syntax. my_list -> filter(fn x => x % 2 == 0) # Include only even elements -> map(fn x => x * x) # Square elements -> sum # Sum elements Useful, user-friendly error diagnostics This one is better demonstrated with an image. Example Tao error Tao preserves useful information about the input code such as the span of each element, allowing for rich error messages that guide users towards solutions to their programs. Diagnostic rendering itself is done by my crate Ariadne. Commands Compile/run a .tao file cargo run -- Run compiler tests cargo test Compile/run the standard library cargo run -- lib/std.tao Compiler arguments * --opt: Specify an optimisation mode (none, fast, size) * --debug: Enable debugging output for a compilation stage (tokens, ast, hir, mir, bytecode) About A statically-typed functional language with generics, typeclasses, sum types, pattern-matching, first-class functions, currying, algebraic effects, associated types, good diagnostics, etc. Topics programming-language functional compiler Resources Readme Stars 512 stars Watchers 12 watching Forks 15 forks Releases No releases published Packages 0 No packages published Contributors 5 * @zesterer * @JCapucho * @dependabot[bot] * @Person-93 * @danaugrs Languages * Rust 100.0% Footer (c) 2022 GitHub, Inc. Footer navigation * Terms * Privacy * Security * Status * Docs * Contact GitHub * Pricing * API * Training * Blog * About You can't perform that action at this time. You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.