A vision for future programming in ATS

[gmhwxi]

Hi, there,

HX-2022-01-29:

A vision for future programming in ATS

Before I start, I would like to quote captain Woodrow F. Call,
a character played by Tommy Lee Jones in Lonesome Dove:

"Man of Vision you say.......? Yeah. Hell of a vision." ~ Woodrow Call

By the way, here is the end of the Lonesome Dove miniseries where
Woodrow Call uttered the above line when interviewed by a reporter:

https://www.facebook.com/caldwellwritesdotcom/videos/lonesome-dove-tells-the-story-of-two-friends-who-were-legendary-texas-rangers-an/440279033007270

Ideally, a programming language should be simple and general, and
it should permit extensive error checking, facilitate proofs of
program properties such as correctness, and possess a correct and
efficient implementation. Invariably there will be some conflicts
among these goals which must be resolved with careful attention to the
needs of the user. I learned the above from Prof. John Reynolds when I
was a PhD student at CMU.

ATS3 is not an ordinary programming language. It is more like a
programming language for support meta-programming of all sorts.
Suppose we want to have programs written in some language X. Then we
traditionally write these programs manually in X. ATS3 provides an
alternative: We can implement a compiler from ATS3 to X to allow us to
write programs in ATS3 and then compile them to code in X.  In
practice, we hope to do co-programming with ATS3 and X; code in X
generated from ATS3 source can be combined with code in X obtained
otherwise. By programming in ATS3, we can benefit greatly from the
advanced type-checking that allows many varities of bugs to be flushed
out at compile-time; we can also benefit greatly from the extensive
use of templates that allows massive amount of quality code to be

generated in an automated manner.

In a following post, I will use a concrete example (co-programming
with ATS3 and Javascript) to outline some of the big steps involved
in building a compiler to support co-programing with ATS3 and X,
where X is just a placeholder for some programming language of one's
choice.

Cheers,

--Hongwei

##################################################################

For previously post messages:

https://github.com/githwxi/ATS-Xanadu/tree/master/docgen/NOTES

##################################################################

[gmhwxi]

Here is project for compiling ATS3 to JS:

https://github.com/xanadu-lang/Xats2js-H0

H0 refers to a high-level abstract syntax tree generated by xatsopt, which

mostly does parsing and fixity resolution and binding resolution and (non-dependent)

type-checking and template resolution.

I put the code for xatsopt in a git submodule. The compiler from ATS3 to JS is referred

to as xats2js, which turns ATS3 code into Javascript code; the obtained JS code needs

to be combined with some code for various basic JS functions (which I call run-time);

and the code combination is done through copying/pasting code :)

You can try some of the JS code generated by xats2js from ATS3 source:

https://xanadu-lang.github.io/

Cheers!

--Hongwei

PS: Sorry, I won't have time to write a detailed documentation for xats2js. However,

if you have high-level (or maybe not so high-level) questions, I will try to answer them

to the extent I can.