In Praise of Hongwei

[Yves Cloutier]

I've been keeping an eye on ATS for a while now, after being introduced to functional programming, learning a bit of SML,OCaml etc.

I have not seen anywhere else the level of drive, enthusiasm, dedication, innovation that Hongwei has and continues to have.

That being said, I'm still in ATS pre-school and can't say I've been able to write anything mildly impressive.

But just wanted to bow my hat down to this human (?) they call Hongwei.

May you keep on innovating and breaking new grounds.

[Artyom Shalkhakov]

Indeed it's a curious thing.

I've been following Hongwei's commits for the last 8 years and he has made an impact on the way I view and practice programming.

Thanks much, Hongwei!

9 февр. 2018 г. 2:55 ДП пользователь "Yves Cloutier" <yves.c...@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-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@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/f74d7c3d-06e7-4dc7-a456-5db9a3b4e34b%40googlegroups.com.

[gmhwxi]

This is a bit unusal :)

Thanks for all the compliments. Maybe it is time to think about ATS3?

Cheers!

On Thursday, February 8, 2018 at 8:24:36 PM UTC-5, Artyom Shalkhakov wrote:

Indeed it's a curious thing.

I've been following Hongwei's commits for the last 8 years and he has made an impact on the way I view and practice programming.

Thanks much, Hongwei!

9 февр. 2018 г. 2:55 ДП пользователь "Yves Cloutier" <...> написал:

[Julian Fondren]

I've been learning ATS for about a month, mostly in the hours of

midnight to 2AM, so it's been slow going. But, I can see this a

genuinely worthwhile language that has both very interesting ideas and

nuch practical value.

I used to learn programming languages obsessively, and I quit that a

long time ago as a bad habit and (in retrospect) mostly wasted effort.

But, I do have that experience, of reading lots of tutorials and using

different kinds of documentation and participating in communities that

varied a lot in their resources, to learn these languages.

So, on topic with the thread, your work for ATS really comes across,

in your websites and your writing and your participating in various

communities. And you do a good job of presenting the language as

*worth* someone trying to use.

On the topic of making ATS easier to learn and use (maybe that's part

of the idea of ATS3?), I think the language as it is can be made much

more accessible with just documentation efforts.

Consider Mercury's docs: http://mercurylang.org/documentation/documentation.html

The Mercury tutorial is not very good, mainly in how little of the

language it covers (imagine that the only ATS tutorial never even

mentions linear types)--but there is also:

  * the Mercury Language Reference Manual, which describes all of the

    features of the language in detail -- its syntax, all of the kinds

    of types it supports, how the language fundamentally works, etc.

  * the Mercury User's Guide, which describes the tools provided with

    the language in detail. All of the compiler's flags, how to use

    the debugger, how to use their build system shortcuts (tools that

    you can use in lieu of writing a Makefile or more, to get

    started).

  * the Mercury Library Reference Manual, which describes all of the

    libraries provided with Mercury, in detail. All the functions that

    you can use with arrays, lists, strings. All of the I/O functions.

    With examples, usage, type information.

At present ATS is missing a User's Guide (not a big deal) and a

Library Reference Manual (this would make a lot of code that shipped

with ATS easier to employ and would double as a source of on-point

examples that would help people understand the language features

exhibited by the code or required for its use) . Currently, for a

language reference I mostly load the onechunk.html version of

Introduction to Programming in ATS and hit ctrl-F and hope what I'm

confused about has some examples that I can understand. For library

reference I have what I see used in examples and what then I do a lot

of 'grep -r strptr /usr/local/lib/ats*'

And then, ATS has some features that no other language has--or has in

a similar-enough manner to be useful--so it would benefit from some

very narrowly focused tutorials. Introduction to Programming in ATS is

good overall, and good for most of the language, but, consider: the

Theorem-Proving in ATS/LF section begins with a dataprop example.

This is very cool, but in order to apply that example I would have to

know a lot more about ATS proofs than I could know at that point. The

next series of examples all accept proof variables or return them.

Later in section IV there is this example:

fn fact{n:nat}

  (n: int (n)): int = let

  fun loop{n:nat}{l:addr} .<n>.

    (pf: !int @ l | n: int n, res: ptr l): void =

    if n > 0 then let

      val () = !res := n * !res in loop (pf | n-1, res)

    end // end of [if]

  // end of [loop]

  var res: int with pf = 1

  val () = loop (pf | n, addr@res) // addr@res: the pointer to res

in

  res

end // end of [fact]

A factorial function, the 'hello world' of functional programming. I

know how that works. And this code functions by reassigning a memory

location allocated on the stack. I understand that too. And pf, that

is... synthesized from the var definition, and then passed around to

show that it's OK for the other code to write to that location.

Awesome! I felt like I'd finally reached a breakthrough in

understanding theorem-proving in ATS with this. A proof variable is

created, used, and then discarded in this short example.