ATS3-Xanadu
A Programming Language System to Unleash the Potentials of Types and Templates
Build Status
GitHub Actions builds ATS3 and runs the JavaScript, Scheme, and Python prelude tests on Ubuntu 24.04, using Node.js 24 and the bundled ATS2 release. CI checks the default branch daily at 2:00 a.m. America/New_York time and skips the build if that commit has already passed CI. Failed builds are retried the next day. Pushes and pull requests do not trigger builds. Scheduled builds also build the bootstrap libraries on alternating calendar days (every two days), provided that the commit needs a build. Manual workflow runs always build and offer an optional bootstrap-library build. See the CI scripts and local build instructions for details.
The separate Cygwin CI workflow builds ATS-Xanadu on Windows and runs the JavaScript and Python prelude tests weekly on Mondays at 2:00 a.m. America/New_York time; it can also be started manually.
Project Description
ATS3 is an attempt to greatly improve upon ATS2.
Probably the biggest problem with ATS2 is the _very_ steep learning curve associated with it. Very few programmers were able to ever overcome it to reach the point where they could truly start enjoying the tremendous power of (advanced) type-checking and (embeddable) templates.
[comment]: # HX: I probably wrote this in 2018 to motivate ATS3!
When DML (the predecessor of ATS) was designed nearly 20 years ago, a two-layered approach to type-checking was taken: ML-like type-checking first and dependent type-checking second. This approach was later abandoned in the design of ATS. Instead, there is only dependent type-checking in ATS1 and ATS2. In ATS3, DML's two-layered approach is to be adopted. In particular, a program in ATS3 that passes ML-like type-checking can be compiled and executed. So one can skip dependent type-checking in ATS3 if one so chooses. In this way, the learning curve is expected to be greatly leveled. But there is much more than just leveling the learning curve.
ML-like types are algebraic (involving no explicit quantifiers). Such types are so much friendlier than dependent types (which often involve explicit quantifiers) for supporting type-based meta-programming. It seems that a chance has finally arrived to properly address the problem of template instance resolution that causes so much annoyance in ATS2 (due to the very use of dependent types for template selection).
In short, ATS3 adds an extra layer to ATS2 for supporting ML-like algebraic type-checking. Type-based meta-programming in ATS3 solely uses algebraic types (while ATS2 uses dependent types).
Installing ATS3
[Comment]: # HX: ATS3 was first successfully bootstrapped on 03/29/2025!
ATS3 is available for testing. Here are some details on the release of ATS3-alpha.0.1. Please see XATSHOME for instructions.
- You need 'node' or 'nodejs' for running the ATS3-to-JS-in-ATS3.js compiler.
- You need 'node' or 'nodejs' for running the ATS3-to-PY-in-ATS3.js compiler.
Developing ATS3
Documenting ATS3
This has been ongoing with no ending in site. Please see the READMEs spreaded in various directories. These READMEs can be seen as the first attempt to document ATS3. Hopefully, there will be more and more attempts in the future when ATS3, its design and implementation, is understood and appreciated by more and more people.
Licenses for ATS/Xanadu
- The Compiler (ATS/Xanadu):
- The ATS source for the Libraries (ATSLIB/{prelude,xatslib}):
- As a special exception, any C code generated by the Compiler based on the Libraries
- The contributed portion (ATS/Xanadu/contrib) is released under the MIT license.
- There is also a release under the MIT license for the C header files of the Libraries,