ATS3-Xanadu

A Programming Language System to Unleash the Potentials of Types and Templates

Build Status

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): GPLv3
• The ATS source for the Libraries (ATSLIB/{prelude,xatslib}): LGPLv3.
• As a special exception, any C code generated by the Compiler based on the Libraries source is not considered by default to be licensed under GPLv3/LGPLv3. If you use such C code together with other code to create an executable, then the C code by itself does not cause the executable to be covered by GPLv3/LGPLv3. However, there may be reasons unrelated to using ATS that can result in the executable being covered by GPLv3/LGPLv3.
• 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, which one can, for instance, freely insert into any C code generated from ATS source code.