Lambda the Ultimate

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

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.

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)