Re: ats tutorial in mountain view

[Raoul Duke]

Thanks to Will for being a stupendously great, knowledgeable, patient,
helpful, and all around terrific tutor. Somebody seriously give that
gentleman a raise.

Thanks for everybody who attended in person, or in spirit. Apologies
for the vagaries of the teleconferencing setup.

Maybe we can even convene again some time?

[Brandon Barker]

http://julialang.org/teaching/  <- it might be nice to have something like this, at some point soon. Not saying it is priority #1 but it could possible be done in parallel with other teaching/meetups. Even if videos are not the best way to get a feel for ATS as opposed to some dynamically typed "interpreted" language, I think it would still show the human element better, and that there's an interested community (and that ATS isn't just an ivory tower gig).

Also, sorry for always referencing julialang... but it is easier to just use one good example.

Brandon Barker
brandon...@gmail.com

--
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 http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAJ7XQb5E9cXO%2B%2BzT7bMs_DtufKYcRKntjiN1arGdWUCqT5r%3DYA%40mail.gmail.com.

[Raoul Duke]

I think if Will posts his annotated code that he worked on during the
tutorial session, that will be a good one to have for people.

(Also... I will then be able to remember the syntax I need to show
that I really really really really really think that the way "!" works
is backwards, if the whole point of linearity is for safety of things.
I figure the syntax will never change, but I figure I should make the
argument one last time, with code. :-)

[Martin DeMello]

agreed, that was a very useful tutorial!

martin

[William Blair]

Thank you very much, I'm glad you liked it. It was really good getting some feed back on ATS and the good suggestions on usability. I plan to (hopefully) work some of them into an external constraint solver. In any case, pretty printing unsolved constraints is high on my priority list :D.  

I'm working on annotating the code we went through, and I'll post it to this thread when it's done.

[Martin DeMello]

one thing i thought while following the tutorial was that it'd be really useful to have a pretty printer for the constraint solver error messages. is this something it would be feasible to do as an external project, on a purely text-transformation basis? if so i'd be happy to have a go at it (if it requires plugging into the guts of ats i probably won't have much chance, but text->text seems like it'd be mostly a matter of putting the work in)

martin

--

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 http://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/26a4910b-8f33-4f11-ae40-722c8e410a6f%40googlegroups.com.

[William Blair]

It is feasible to do now that the ATS compiler can export constraints in a JSON format. One issue is that it exports all of the constraints in the program into one big JSON object. We have been working on an external constraint solver that uses this format as input. I need to clean the code up a bit so that others can contribute and use it, but the task of pretty printing in it shouldn't be that difficult.

If you'd like to inspect constraints in JSON, you can do the following:

    patsopt --constraint-export -tc -d foo.dats | python -m json.tool > foo.json

and you'll get nice formatted output.

[Martin DeMello]

Great, I'll take a look at it :)

martin

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/1032f361-4cfb-4aa3-b2dd-e63fc947caf9%40googlegroups.com.

[gmhwxi]

You will get used to it if you stare it long enough :)

I can tell you that I have stared at Python's syntax for quite some time
recently.

[Raoul Duke]

now i can only think of A Clockwork Orange...

[gmhwxi]

For now, a simple document telling people how to read the type-error messages should be very helpful.

For instance, the following line of code

val () = assertloc (sum = showtype(1+2+3+4+5.0))

generates the following messages:

/tmp/abcde.dats: 357(line=27, offs=10) -- 394(line=27, offs=47): error(3): the symbol [=] cannot be resolved as no match is found.
/tmp/abcde.dats: 357(line=27, offs=10) -- 394(line=27, offs=47): error(3): [/home/hwxi/research/Postiats/git/src/pats_trans3_util.dats]: d3exp_trdn: the dynamic expression cannot be assigned the type [S2Eapp(S2Ecst(bool_bool_t0ype); S2EVar(10))].
/tmp/abcde.dats: 357(line=27, offs=10) -- 394(line=27, offs=47): error(3): mismatch of static terms (tyleq):

It means:

1. the overloaded operator = cannot be resolved
2. the compiler assigns a error-type (S2Eerr) to the expression: sum = showtype(1+2+3+4+5.0)
3. S2Eapp(S2Ecst(bool_bool_t0ype); S2EVar(10)) stands for bool_bool_t0ype(...)
4. assertloc expects a value of type bool_bool_t0ype(...), but a value of error-type (S2Eerr) is provided.

I think such a document would be far more useful than pretty-printing constraints at this point.

On Friday, August 15, 2014 3:59:26 PM UTC-4, Martin DeMello wrote:

[Raoul Duke]

> I think such a document would be far more useful than pretty-printing
> constraints at this point.

Is this because the format of the constraints might change? Otherwise
I cannot agree :-)

[gmhwxi]

There is no plan to change the format of the constraints.

I once worked on a theorem-proving project and we spent a LOT of time
on prettifying the output of our theorem-prover. This somewhat traumatizing
experience taught me to be wary of pretty-printing.

[Raoul Duke]

> I once worked on a theorem-proving project and we spent a LOT of time
> on prettifying the output of our theorem-prover. This somewhat traumatizing
> experience taught me to be wary of pretty-printing.

ah, ok, good point then -- actual experience! :-)

here's me w/out that experience, as a newbie, thinking: anything that
can be written as actual mathematical symbols (e.g. "illegal: 1 + x ==
x") rather than as the names used internally by the solver etc. would
be better UI/UX i think.

i guess i hope there's a way to do something like that but to do it in
light of your experiences? where do you think it went off track? are
there small wins that could be attained if not for 'solving' the whole
question?

[gmhwxi]

To get a clear message like "illegal: 1 + x == x" is very difficult
to do in general.

If one has some basic understanding of typechecking in ATS, then
one can often use type annotations to get more accurate/informative
messages.

When programming in ATS, one is expected to be able to tell the type
of *any* expression in his or her code. If not, then one may get lost even
if type-error messages are prettified.

When I program in ATS, I primarily rely on the source locations reported
by the typechecker to fix my code. Sometimes, I use showtype and showviewtype.
Sometimes, I try to provide static/template arguments explicitly.

[Brandon Barker]

I used to think it was on par with staring at STL compile errors in C++; now I think it isn't too bad (but I understand your point about a newbie having trouble staring at it - maybe the json approach will provide a less correct but alternative and prettier explanations/guesses).

There is some work still to be done in describing some terms in the error messages, but here's what we have now:

https://github.com/githwxi/ATS-Postiats/wiki/Internal-types

Also, Hongwei's example and maybe others could be added to a tutorial - here's a simple one: https://github.com/githwxi/ATS-Postiats/wiki/Error-messages

Brandon Barker
brandon...@gmail.com

On Fri, Aug 15, 2014 at 5:12 PM, Raoul Duke <rao...@gmail.com> wrote:

now i can only think of A Clockwork Orange...

--
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 http://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAJ7XQb5tPe23WCHiCp%3DuDCaSpRzp2Efwz_icCgpGoXxXfPiZGw%40mail.gmail.com.