whither ATS2?

From the ATS2 mailing list, a post with a history and an update:

As the primary uncertainty stems from the novel and complex template system of ATS2, I would like to tell you a bit about the motivation behind it.

ATS Trilogy
Part 1. Dependent Types
Part 2. Linear Types
Part 3. Function Templates

The thread is a discussion about how to achieve a language that "provides a powerful high-mechanism for writing (source) code" and some other languages we are all familiar with are (albeit briefly) looked at.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

I don't understand

What is a "high-mechanism for writing (source) code"?

(The thread discussion is baroque; I don't understand which problem is being discussed, but I don't see how "Jay's pattern-calculus" and "type-level sequent calculus used in Shen" may be an answer to the same question.)

an uroboros who begs the question

A fine point, I might have posted something too vapid, for which I apologize.

My interpretation of the tea leaves was that ATS2's Function Templates are hoped to be an interesting experiment along the lines of OO overloading/dynamic dispatch, typeclasses/implicits, etc. Then some other people chimed in with some other things their brains pattern matched. I have a small familiarity with Shen and so the sequent calculus, but not how useful it is for this. The Pattern Calculus has been mentioned here before.

Improvements for proofs and dependent types

I'm looking forward to the ATS2 improvements to the dependent types and proofs. Currently ATS can't handle non-linear constraints, so an implementation of this function fails to typecheck in ATS but my understanding is it should in ATS2:

fun{a:t@ype} list_concat {n1,n2:nat} (xss: list (list (a, n1), n2)): list (a, n1*n2)

(See circumventing non-linear constraints for information on this).

Another improvement is if I use code like the following in ATS:

viewtypedef some_struct = @{ ... }
abstype something (l:addr)

assume something (l:addr) = @{ pfgc= free_gc (some_struct?, l), pfat= some_struct @ l, p= ptr l }

This requires unpacking and repacking the proof everytime you want to access some_struct:

prval pfat = s.pfat
val () = do_something (!s.p)
prval () = s.pfat := pfat

This is apparently improved in ATS2:

Yes, this is pretty annoying. It is due to the weakness of automatic
proof-management in ATS. The good news is that this is all fixed in ATS2.
You just need to do the following in ATS2:

val () = do_something (!s.p)