ATS3: What is it?

[gmhwxi]

FYI.

As I often get this question, I would like to say a few words about it.

I could talk about some "philosophy" that influenced my design of ATS3

(e.g., Taoist influence on the design of the template system in ATS3) but

that is probably for another post :)

I have been teaching ATS2 at Boston University for about 5 years. The

biggest problem I see is the VERY steep learning curve associated with ATS2.

Very few students were able to ever overcome it to reach the point where they

could truly start enjoying the power of (advanced) typechecking.

When I designed DML (the predecessor of ATS), I employed a two-layered

approach to typechecking: ML-like typechecking first and dependent typechecking

second. I abandoned this approach in ATS. Instead, there is only dependent typechecking

in ATS1 and ATS2. In ATS3, I plan to follow DML's two-layered approach. In particular,

a program in ATS3 that passes ML-like typechecking can be compiled and executed. So

one can skip dependent typechecking 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. Such types are so much friendlier than dependent types

(which often involve quantifiers) for supporting type-based meta-programming. I feel I have

finally got a chance to properly address the template selection problem that brings so

much annoyance in ATS2 (due to the use of dependent types for template selection).

In short, ATS3 adds an extra layer to ATS2 for supporting ML-like algebraic typechecking.

Type-based meta-programming in ATS3 solely uses algebraic types (while aTS2 uses dependent

types). ATS3 may be initially compiled to ATS2 so as to get it going quickly.

Cheers!

--Hongwei

[Kiwamu Okabe]

Could you write this on
https://github.com/githwxi/ATS-Xanadu/blob/master/README ?

[Julian Fondren]

On Friday, October 12, 2018 at 8:54:52 PM UTC-5, gmhwxi wrote:

When I designed DML (the predecessor of ATS), I employed a two-layered

approach to typechecking: ML-like typechecking first and dependent typechecking

second. I abandoned this approach in ATS. Instead, there is only dependent typechecking

in ATS1 and ATS2. In ATS3, I plan to follow DML's two-layered approach. In particular,

a program in ATS3 that passes ML-like typechecking can be compiled and executed. So

one can skip dependent typechecking 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.

Does this something other than the default stdlib avoiding dependent typing for array references,

argc and argv, etc?

That was a very early thought I had about how I might learn ATS2 faster--use a stdlib patterned

after OCaml's so I could just right to work doing things the same way I did in OCaml, and then

gradually make use of dependent types. But, I got comfortable with dependent types faster

than I could finish the purely-runtime-checked stdlib, and gave it up.

I still think that'd be a good idea for learning the language though. The advantage that gradual

dependent typing has over the stdlib making lots of use of them, is that when you get an error

message it's about a constraint that you yourself added to your code, so it should be easier to

figure out.

[Hongwei Xi]

>>Does this something other than the default stdlib avoiding dependent typing for array references,

>>argc and argv, etc?

Yes, this is one aspect.

Say I write A[i]. If the typechecker tells me that there is a type-error because the index may be out-of-bounds,

I am delighted because a possible bug is caught. Unfortunately, many people (e.g., many students I taught) think

otherwise. They would rather have the code compiled so that they could debug it at run-time. I now feel that ATS3

can be designed and implemented so that even people as such can benefit from using it.

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/322ee442-1011-44ea-bdf7-2dd23ad137bd%40googlegroups.com.

[Julian Fondren]

On Saturday, October 13, 2018 at 10:51:58 AM UTC-5, gmhwxi wrote:

>>Does this something other than the default stdlib avoiding dependent typing for array references,

>>argc and argv, etc?

Yes, this is one aspect.

Say I write A[i]. If the typechecker tells me that there is a type-error because the index may be out-of-bounds,

I am delighted because a possible bug is caught. Unfortunately, many people (e.g., many students I taught) think

otherwise. They would rather have the code compiled so that they could debug it at run-time. I now feel that ATS3

can be designed and implemented so that even people as such can benefit from using it.

I think the clarity of the error message would have a lot to do with how the error is received.

For example, in ATS2 this code

#include "share/atspre_staload.hats"

implement main0(argc, argv) = println!(argv[1])

 yields this error:

83(line=3, offs=45) -- 84(line=3, offs=46): error(3): unsolved constraint:
C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(<); S2EVar(5239->S2Eintinf(1)), S2Evar(n$3341(8448))))

So the the problem is clearly located at that argv[1], but what's the problem? ...  some number 'n' isn't less than 1?

There's no 'n' anywhere in this code!

Suppose it read like this:

83(line=3, offs=45) -- 84(line=3, offs=46): error(3): failed to prove n>1, from:
(* ****** ****** *)
//
fun
argv_get_at{n:int}
  (argv: !argv(n), i: natLt(n)):<> string = "mac#%"

then the reaction is more like, "oh, I must've failed to satisfy that natLt(n) there."

and even if you don't immediately realize that tests against argc are what's required, some kind of

constraint querying system, "tell me everything you know about argv" would pull up argc.

since it's also already possible to ignore constraint failures...

$ patsopt --constraint-ignore -o argv_dats.c -d argv.dats
$ patscc -o argv argv_dats.c
$ ./argv
(null)

maybe you could make them *warnings* instead of errors, and then add an option to patscc to restore

their status as errors.

Then the experience is, "I tried to just look at argv, go this really weird warning, but then when I ran

the program there were some bugs... oh! So that's what the warning meant!"

You can still code as if the stdlib didn't use dependent types, but gradually your compiles get noisier :)

[gmhwxi]

Most people can readily understand why argv[1] does not

work if you point out the issue. The problem is that most students

I met could not handle the following one:

extern

fun
{a:t@ype}
Permute(xs: list(a,n)): List(list(a,n))

where Permute returns the list of all the permutations of a given list.

I feel that ATS has many other features to offer in addition to its advanced

support of types. With ATS3, I would like to emphasize more on programming

productivity (instead of primarily focusing on types).

[Chris McCulloch]

I think it might be wise to take some cues from the Wirth family of programming languages. Wirth designed the Oberon system specifically for teaching.

Of course ATS is radically different from Oberon, but the one thing ATS fails to do is address programming "as a human activity". Once that is addressed I suspect ATS will take a noticeable chunk of the FOSS mindshare.

I'm impressed with ATS, but still using Spark and VHDL for my critical programming tasks.

Diogenes

[Hongwei Xi]

>>but the one thing ATS fails to do is address programming "as a human activity

Yes, you are spot on!

I am trying to address this fundamental issue in ATS3. I pin my hope on a re-implementation

of the template system of ATS that is expected to serve as the basis for various meta-programming

extensions of ATS.

>>I think it might be wise to take some cues from the Wirth family of programming languages.

I did draw inspirations from Prof. Wirth's great work on PL and OS. Used to carry his book "Project Oberon"

all the time :)

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/19dc8f9d-2e5a-493a-882a-daa4e279bc1c%40googlegroups.com.

[Yannick Duchêne]

Le mercredi 9 janvier 2019 02:00:48 UTC+1, Chris McCulloch a écrit :

[…] Of course ATS is radically different from Oberon, but the one thing ATS fails to do is address programming "as a human activity". […]

Although tasty, the sentence about programming as a human activity, is not constrained enough to be unembigously interpreted.

People who approve removal of any typing in language (to sometime lately complain it must be bring back in languages not initially design in that purpose), do so complaining type errors are annoying or types are too much a constraint. I mean, they would as much say they prefer no typing to get “programming as a human activity”.

This sentence depends on implicite requirements, lacking to say something about it.

This depends on the purpose of this activity, since software design, when not just a video‑game alternative, is with some practical needs in mind. From the importance of this needs or from the expected reliability of the software fulfilling the needs, the lifetime guesses (ex. temporary need or long time need, and with long time needs comes specialisation of the designers), one may derive these requirements.

That’s for what I would call “programming as a human technical activity”. But they is another one (unfortunately the dominant one I believe), which I would call “programming as an human ideological activity”, which is another question …

In fewer words, the way to “programming as a human activity”, will not be the same for everyone.

[Yannick Duchêne]

Le samedi 13 octobre 2018 03:54:52 UTC+2, gmhwxi a écrit :

[…]

I have been teaching ATS2 at Boston University for about 5 years. The

biggest problem I see is the VERY steep learning curve associated with ATS2.

Very few students were able to ever overcome it to reach the point where they

could truly start enjoying the power of (advanced) typechecking.

When I designed DML (the predecessor of ATS), I employed a two-layered

approach to typechecking: ML-like typechecking first and dependent typechecking

second. I abandoned this approach in ATS. Instead, there is only dependent typechecking

in ATS1 and ATS2. In ATS3, I plan to follow DML's two-layered approach. In particular,

a program in ATS3 that passes ML-like typechecking can be compiled and executed. So

one can skip dependent typechecking 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.

[…]

The risk I see with it, is that the other layer of checks, may always be avoided, like something in a “todo list” which is never done.

But I know it’s a good idea too, this is just that I feel to see this risk.

[girp...@gmail.com]

There's something that I'm curious about when it comes to this two-tiered type system, and that's if using only algebraic types for type-based metaprogramming affects the expressiveness compared to ATS2. I'm still a complete beginner at ATS, so I don't really know how big of an impact this would have, if any.

[gmhwxi]

I don't really have much to say at this moment other than

I am actively working on such a two-tiered system. Hope that

I will be able to pull it off :)