## 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

### 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)