Re: Building ATS2 from Github head.

[Steinway Wu]

 It is so weird, turns out that

ATSHOME=/some/path/with/../../in/it make -f Makefile_devl all

will fail, but

ATSHOME=/some/absolute/path/with/no/dot make -f Makefile_devl all

works.

Any idea what could have caused that? Is it a Make issue or is it an ATS
compiler issue?



*Steinway Wu*

*吴翰文*

*Google Cloud*

*I'm not a coder.*
*I'm an artist of life.*


On Dec 31, 2020 at 1:31:10 PM, gmhwxi  wrote:

>
> Maybe this has something to do with where the ATS2 package is stored on
> your computer.
> Could you try something like:
>
> cd /tmp
> wget
> http://downloads.sourceforge.net/project/ats-lang/ats-lang/anairiats-0.2.12/ats-lang-anairiats-0.2.12.tgz
> tar xf ats-lang-anairiats-0.2.12.tgz
> cd ats-lang-anairiats-0.2.12/
> export ATSHOME=${PWD}
> export ATSHOMERELOC=ATS-0.2.12
> ./configure && make all
>
> Just tried. This script works for me.
>
> On Thursday, December 31, 2020 at 12:18:22 PM UTC-5 stein...@gmail.com
> wrote:
>
>> Hi,
>>
>> It seems the documentation at
>> https://github.com/githwxi/ATS-Postiats/wiki/Building-and-installing as
>> well as scripts at
>> https://github.com/ats-lang/ats-lang.github.io/blob/master/SCRIPT/C9-ATS2-install-latest.sh
>> are outdated. I’m trying both and encountered link errors.
>>
>> Here’s what I did.
>>
>> # installing ats1
>> wget …
>> ./configure —prefix=…
>> make all_ngc
>> make install
>>
>> # installing ats2
>> git clone …
>> export ATSHOME=…
>> export ATSHOMERELOC=ATS-0.2.12
>> make -f Makefile_devl
>>
>> The errors I see is undefined reference to symbols like
>> _2root_2parts_2ats1_2build_2libatsdoc_... Using nm to view the symbols
>> of libatsdoc.a, I can see they are named like
>> ATS_2d0_2e2_2e12_2libatsdoc_... instead.
>>
>> There was a post
>> https://groups.google.com/g/ats-lang-users/c/uKlIX4jcL0Y/m/nKf8oezDBAAJ with
>> the same error, but I believe I correctly set ATSHOMERELOC
>>
>> Any idea what I’m missing?
>>
>>
>> --
> You received this message because you are subscribed to a topic in the
> Google Groups "ats-lang-users" group.
> To unsubscribe from this topic, visit
> https://groups.google.com/d/topic/ats-lang-users/W62cWGzt0AI/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to
> ats-lang-users+unsubscr...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/87cbe011-5997-4d96-a439-2522ced8e8adn%40googlegroups.com
> <https://groups.google.com/d/msgid/ats-lang-users/87cbe011-5997-4d96-a439-2522ced8e8adn%40googlegroups.com?utm_medium=email_source=footer>
> .
>

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/CAL-Unv9pvBNQtcQwK_wJ-wVdzmS-2HmnmZzKLr_SoTKonBVPmA%40mail.gmail.com.

Building ATS2 from Github head.

[Steinway Wu]

Hi, 

It seems the documentation at 
https://github.com/githwxi/ATS-Postiats/wiki/Building-and-installing as 
well as scripts at 
https://github.com/ats-lang/ats-lang.github.io/blob/master/SCRIPT/C9-ATS2-install-latest.sh
 
are outdated. I’m trying both and encountered link errors. 

Here’s what I did.

# installing ats1
wget …
./configure —prefix=…
make all_ngc
make install

# installing ats2
git clone …
export ATSHOME=… 
export ATSHOMERELOC=ATS-0.2.12 
make -f Makefile_devl

The errors I see is undefined reference to symbols like 
_2root_2parts_2ats1_2build_2libatsdoc_... Using nm to view the symbols of 
libatsdoc.a, I can see they are named like ATS_2d0_2e2_2e12_2libatsdoc_... 
instead. 

There was a post 
https://groups.google.com/g/ats-lang-users/c/uKlIX4jcL0Y/m/nKf8oezDBAAJ with 
the same error, but I believe I correctly set ATSHOMERELOC

Any idea what I’m missing? 


-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/c393eec2-72fc-49c6-a065-b95c62482a61n%40googlegroups.com.

Re: Temptory Docs Website

[Steinway Wu]

That’s awesome! 

-- 
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+unsubscr...@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/1eeaf73a-4a8f-41a8-ac7e-8c71ecfe9f80%40googlegroups.com.

Re: Linear lazy stream, $ldelay, and freeing a single element.

[Steinway Wu]

I was playing with a utility library based on type classes, implemented as 
templates. As you mentioned, I experienced "interface explosion". For 
things like a fold, or a fmap, I have a t@ype version that is probably 
garbage collected, a vt@ype version that is call-by-value, and a vt@ype 
version that consumes the resources which seems to be the only possible 
version for lazy linear types. Is it theoretically possible to introduce 
some way of doing sort scheme? So one doesn't need to specify any specific 
base sorts?

On Sunday, May 6, 2018 at 2:16:28 PM UTC-4, gmhwxi wrote:
>
> Yes. Should probably use some more informative syntax in ATS3.
>
>
>
>

-- 
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+unsubscr...@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/1ee4e0ba-9e8b-46a2-ad8e-3043063389ba%40googlegroups.com.

Re: Linear lazy stream, $ldelay, and freeing a single element.

[Steinway Wu]

And the `free` method is defined to be the second argument of $ldelay? Is 
that understanding correct?

On Sunday, May 6, 2018 at 12:19:55 AM UTC-4, gmhwxi wrote:
>
>
> A linear stream is a bit like an object with two methods:
> one for eval and the other for free; !xs calls the eval method
> and ~xs calls the free method.
>
>
>

-- 
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+unsubscr...@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/d0d3115a-0dd9-463e-bb26-3a9a18c8c44d%40googlegroups.com.

Re: Linear lazy stream, $ldelay, and freeing a single element.

[Steinway Wu]

I have a follow up question. How does `~xs` as in `$ldelay(..., ~xs)` 
handle a stream of linear elements, or even linear closures? 

On Saturday, May 5, 2018 at 11:23:33 PM UTC-4, Steinway Wu wrote:
>
> Oh, there's a gfree_val and gfree_ref
>
> On Saturday, May 5, 2018 at 11:01:16 PM UTC-4, gmhwxi wrote:
>>
>> Is there a template called gfree? You can put gfree(x) there.
>> For non-linear x,
>>
>> implement(a:t@ype) gfree(x) = ().
>>
>> On Saturday, May 5, 2018 at 10:51:34 PM UTC-4, Steinway Wu wrote:
>>>
>>> Hi, 
>>>
>>> Even though `stream_vt (a)` is defined on `a: vt@ype`, many library 
>>> functions for `stream_vt (a)` is only defined on `a: t@ype`. It feels like 
>>> `a: t@ype` is easier to work with since there's no need to free a single 
>>> element in some of the library functions, like `stream_vt_make_cons`. Is 
>>> there other reasons not to support an element of some true view type? What 
>>> should I put in the 2nd arg in `$ldelay` if I'd like to implement 
>>> `stream_vt_make_cons` for `a: vt@ype`? 
>>>
>>

-- 
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+unsubscr...@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/b113df86-f9da-4ecf-9781-4eb0ef83dad3%40googlegroups.com.

Re: Linear lazy stream, $ldelay, and freeing a single element.

[Steinway Wu]

Oh, there's a gfree_val and gfree_ref

On Saturday, May 5, 2018 at 11:01:16 PM UTC-4, gmhwxi wrote:
>
> Is there a template called gfree? You can put gfree(x) there.
> For non-linear x,
>
> implement(a:t@ype) gfree(x) = ().
>
> On Saturday, May 5, 2018 at 10:51:34 PM UTC-4, Steinway Wu wrote:
>>
>> Hi, 
>>
>> Even though `stream_vt (a)` is defined on `a: vt@ype`, many library 
>> functions for `stream_vt (a)` is only defined on `a: t@ype`. It feels like 
>> `a: t@ype` is easier to work with since there's no need to free a single 
>> element in some of the library functions, like `stream_vt_make_cons`. Is 
>> there other reasons not to support an element of some true view type? What 
>> should I put in the 2nd arg in `$ldelay` if I'd like to implement 
>> `stream_vt_make_cons` for `a: vt@ype`? 
>>
>

-- 
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+unsubscr...@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/0dba6dfd-46df-43ab-bf99-ee3b39ae35f4%40googlegroups.com.

Linear lazy stream, $ldelay, and freeing a single element.

[Steinway Wu]

Hi, 

Even though `stream_vt (a)` is defined on `a: vt@ype`, many library 
functions for `stream_vt (a)` is only defined on `a: t@ype`. It feels like 
`a: t@ype` is easier to work with since there's no need to free a single 
element in some of the library functions, like `stream_vt_make_cons`. Is 
there other reasons not to support an element of some true view type? What 
should I put in the 2nd arg in `$ldelay` if I'd like to implement 
`stream_vt_make_cons` for `a: vt@ype`? 

-- 
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+unsubscr...@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/5dfad156-1e0f-47e7-890b-e91c3f4c2bfc%40googlegroups.com.

Re: Templates and Closures

[Steinway Wu]

Well, I sort of find a way around, that is to write a eta-expanded version 
that is a template. So the template get's invoked right before it is used 
to generate a closure. https://glot.io/snippets/f0pf8h25o9


On Thursday, May 3, 2018 at 8:05:28 PM UTC-4, Steinway Wu wrote:
>
> Hi, 
>
> If a put a template function invocation inside a closure function, it 
> seems that the template is resolved at the closure definition time. I know 
> one way to work around this is to use templates all the way, and replace 
> closures with something like `foobar$fwork`. But is there another way of 
> doing so while keeping the closures? Is there something like an anonymous 
> template and corresponding type for 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-users+unsubscr...@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/a497b45c-9cd4-43c8-a959-384442e490e2%40googlegroups.com.

Re: Nix

[Steinway Wu]

Cool! I just learned about Nix recently, and it looks (at first glance, at 
least) promising. Do you (or Brandon)  have any experiences comparing 
packaging individual ATS libraries using NPM vs using Nix? 

On Tuesday, May 1, 2018 at 11:29:29 PM UTC-4, Artyom Shalkhakov wrote:
>
> Hi Steinway,
>
> These days Brandon Barker maintains ATS packages for NixOS:
>
>
> https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/compilers/ats2/default.nix
>
> You can install ATS2 as follows
>
> $ nix-env -i ats2
>
> I used to have a separate environment for ATS2 development on my laptop. 
> Nothing fancy, just ATS2, binutils and the like. For me, Docker provides a 
> much simpler approach.
>
>
>

-- 
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+unsubscr...@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/576d8977-57a5-4618-ae45-c9b1c1e5fef9%40googlegroups.com.

Re: Template-based implementation for functors

[Steinway Wu]

I actually just tried it, and it works with `[n:nat] List (a, n)`. See 
https://glot.io/snippets/f0nf39m7lk.

On Tuesday, May 1, 2018 at 11:59:32 PM UTC-4, Steinway Wu wrote:
>
> Oh I see. But anyway, here's a monad type class. Just for the record. 
>
> https://glot.io/snippets/f0nejek645
>
>
> On Tuesday, May 1, 2018 at 11:27:29 PM UTC-4, gmhwxi wrote:
>>
>>
>> This approach can only handle simple type constructors like list and 
>> maybe.
>> It would not handle List defined as follows:
>>
>> typedef List(a:t@ype) = [n:nat] List(a, n)
>>
>>

-- 
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+unsubscr...@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/9b3f1afa-9508-4fbf-b969-ef0984699834%40googlegroups.com.

Re: Template-based implementation for functors

[Steinway Wu]

Hi Hongwei and August, 

https://glot.io/snippets/f0nd233vde

I have this functor code working without any "name" hack. @Hongwei, did you 
make any improvements on templates to make it happen? Or am I missing 
something? And btw, glot.io is still running ATS 0.2.11. 

On Wednesday, March 29, 2017 at 10:38:00 AM UTC-4, gmhwxi wrote:
>
>
> If we box everything, then implementing functors (as is defined in 
> Haskell) is straightforward
> in ATS. However, for performance, one may not want to box everything. I 
> sketched a template-based
> implementation for functors as follows:
>
>
> https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/MISC/tempfunctor.dats
>
> It should be fun and very useful to support linear functors (e.g., 
> List0_vt).
>
> Cheers!
>
> --Hongwei
>
>
>

-- 
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+unsubscr...@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/56284850-c51f-4474-b5ae-445e93960a53%40googlegroups.com.

ATS-Redis

[Steinway Wu]

Hi all, 

I just updated the ats-redis bindings to work with the latest hiredis. 
https://github.com/steinwaywhw/ats-redis
It is a binding at its bare minimum, but still useful. Pull requests are 
welcomed.  

Npm package is on the way. I did something wrong and need to wait 24hr 
before I can publish 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-users+unsubscr...@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/70b7e956-bc1c-4d7b-8798-2627efb75153%40googlegroups.com.

Re: ATS3: ATS/Xanadu

[Steinway Wu]

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 around 
the symbols to define it, and use the symbol without parenthesis to invoke 
it. I hope ATS3 can have better support for first-class user-defined 
operators without relying on overloading.

// something like this for any infix operators would be nice
fun (?op) (arg1:type1, arg2:type2): type3 = ...

val x = y ?op z // use it as infix op by default
val x = (?op)(y, z) // temporarily use it as prefix op



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 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 have in mind regarding ATS3.
>
> I know that a lot of people have been complaining about the syntax of 
> ATS2. So
> we can start the effort of designing some "nice" syntax for ATS3. Please 
> feel free
> to post here if you would like share your opinions and ideas.
>
> I will be happy to take the lead but we definitely need to have some form 
> of community
> effort on this project given its size and scope.
>
> Cheers!
>
> --Hongwei
>
> PS: I felt rushed every time up to now when implementing ATS. This time I 
> am hoping
> to have the luxury of thinking about implementation a bit before actually 
> doing 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-users+unsubscr...@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/07fc31bd-21c0-4d84-bed0-283bd9b40fb8%40googlegroups.com.

Re: Intro to ATS - How to code productively

[Steinway Wu]

Hi Artyom, 

Yes, I think it's good :)

(Sorry for the delay. I was offline for the past week. )

On Monday, April 2, 2018 at 1:48:19 AM UTC-4, Artyom Shalkhakov wrote:
>
>
> Hi Steinway,
>
> On Sunday, April 1, 2018 at 11:39:34 PM UTC+6, Steinway Wu wrote:
>>
>> Hi Artyom, 
>>
>> This is awesome :)
>>
>> Thanks!
>  
>
>> I have a question about "gradual improvement" of performance. I 
>> personally feels it is more about gradual improvement of specification, 
>> e.g. change a simple data type into a more refined type, to catch more 
>> bugs. So the sales pitch is more like "write dirty code that works first, 
>> and then sit down and formally specify what the code should do", at least 
>> to me. What do you think? 
>>
>>
> Well, I guess the two views are complementary! I was actually thinking 
> about non-linear data type to linear data type to be a refinement -- is 
> this not  considered the usual meaning? I wasn't actually thinking of 
> "refinement" in a technical sense.
>
> I changed the phrasing somewhat:
>
>
>>- gradual improvement: no need to put a lot of effort upfront, write 
>>dirty code that works, and then sit down and improve efficiency and 
>>correctness (either or both, you have the tools!)
>>
>> Is this any better?
>
> Also I would like to point out abstract types. It's a great way to work 
>> out a system in a top-down fashion. We craft some abstract types, then 
>> provide a set of functions that works on values of these types (like a 
>> DSL), and program using these functions. We can quickly prototype the idea 
>> using the type checker, and defer the implementation details to a later 
>> point. C can probably do this via pointers or structs, but then you need to 
>> think about the details of a struct. 
>>
>>
> Indeed! This is certainly the way to go.
>  
>
>> On Saturday, March 31, 2018 at 7:49:39 AM UTC-4, Artyom Shalkhakov wrote:
>>>
>>> Hi Lance,
>>>
>>> I've put this 
>>> <https://gist.github.com/ashalkhakov/16cf939ba5a7e91cc68733c0441c029b> 
>>> together.
>>>
>>> What do you think? And the rest of the group? This is mostly aimed at C 
>>> programmers.
>>>
>>> On Thursday, March 29, 2018 at 1:48:45 AM UTC+6, Lance Galletti wrote:
>>>>
>>>> Awesome thank you! Looking forward to it! :)
>>>>
>>>> On Wednesday, March 28, 2018 at 12:00:14 PM UTC-4, Artyom Shalkhakov 
>>>> wrote:
>>>>>
>>>>> On Wednesday, March 28, 2018 at 9:34:37 PM UTC+6, Lance Galletti wrote:
>>>>>>
>>>>>> Hi Artyom!
>>>>>>
>>>>>> Thank you for your feedback! It is great to hear an advanced 
>>>>>> programmer's perspective on the appeal of ATS. If you have the time it 
>>>>>> would be great to incorporate into the write-up a section about this! :)
>>>>>>
>>>>>>
>>>>> I wouldn't call myself an advanced programmer, but I've been 
>>>>> interested in ATS programming for a lot of time, that's true.
>>>>>
>>>>> I'll write a sales-pitch. It's really exciting stuff (to me, at 
>>>>> least!).
>>>>>  
>>>>>
>>>>>> So far I have been just putting together what I have learned from 
>>>>>> Hongwei's classes and books but I will definitely be checking out HtDP - 
>>>>>> thank you for the suggestion!
>>>>>>  
>>>>>>
>>>>>
>>>>>> On Wednesday, March 28, 2018 at 3:13:37 AM UTC-4, Artyom Shalkhakov 
>>>>>> wrote:
>>>>>>>
>>>>>>> Hi Lance,
>>>>>>>
>>>>>>> On Tuesday, March 27, 2018 at 9:40:55 PM UTC+6, Lance Galletti wrote:
>>>>>>>>
>>>>>>>> Hi ats users!
>>>>>>>>
>>>>>>>> I recently had the opportunity to give a talk at a hackathon about 
>>>>>>>> ATS and coding productivity / quality. I thought I would share my 
>>>>>>>> slides 
>>>>>>>> here:
>>>>>>>>
>>>>>>>>
>>>>>>>> https://docs.google.com/presentation/d/157VR0oQNTfUiiChYdbv77PYZkYKo_zkZfwRiqGv6sEY/edit?usp=sharing
>>>>>>>>
>>>>>>>> And the informal writ

Re: Theoretical underpinnings for ATS's type system

[Steinway Wu]

Hi Brandon, 

ATS, as formulated in http://www.ats-lang.org/MYDATA/ATSfoundation.pdf, is 
proven sound. See Section 3. ATS with theorem-proving is proven sound by 
proof erasure, in Section 4. 
As far as I know, the soundness is proven directly, following the 
traditional approach of Progress + Preservation through canonical forms, 
substitution lemma, etc. 

I believe there are definitely impredicativity in ATS, although my 
understanding is very vague. 
In the static term language, there's quantifiers, and there's functions. 
You can quantify over static functions. You can also put a quantified term 
as a static function argument. 
I feel like these are something impredicative. 

On Wednesday, March 7, 2018 at 10:33:26 AM UTC-5, Brandon Barker wrote:
>
> Hi All,
>
> I just realized that I hadn't been seeing many ATS messages recently 
> (really, none for months), so I'm sad that I missed them but excited to see 
> that I have a lot to go through (to start, I may take a half vacation day 
> ...), and will try to get my e-mail sorted out...
>
> I'm trying to learn a bit more about type systems these days from the 
> theoretical side (I do not have a background in PL, so I've a lot pick up 
> as yet). I would like to know the theoretical underpinnings of ATS. Sorry 
> if my following questions do not make sense. My ATS is a bit rusty, though 
> I hope to remedy that soon. 
>
> First, can ATS (or any version of it) be proven sound? I noticed there was 
> a lot of emphasis on proving Dotty ("Scala 3") is sound by embedding its 
> type system in System F_<:, I believe. I guess that since ATS is based on 
> ML, it can (or parts of it can) be encoded in System_F (though if only 
> parts, I guess this doesn't necessarily guarantee the type system is 
> consistent).
>
> Mentioning System F and variants, can one construct impredicative types, 
> i.e, Type contains itself. If v:T then T:Type, but does Type:Type work? 
> This would seeming make ATS great for dealing with category theoretic 
> applications. I understand supporting this relates to the need for 
> higher-order (higher-kinded?) polymorphism, and if ATS supports it, I'd be 
> grateful for a pointer to the appropriate documentation.
>
> Best,
>
>

-- 
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+unsubscr...@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/359c5578-0a8e-4e2a-985e-f39336c2f127%40googlegroups.com.

Re: ATS3: ATS/Xanadu

[Steinway Wu]

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 
knob, or annotate the literal, to switch among interpretations. 
2. Some meta-programming supports via templates. E.g. `derive` of Haskell. 
3. Formalization of templates.
4. Module systems. 
5. Session types :)
6. Modular design of the whole tool chain. E.g. parsing, type equality, 
constraints solving, template dispatch, type erasure, etc. 
7. Maybe database-based compilations? We can store compiled blocks as a 
(hash, binary IR) pairs in some file-based databases, for easy reuse. Not 
sure how feasible it is. 
8. Interpreter, REPL, language servers, documentation tools, standard 
libraries, type inference, etc. 
9. More importantly, a process for open source contribution. 

Exciting!

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 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 have in mind regarding ATS3.
>
> I know that a lot of people have been complaining about the syntax of 
> ATS2. So
> we can start the effort of designing some "nice" syntax for ATS3. Please 
> feel free
> to post here if you would like share your opinions and ideas.
>
> I will be happy to take the lead but we definitely need to have some form 
> of community
> effort on this project given its size and scope.
>
> Cheers!
>
> --Hongwei
>
> PS: I felt rushed every time up to now when implementing ATS. This time I 
> am hoping
> to have the luxury of thinking about implementation a bit before actually 
> doing 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-users+unsubscr...@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/73f8357d-fdd7-4949-8515-6cd2abe96e1a%40googlegroups.com.

Re: Static Templates

[Steinway Wu]

I was trying to add some "derive" functionality by representing datatypes, 
say "a" with some generic datatype, say "rep (a)". However, for a generic 
function to work on a value of type "rep (a)", we need the type information 
for the actual values stored in the original value of type "a" (which are 
copied into the value of type "rep (a)"). 

It's much like trying to print a heterogeneous list, generically. I need to 
supply the print function with the actual type of every element. Thus I 
think I probably need the type info to be a template, so that the user can 
instantiate it for every datatype they want to be generic. 

Am I on the right track? Are there other ways of doing it? 

On Saturday, October 21, 2017 at 4:26:02 PM UTC-4, gmhwxi wrote:
>
> I don't know how to do it,
>
> This gets into the domain of meta-programming.
>
> In general, it is very difficult to do meta-programming in a typeful
> manner.  Often one tries to write code to generate code that may
> contain type-error and then apply typechecking to the generated code.
>
> On Friday, October 20, 2017 at 5:45:45 PM UTC-4, Steinway Wu wrote:
>>
>> Hi, 
>>
>> We now have dynamic templates, parameterized by static terms. Is it 
>> possible to have some simple form of static templates like the followings? 
>> Or is there any other way to make static functions ad-hoc polymorphic? 
>>
>> datasort typelist =
>> | tnil of ()
>> | tcons of (t@ype, typelist)
>>
>> #define :: tcons
>>
>> datatype OneConstructor = One of (int, int, string)
>> datatype AnotherConstructor = Another of (int, int, bool)
>>
>> template stacst Code: typelist
>>
>> implement Code = int :: int :: string :: tnil
>> implement Code = int :: int :: bool :: tnil
>>
>>
>>
>>
>>
>>
>>

-- 
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+unsubscr...@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/94b5a0fb-1f06-4f47-adb3-ab1ccb464ae7%40googlegroups.com.

Re: Best way to handle short-living linear objects

[Steinway Wu]

I guess you can define \cross and * as functions that consumes the linear 
list and return a new one? 

On Friday, October 20, 2017 at 10:11:00 AM UTC-4, Russoul wrote:
>
> Let's treat `list_vt(a,n)` as algebraic vector of dim 'n'. Then let's 
> perform some operations on a bunch of them:
>
> (*pseudocode*)
> ...
> val a = $list_vt(1,0,0)
> val b = $list_vt(0,1,0)
> val c = a \cross b
> val d = c * PI
> ...
> val _ = free a
> val _ = free b
> val _ = free c
> val _ = free d
> (*end of code fragment*)
>
> Cleaning(freeing) after simple algebraic operations in the above example 
> is tedious. And I suppose it can become a real pain in math extensive code.
> What is the way out ?
>
>

-- 
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+unsubscr...@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/c0605c82-f53e-4434-857e-3a194a852a2b%40googlegroups.com.

Re: Deech's talk and slides from StrangeLoop 2017

[Steinway Wu]

Hi Aditya, 

Your talk is also featured on *The Verge*! Congratulations!

https://www.theverge.com/2017/10/2/16404152/strange-loop-2017-programming-talks-youtube


On Monday, October 2, 2017 at 3:02:03 AM UTC-4, Artyom Shalkhakov wrote:
>
> Seen on reddit:
>
>
> https://www.reddit.com/r/programming/comments/73lhj0/a_not_so_gentle_introduction_to_systems/
>
> Also see the discussion on r/rust:
>
>
> https://www.reddit.com/r/rust/comments/73j4p5/a_not_so_gentle_introduction_to_systems/
>
> Cheers!
>

-- 
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+unsubscr...@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/083634af-3b91-4c56-ab17-0a281e4cd8aa%40googlegroups.com.

Re: Deech's talk and slides from StrangeLoop 2017

[Steinway Wu]

Hi Aditya, 

Great talk! You did a great job presenting a difficult system in a 
easy-to-understand way :)

Just wanna point out a detail. Proofs are dynamic terms (of sort "prop"). 
So they are not really "type-level". But I guess it is ok to say 
"type-level" in the talk since they will be erased after proof-checking and 
you didn't really go into the details about the proof language. 

Again, thank you very much for the presentation!

On Monday, October 2, 2017 at 11:18:38 AM UTC-4, aditya siram wrote:
>
> No problem. ATS is a great language! Feedback welcome.
>
> On Monday, October 2, 2017 at 8:42:57 AM UTC-5, gmhwxi wrote:
>>
>>
>> This is really good publicity for ATS :)
>>
>> Thanks!!!
>>
>> On Monday, October 2, 2017 at 3:02:03 AM UTC-4, Artyom Shalkhakov wrote:
>>>
>>> Seen on reddit:
>>>
>>>
>>> https://www.reddit.com/r/programming/comments/73lhj0/a_not_so_gentle_introduction_to_systems/
>>>
>>> Also see the discussion on r/rust:
>>>
>>>
>>> https://www.reddit.com/r/rust/comments/73j4p5/a_not_so_gentle_introduction_to_systems/
>>>
>>> Cheers!
>>>
>>

-- 
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+unsubscr...@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/074a63a6-cf40-491f-b83f-7ba5f2887e05%40googlegroups.com.

pandoc supports ATS syntax highlighting

[Steinway Wu]

Hey friends, 

I just came across this, 
https://github.com/jgm/skylighting/blob/master/xml/ats.xml, when I was 
writing a latex documents indirectly by using markdown/pandoc. I found that 
Pandoc natively supports ATS syntax highlighting, which generates pretty 
LaTex/PDF files. That's AMAZING! I don't know who is the original author of 
that syntax file, but this pearl definitely worth sharing with anyone who 
uses pandoc.  

:)

-- 
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+unsubscr...@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/71d5489e-27f6-43ca-b335-100b2b69f415%40googlegroups.com.

Re: Adding join patterns to ATS

[Steinway Wu]

I didn't know Join-calculus before, but this definitely looks interesting 
to me. It seems that it can encode pi-calculus to some degree, but I 
haven't fully investigate that paper. But just for your information, ATS 
supports session types which I think is relevant here. You may want to have 
a look at session type related examples, 
http://ats-lang.sourceforge.net/EXAMPLE/EFFECTIVATS/.

On Wednesday, December 21, 2016 at 4:23:57 PM UTC-5, Ian MathWiz wrote:
>
> I've seen some other feature/roadmap ideas on this list, so I assume this 
> is the place for those. If it's not, please let me know.
>
> I've been using ML-based languages for almost a year now, and there are 
> two such languages that I've particularly grown to love. The first is, of 
> course, ATS. The second is a language called JoCaml 
> , which is a language that augments OCaml with a 
> construction for concurrency and distributed programs called the join 
> pattern.
>
> While I'm aware that ATS has pthreads, I think join patterns have a number 
> of advantages that warrant their inclusion as features in the language. 
> First, join patterns are highly intuitive and elegant, and it's quite 
> simple to spawn and consume new processes. Second, while threads are highly 
> efficient for use with imperative programming, join patterns blend 
> seamlessly with functional programming. (For an example of this, as well as 
> a neat introduction to join patterns, see this paper 
> .) Third, the join calculus 
> is practical to use in distributed systems. This is because it doesn't 
> contain some constructs in other process calculi that are difficult to 
> implement without the client-server model. Personally, I think being able 
> to create distributed systems with ATS would help it see greater adoption, 
> as these applications are going to get more widely used in the future.
>
> I'm currently trying to figure out the difficulties in implementing these 
> in ATS. JoCaml compiles to OCaml bytecode, while ATS compiles to C, so I'm 
> not entirely sure how efficiently these can be implemented in ATS. Also, if 
> we use the same syntax as used in JoCaml, "def" "reply" and "spawn" would 
> become keywords, while "&" and "or" would acquire a different meaning than 
> the logical ones they already have. Anyway, let me know what you think of 
> this suggestion.
>
> Also, while I'm on the subject of OCaml languages, I had another question: 
> what would the difficulty be in implementing OCaml-style objects in ATS? 
> Would they break the type system?
>
> Regards,
> Ian
>

-- 
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+unsubscr...@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/301df497-b0e6-463c-823f-4745390816dd%40googlegroups.com.

Re: Ask/Answer ATS-related questions on StackOverflow

[Steinway Wu]

yes... but not a big issue though. hope we could have more people 
interested in ATS and ask questions there. 

On Sunday, October 16, 2016 at 7:02:43 AM UTC-4, Kiwamu Okabe wrote:
>
> On Sun, Oct 16, 2016 at 3:20 AM, gmhwxi  wrote: 
> > http://stackoverflow.com/tags/ats/info 
>
> I think the "ats" tag has some noise, because the same tag is used by 
> iOS for "App Transport Security". 
>
>   Apple will require HTTPS connections for iOS apps by the end of 2016 
> | TechCrunch 
>   
> https://techcrunch.com/2016/06/14/apple-will-require-https-connections-for-ios-apps-by-the-end-of-2016/
>  
>
> So sad... 
> -- 
> Kiwamu Okabe at METASEPI DESIGN 
>

-- 
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+unsubscr...@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/08802d1e-f4ce-428c-9723-584e6076d790%40googlegroups.com.

Sublime Text - Build/Type Check with hot key

[Steinway Wu]

Hi,

https://gist.github.com/steinwaywhw/27d8fbb569cf178d08d9465aa92c741e

I’m sharing my SublimeText script for building/typechecking ATS files.
After loading this plugin, and filling the blanks, press the hotkey for
Build (on mac, it is cmd+b/cmd+shift+b), it will compile/typecheck the
program.

Hope it helps.

-- 
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+unsubscr...@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/CAL-Unv9g6xa%2BrkJsN1FVxY0DMboWWkgvqyQmA7_h6u_Gpn0eZQ%40mail.gmail.com.

A demo of Union/Find algorithm in ATS

[Steinway Wu]

Hi,

I was reading a chapter about type inference and constraint solving in ML.
It mentioned a quick Union/Find algorithm for testing equivalent classes. I
translate the code into ATS, and pasted here at [glot.io: Union/Find](
https://glot.io/snippets/eiaoq3icf1)

Just for fun.

-- 
Steinway Wu
Sent with Airmail

-- 
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+unsubscr...@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/CAL-Unv8hPLdK%2BXePPCo%2BnfKY81iUc2oHxMaOFm3sH1q%2BLazaaQ%40mail.gmail.com.

Re: glot.io, a code pastebin that can also run your code, now supports ATS.

[Steinway Wu]

Sure, it is merged. It will be published in the next deployment.

On Monday, May 9, 2016 at 9:57:03 AM UTC-4, gmhwxi wrote:
>
> It is here:
>
>
> https://github.com/githwxi/ATS-Postiats/blob/master/doc/PROJECT/MEDIUM/ats2langweb/theLogo/theLogo.png
>
> On Mon, May 9, 2016 at 9:52 AM, Steinway Wu <stein...@gmail.com 
> > wrote:
>
>> Sure, but where can I find the source file for the logo?
>>
>> On Saturday, May 7, 2016 at 5:28:38 PM UTC-4, gmhwxi wrote:
>>>
>>> Could you also make ATS logo shown in the entry for ATS?
>>>
>>> On Saturday, May 7, 2016 at 2:18:45 PM UTC-4, Steinway Wu wrote:
>>>>
>>>> Hi, 
>>>>
>>>> I recently came across glot.io, an online service that lets you run 
>>>> and share snippets. It is open source, so I took the opportunity to add 
>>>> support for our ATS programming language. They use docker image to run ATS 
>>>> code, and the image I provide contains not only ATS, but also 
>>>> erlang/elixir/z3 and make. You have all the freedom to play with a lot of 
>>>> fun stuff in that setting. What's also cool is they provide the ability to 
>>>> embed the snippets as a nice little widget/iframe, while keeping your 
>>>> files 
>>>> editable and runnable!
>>>>
>>>> I posted a proof for the admissibility of cut in intuitionistic logic 
>>>> here https://glot.io/snippets/eegppgnisi, and you can actually run it 
>>>> and check the proof using ATS/z3.
>>>>
>>>> Some links:
>>>>
>>>>- glot.io project page on github: 
>>>>
>>>> https://github.com/prasmussen/glot/wiki/Instructions-for-adding-a-new-language-to-glot.io
>>>>- ATS docker container: 
>>>>https://github.com/steinwaywhw/docker-ats/blob/master/Dockerfile
>>>>
>>>>
>>>>
>>>> -- 
>> 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/16047368-20e9-4e94-9a68-5846e16443c2%40googlegroups.com
>>  
>> <https://groups.google.com/d/msgid/ats-lang-users/16047368-20e9-4e94-9a68-5846e16443c2%40googlegroups.com?utm_medium=email_source=footer>
>> .
>>
>
>

-- 
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+unsubscr...@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/9a4105b3-47ae-4c70-8909-201b5dacb2c5%40googlegroups.com.

Re: glot.io, a code pastebin that can also run your code, now supports ATS.

[Steinway Wu]

Sure, but where can I find the source file for the logo?

On Saturday, May 7, 2016 at 5:28:38 PM UTC-4, gmhwxi wrote:
>
> Could you also make ATS logo shown in the entry for ATS?
>
> On Saturday, May 7, 2016 at 2:18:45 PM UTC-4, Steinway Wu wrote:
>>
>> Hi, 
>>
>> I recently came across glot.io, an online service that lets you run and 
>> share snippets. It is open source, so I took the opportunity to add support 
>> for our ATS programming language. They use docker image to run ATS code, 
>> and the image I provide contains not only ATS, but also erlang/elixir/z3 
>> and make. You have all the freedom to play with a lot of fun stuff in that 
>> setting. What's also cool is they provide the ability to embed the snippets 
>> as a nice little widget/iframe, while keeping your files editable and 
>> runnable!
>>
>> I posted a proof for the admissibility of cut in intuitionistic logic 
>> here https://glot.io/snippets/eegppgnisi, and you can actually run it 
>> and check the proof using ATS/z3.
>>
>> Some links:
>>
>>- glot.io project page on github: 
>>
>> https://github.com/prasmussen/glot/wiki/Instructions-for-adding-a-new-language-to-glot.io
>>- ATS docker container: 
>>https://github.com/steinwaywhw/docker-ats/blob/master/Dockerfile
>>
>>
>>
>>

-- 
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+unsubscr...@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/16047368-20e9-4e94-9a68-5846e16443c2%40googlegroups.com.