Re: ATS3: ATS/Xanadu

Thanks for your interest in ATS! Will take into consideration your suggestions. The current implementation of ATS3 is done in a way that should make it straightforward for other people to implement tools performing code analysis. My hope is that such tools can be distributed independently and

Re: ATS3: ATS/Xanadu

Thanks for your continued interest. I have not started this line of work yet. Currently I am working on an interpreter for ATS3, trying to complete a reference implementation before going forward. On Friday, December 6, 2019 at 10:49:54 AM UTC-5, Dan'l Miller wrote: > > In ATS3, how is the

Re: ATS3: ATS/Xanadu

In ATS3, how is the alternate-syntax-to-ground-syntax coming along as an archetypical mechanism (not any one particular transform yet) or is that capability still future work yet to be added to ATS3's source code? Is alternate-to-ground syntax transforms envisioned to be tree transductions

Re: ATS3: ATS/Xanadu

Hello, I have been learning ATS2, and wanted to chime in. I'm a bit late to the party, but I've given these quite a bit of thought. I have more, but I need to learn more about ATS2 before being sure enough to suggest them. I'll be asking a few things soon :) I don't have an issue with how

Re: ATS3: ATS/Xanadu

Are there any plans on streamlining it's use with LLVM and/or the musl libc library? Have you (or anyone else) tested it's usefulness with Webassembly? These would come in handy. Diogenes -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To

Re: ATS3: ATS/Xanadu

On Mon, Oct 22, 2018 at 1:38 AM gmhwxi wrote: > > > Yes, you can already use ATS2 with Z3: > > https://github.com/githwxi/ATS-Postiats/tree/master/contrib/ATS-extsolve-z3 > I wrote a bit about using it here: https://bluishcoder.co.nz/2018/01/03/writing-basic-proofs-in-ats.html --

Re: ATS3: ATS/Xanadu

Yes, you can already use ATS2 with Z3: https://github.com/githwxi/ATS-Postiats/tree/master/contrib/ATS-extsolve-z3 On Sunday, October 21, 2018 at 3:19:39 AM UTC-4, Kiwamu Okabe wrote: > > On Sun, Oct 21, 2018 at 8:05 AM Hongwei Xi <...> wrote: > > I hope > > to be able to export theorems

Re: ATS3: ATS/Xanadu

On Sun, Oct 21, 2018 at 8:05 AM Hongwei Xi wrote: > I hope > to be able to export theorems needed by a ATS program to external > theorem-provers. > I think a particular focus should be on automated theorem-proving. Do you use Z3 such like F*? https://www.fstar-lang.org/ -- Kiwamu Okabe at

Re: ATS3: ATS/Xanadu

Does this mean one of the external theorem provers will replace ATS/LF? Will one be chosen or will it be relatively easy for a user to choose without much tooling for ATS3? I've never used one but have it on my list to try out out. I've heard good things about the generality of Coq but also

Re: ATS3: ATS/Xanadu

Thanks! Yes, the syntax design for the core of ATS3 is mostly done at this stage. The comments may not be up-to-date but should not be far off. Here are a few notes: Keywords for initiating a declaration usually start with the symbol # For instance, #infixl (50) + - #include

Re: ATS3: ATS/Xanadu

On Sat, Oct 20, 2018 at 1:42 PM Vanessa McHale wrote: > Cross-compilation is in decent shape even with ATS2, at least on Debian. Thanks. I hope ATS3 also do that. > I have built binaries for many platforms you can imagine, including > Redox https://github.com/vmchale/illiterate/releases Wow!

Re: ATS3: ATS/Xanadu

Cross-compilation is in decent shape even with ATS2, at least on Debian. I can cross-compile a program for Raspberry Pi using Debian-provided cross-compilers. I have built binaries for many platforms you can imagine, including Redox https://github.com/vmchale/illiterate/releases As for package

Re: ATS3: ATS/Xanadu

Dear Hongwei, Thanks for your great effort for developing ATS3. I can hardly wait publishing your first release of ATS3 manual! On Sat, Oct 20, 2018 at 10:48 AM gmhwxi wrote: > I currently have no plan to add more support for theorem-proving in ATS3. OK. It's just idea. No problem. > My

Re: ATS3: ATS/Xanadu

Hi Kiwamu, As always, thanks for your input! I currently have no plan to add more support for theorem-proving in ATS3. My expectation is to find ways to make direct use of existing theorem-proving systems (e.g., Isabel, Coq, Lean, various SMT solvers, etc.). I certainly want to be ambitious

Re: ATS3: ATS/Xanadu

I slightly learn Prolog for the design of ATS3. My opinion is following: ## Variable is useful ``` $ cat family.pl father(naoyuki, hyogo). father(saburo, naoyuki). father(saburo, shinji). father(yoshihisa, hisako). mother(hisako, hyogo). mother(yoko, naoyuki). mother(yoko, shinji).

Re: ATS3: ATS/Xanadu

On Thu, Oct 11, 2018 at 1:40 PM Kiwamu Okabe wrote: > A. Symbolic execution such like https://github.com/verifast/verifast IDE, >because we can watch execution sequence on the IDE. >See the following Steps pane on figure 1 at page 4. >

Re: ATS3: ATS/Xanadu

Also I think following are good parts: A. Symbolic execution such like https://github.com/verifast/verifast IDE, because we can watch execution sequence on the IDE. See the following Steps pane on figure 1 at page 4. https://people.cs.kuleuven.be/~bart.jacobs/verifast/tutorial.pdf B.

Re: ATS3: ATS/Xanadu

On Thu, Oct 11, 2018 at 12:07 PM Hongwei Xi wrote: > I hope that I can structure the ATS3 compiler in such a way that you > should be to add DWALF support on your own. Yes. I believe such DWARF support is only hoped by me. -- Kiwamu Okabe at METASEPI DESIGN -- You received this message

Re: ATS3: ATS/Xanadu

Okay. I keep this in mind. I hope that I can structure the ATS3 compiler in such a way that you should be to add DWELF support on your own. On Wed, Oct 10, 2018 at 10:48 PM Kiwamu Okabe wrote: > May I add more requirement? > > ## Debugger support with DWARF > > * Rust support showing

Re: ATS3: ATS/Xanadu

May I add more requirement? ## Debugger support with DWARF * Rust support showing backtrace on the Rust source code. https://rust-embedded.github.io/bookshelf/discovery/05-led-roulette/debug-it.html * It's useful to debug hardware, not software. * Sometime we face such hardware bugs and end

Re: ATS3: ATS/Xanadu

Indeed, this can be a very useful feature. When I implemented macdef (and macrodef as the recursive version of macdef), I only handled certain forms of expression (to be used as the definition of a macro). I could try to see if it is easy to add a few more forms so as to handle your example.

Re: ATS3: ATS/Xanadu

Thanks Julian, I could see this as a possible implementation of the original templates. Ultimately, I would see the parser parameterized over different input / output types, and stack allocated variables could be different sizes, depending on what is being parsed. I think templates would be

Re: ATS3: ATS/Xanadu

On Thursday, October 4, 2018 at 8:47:31 PM UTC-5, M88 wrote: > > Recently I was attempting to write parser combinators without > heap-allocated closures (or any sort of allocation). It was a bit > difficult because stack-allocated closures are of varying size and must be > affixed to a `var`.

Re: ATS3: ATS/Xanadu

I'd agree in general that documentation, errors and usability improvements are very important in ATS3 -- ATS2 is a feature-rich language as it is, but exceedingly difficult to navigate. I will go on to propose a feature, but the former aspect should get more of the focus. Recently I was

Re: ATS3: ATS/Xanadu

Thanks for all of your input and effort! In ATS3, syntax errors of a program are internalized in its abstract syntax tree. I expect that various syntax-checkers can be written to explain the cause of syntax errors. With good support from the community, the learning curve for ATS3 should be a lot

Re: ATS3: ATS/Xanadu

Thanks for all the input! Still working on the parser. Will post a message on its progress shortly. I personally like SML-like syntax, which is quite different from OCaml's. After I publish the syntax for ATS3, I hope that someone could design a version for it based on Lisp's syntax. Cheers!

Re: ATS3: ATS/Xanadu

On Monday, October 1, 2018 at 6:40:20 PM UTC-5, Vanessa McHale wrote: > > To me the main appeal of C over ATS is the existence of a standard and > several competing compilers. It's just a more stable language and there's > guarantees of better support. C features are documented and there are

Re: ATS3: ATS/Xanadu

To me the main appeal of C over ATS is the existence of a standard and several competing compilers. (I also like the fact that C has an ABI, but then ATS benefits from this as well :)). It's just a more stable language and there's guarantees of better support. C features are documented and there

Re: ATS3: ATS/Xanadu

Prompted by Zig's 0.3.0 release, I thought about ATS3 a little more. Zig prompted that in two different ways: first, the release notes had this charming assertion: "Zig intends to be so practical that people find themselves using it even if they dislike it." Second, while considering Zig, although

Re: ATS3: ATS/Xanadu

As I'm sure you're aware OCaml's syntax is not widely liked, leading to a lot of attempts at resyntaxing (Revised, Pidgin, ReasonML amongst others) so attempting to copy it doesn't strike me as a good idea. SML is not widely used enough for me to have a sense of how much the syntax was liked.

Re: ATS3: ATS/Xanadu

It is not too late :) For meta-programming support, LISP-like syntax is definitely on my mind. At this point, I want to first finish designing and implementing some ML-like (ML-inspired) syntax for ATS. I am getting there :) Once this ML-like syntax is done, it can readily serve as the basis

Re: ATS3: ATS/Xanadu

I know this comes too late and was doomed anyway, but my opinion is the best syntax is always Lisp. :) On Friday, February 9, 2018 at 12:15:22 PM UTC-6, gmhwxi wrote: > > For the moment, I just want to open a thread for ATS3. > > I decided to pick ATS/Xanadu for the full project name. I like the

Re: ATS3: ATS/Xanadu

Hi Andrew, Many thanks for all these questions and links. Very thoughtful! Besides being a programming language for people to write code in, I certainly hope that ATS3 can also be a platform for you (and others) to try out ideas (e.g., those you mentioned). It may sound a bit strange but I do

Re: ATS3: ATS/Xanadu

Just some miscellaneous thoughts and questions. - Here's a paper ("Beyond Type Classes") that I found interesting. It's a generalization of Haskell's type class system that does type-directed overloading via user-defined Constraint Handling Rules (CHRs). It fits nicely with the logic

Re: ATS3: ATS/Xanadu

Yes, I have a similar thought :) On Thursday, May 10, 2018 at 8:35:57 PM UTC-4, Andrew Knapp wrote: > > Another idea/request: replace the use of > ATS_MEMALLOC_USER/ATS_MEMALLOC_LIBC and friends with embeddable templates. > > In this example > > let > implement allocate() =

Re: ATS3: ATS/Xanadu

Did anyone mention operators definition/overloading? I think currently in ATS2, one can only overload a symbol with a function. But I actually prefer how OCaml and Haskell handles operators: they are just functions whose names happen to be symbols instead of alphabets. One use parenthesis

Re: ATS3: ATS/Xanadu

I suppose there has been a fair bit of talk about syntax already. I had been thinking a whitespace-significant label-block structure (a-la Nim) might suit the language well, and some recent code sample inspired me to demonstrate. Original: datasort tlist = tnil | tcons of (t0ype, tlist)

Re: ATS3: ATS/Xanadu

>>As for build systems, I think that shake is probably good to have ... That would be great! I plan to export the syntax tree of an ATS program into JSON. >>On the ATS front: I am curious as to how ATS optimizes tail recursion. I know Scala doesn't

Re: ATS3: ATS/Xanadu

I'm actually not a huge fan of Scala syntax, simply because I find it verbose and I believe that it is not suited to functional programming in general. If there are reasons to support methods and whatnot, then I would be more amenable to it. As for build systems, I think that shake

Re: ATS3: ATS/Xanadu

After writing several thousand lines of ATS, I'd say there isn't terribly much I'd change, honestly. A lot less than when I got started, for sure. What I would like to see changed: 1. Real module system. MixML might not be a bad source of inspiration, as it would essentially be a better

Re: ATS3: ATS/Xanadu

Many thanks for your input! >>perhaps H/M inference alone could go a long way. That is really my bet :) >>I suppose I'm about as efficient at ATS2 as I am with C Yes, one can do C-style coding in ATS. With ATS, my hope is that one is able to use more functional programming to solve problems

Re: ATS3: ATS/Xanadu

> I thought about this issue as well. One idea I had is to > use overloading aggressively. > A thought I had recently -- I'm almost wondering if certain proofs (eg, linear proofs) could behave more like value constraints. That is, they could be invoked optionally, and would only be checked

ATS3: ATS/Xanadu

Not sure if it's feasible or theoretically sound, but it would be nice to see a less stark divide between datatypes and dataviewtypes in ATS3. It would be great to be able to declare a data structure once and use either linear or gc'd versions. Maybe this could extend to other types that have

Re: ATS3: ATS/Xanadu

This sounds more like an IDE issue to me. On Tue, Mar 13, 2018 at 3:20 PM, Brandon Barker wrote: > Replying to the concise syntax issue in particular: I like concise syntax > up to a point, but when it comes to types, explicit syntax is sometimes > nice (though it

Re: ATS3: ATS/Xanadu

Replying to the concise syntax issue in particular: I like concise syntax up to a point, but when it comes to types, explicit syntax is sometimes nice (though it would be great to allow the user to choose). Both to make compilation proceed quicker (possibly), and to make it more obvious what

Re: ATS3: ATS/Xanadu

I don't know if TASTY might be of help, either in ideas or actual implementation. Some more indepth discussion of TAST: https://github.com/twitter/reasonable-scala/issues/21 On Saturday, March 10, 2018 at 10:00:31 AM UTC-5, gmhwxi wrote: > > Thanks. > >

Re: ATS3: ATS/Xanadu

While jumping back into ATS, a few other minor things (lots of minor things add up) that might be nicer is string interpolation in the form of python 3.6 or Scala (both are very similar). Here's a copy paste example from python 3.6: 1. name = "Spongebob Squarepants"print(f"Who lives in a

Re: ATS3: ATS/Xanadu

Glad to see this thread is here. I will just share some general thoughts for syntax as my ATS is a bit rusty: 1. I like Scala style syntax - I think it is easy enough to read, unless maybe you are doing stuff at the type level, where ATS seems to have an advantage over Scala. I think Scala is

Re: ATS3: ATS/Xanadu

In reference to the quoted, I will note that I have written a package for dealing with ATS syntax in Haskell. The pretty-printer works marvelously, but getting the parser right is HARD. The package already has around 1400 lines of code for the

Re: ATS3: ATS/Xanadu

Many here have mentioned syntax as a point of improvement. While I agree, I have no opinions on which variant (ML vs. C vs. Lisp) is more aesthetically appealing. Some things I look for are unambiguous indentation, easy for a machine to format and easy to parse. I think syntax should be

Re: ATS3: ATS/Xanadu

On Saturday, February 10, 2018 at 12:15:22 AM UTC+6, gmhwxi wrote: > > For the moment, I just want to open a thread for ATS3. > > I decided to pick ATS/Xanadu for the full project name. I like the name > Xanadu > because it is poetic and brings a feel of exoticness. > > ATS3 is supposed to be

Re: ATS3: ATS/Xanadu

I have accrued a bit of a wishlist while working with ATS. Maybe some of it is useful or feasible. Things I would keep the same: - I think dependent type / proof syntax is well done, and it feels a bit more natural than Idris. I'd keep this the same - The '~' to free an unfolded

Re: ATS3: ATS/Xanadu

I have something to add to the wishlist: "better" linear functions. We had a discussion about this almost a year ago. The issue I raised back then is that there is no real way to free a linear function without applying it. This is not a concern motivated by category theory or something such,

Re: ATS3: ATS/Xanadu

Thanks for writing it down. Hopefully, this does not end up a merely pipe dream :) I would also put 'type inference' high up there. Some variant of Hindley-Milner type inference should be a crucial part of ATS3. On Tuesday, February 13, 2018 at 2:52:29 PM UTC-5, Steinway Wu wrote: > > Hi

Re: ATS3: ATS/Xanadu

It is not that I like pan-syntax. What I really like is syntax-independence, but we are still very far from it :) When facing uncertainties, I would say that one's natural reaction is to keep the options open. On Tuesday, February 13, 2018 at 2:24:08 PM UTC-5, August Alm wrote: > > I realize

Re: ATS3: ATS/Xanadu

Hi Hongwei, just for the record, let me put down some offline discussions. 1. Programmers can decide how a literal is parsed, or even write some plugins to parse some custom literals. For instance, 1 can be interpreted as int, nat, and int(1) etc. Programmers should be able to either turn a

Re: ATS3: ATS/Xanadu

Let's experiment. My rough plan for now is to have something largely based on the current syntax of ATS2 (modulo some minor fixes) as the "ground" syntax. This syntax is going to be explicit and verbose. There will be an interface for it (e.g., via JSON). Then we can embrace a "pan-syntax"

Re: ATS3: ATS/Xanadu

Fine by me! As long as the syntax encourages a uniform and readable coding style. Also, I think it would help ATS if it looked more (seemingly) familiar to a more widely known language. For example, at the moment we have the abbreviated syntax " = {...}" for "= () where {...}", which allows us

Re: ATS3: ATS/Xanadu

If we talk syntax, why not adopt that of C? :-) 13 февр. 2018 г. 8:43 ПП пользователь "August Alm" написал: I second the preference for Haskell-style "let" and "where", which is to say no "end"s and no curly braces. Of course, this requires indentation to be syntactic and

Re: ATS3: ATS/Xanadu

I don't have any concrete suggestions, but I would suggest Idris as an example to follow. Haskell syntax is relatively popular and concise, and Idris' is even more refined. I will say I'd prefer syntax that eases functional programming, but that might just be me. And I think that replacing -

Re: ATS3: ATS/Xanadu

This works: %{ int ex1[3][4] = { {5, 1, 9, 5} , {7, 5, 3, 0} , {2, 4, 6, 8} }; %} val ex1 = $extval(matrixref(int, 3, 4), "ex1") On Fri, Feb 9, 2018 at 5:59 PM, Julian Fondren wrote: > (Although this is wrong, and causes a segfault.) > > On Friday, February 9, 2018

Re: ATS3: ATS/Xanadu

ah. also: val ex1 = (arrayref)$arrpsz{arrayref(int, 4)}(a, b, c) where { val a = (arrayref)$arrpsz{int}(5, 1, 9, 5) val b = (arrayref)$arrpsz{int}(7, 5, 3, 0) val c = (arrayref)$arrpsz{int}(2, 4, 6, 8) } is there a nicer way to include a matrix in an ATS2 program than this? One might

Re: ATS3: ATS/Xanadu

Aye, like in https://www.youtube.com/watch?v=zt0OQb1DBko where it's twice emphasized that "there are no typos here--this is what ATS looks like". Those are the most off-putting. I would also prefer a more OCaml-like "let val x=1 in (expression)" to the existing "let val x=1 in (expression)

Re: ATS3: ATS/Xanadu

This one is already on my mind. Learned my lessons :) The plan is to use 'abstype' in place of abst@ype. On Fri, Feb 9, 2018 at 4:57 PM, Martin DeMello wrote: > I would love to see t@ype and similar keywords with symbols in the middle > replaced by something more

Re: ATS3: ATS/Xanadu

I would love to see t@ype and similar keywords with symbols in the middle replaced by something more pronounceable - the lack of quick mental pronunciation is a surprisingly large annoyance when reading and wirting code. martin On Fri, Feb 9, 2018 at 10:15 AM, gmhwxi wrote: >

Re: ATS3: ATS/Xanadu

Of course, if you feel that it is more appropriate to have a private discussion, please feel free to send your messages to me directly. On Friday, February 9, 2018 at 1:15:22 PM UTC-5, gmhwxi wrote: > > For the moment, I just want to open a thread for ATS3. > > I decided to pick ATS/Xanadu for

ATS3: ATS/Xanadu

For the moment, I just want to open a thread for ATS3. I decided to pick ATS/Xanadu for the full project name. I like the name Xanadu because it is poetic and brings a feel of exoticness. ATS3 is supposed to be compiled to ATS2. At least at the beginning. I will try to write more about what I