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

2016-05-07 Thread Steinway Wu
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/ed7a507d-91e6-4647-b51c-f180969af73a%40googlegroups.com.


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

2016-05-09 Thread 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.


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

2016-05-10 Thread 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  > 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&utm_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: ifcase-expressions

2016-05-23 Thread Steinway Wu
This is cool!

On Sunday, May 22, 2016 at 12:24:21 AM UTC-4, gmhwxi wrote:
>
>
> ATS2 now supports ifcase-expressions, which are similar to
> the if-expressions in Erlang. Here is an example:
>
> //
> fun
> acker
> {m,n:nat}
> ..
> (
>   m: int(m)
> , n: int(n)
> ) : intGte(0) =
> (
> ifcase
> | m = 0 => n + 1
> | n = 0 => acker(m-1, 1)
> | _(*else*) => acker(m-1, acker(m, n-1))
> // end of [ifcase]
> )
> //
>
> Note that the ifcase-expression in the above code is equivalent
> to the following one:
>
> if m=0 then n+1 else if n=0 then acker(m-1, 1) else acker(m-1, acker(m, 
> n-1))
>

-- 
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/d36821e9-432d-4137-b039-bf7c36b776c4%40googlegroups.com.


#ats tag wiki on StackOverflow

2016-06-11 Thread Steinway Wu
Hi, I just created a tag wiki for ATS on stackoverflow, in case anyone post 
relevant questions there. 

http://stackoverflow.com/tags/ats/info

-- 
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/848ca67c-ed07-43f7-a2f6-d19671d0a49d%40googlegroups.com.


Re: Declaring a static constant with an external name

2016-06-30 Thread Steinway Wu
This is so cool!

On Wednesday, June 29, 2016 at 1:24:12 PM UTC-4, gmhwxi wrote:
>
>
> In ATS2-0.2.8, a static constant can now be declared with an external name:
>
> For instance:
>
> stacst sine_of_real : real -> real = "ext#sin"
>
> This is useful when constraints generated during typechecking are to be 
> exported
> for solving externally. If a static constant is given an external name, 
> then the external
> name is used in exported constraints (otherwise, a name like 
> sine_of_real!12345 is
> used, where 12345 is the stamp attached to the static constant).
>
> Here are some examples that you can try (using the given Makefile):
>
>
> https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST
>
> 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/f86554cd-a6f2-4bb0-a641-5504b2011c93%40googlegroups.com.


A demo of memorizing functions in ATS

2016-07-10 Thread Steinway Wu
Hi, 

In a practice, I encountered a problem of memorizing functions. Given a 
function `f`, a memorized version of `f`, called `memo f` should cache the 
results of `f` applying on some `input`. I tried a demo here 
https://glot.io/snippets/egflakau5h, which shows a generic implementation 
of the function `memo0` (for memorizing a function of no arguments) and 
`memo1` (for memorizing a function with one argument). Comments are 
welcomed.

-- 
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/19db82d7-1c14-41cf-8125-bd039497e742%40googlegroups.com.


Re: A demo of memorizing functions in ATS

2016-07-10 Thread Steinway Wu
Thanks, I forgot to save it after debug. Now it works. 

On Sunday, July 10, 2016 at 9:38:49 PM UTC-4, gmhwxi wrote:
>
> Please change
>
> memo1
>
> to
>
> memo1
>
> Also, please delete the line "staload .../gorder_int.dats"
>
> On Sunday, July 10, 2016 at 9:15:10 PM UTC-4, Steinway Wu wrote:
>>
>> Hi, 
>>
>> In a practice, I encountered a problem of memorizing functions. Given a 
>> function `f`, a memorized version of `f`, called `memo f` should cache the 
>> results of `f` applying on some `input`. I tried a demo here 
>> https://glot.io/snippets/egflakau5h, which shows a generic 
>> implementation of the function `memo0` (for memorizing a function of no 
>> arguments) and `memo1` (for memorizing a function with one argument). 
>> Comments are welcomed.
>>
>

-- 
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/adda145a-e119-4431-b72b-b948702fa13f%40googlegroups.com.


Linear component may be abandoned.

2016-07-14 Thread Steinway Wu
Hi, 

In `stream_vt.dats`, I saw the following snippets,

fun {a:vt0p} {b:vt0p} stream_vt_map_con (xs: stream_vt (a)) : stream_vt_con 
(b) = let
val xs_con = !xs
in
case+ xs_con of
| @stream_vt_cons(x, xs) => let
val y = stream_vt_map$fopr (x) // fopr is of type {a,b:vt@ype} 
&a >> a?! -> b
val xs = xs
val () = free@ (xs_con)
  in
stream_vt_cons{b}(y, stream_vt_map (xs))
  end 
| ~stream_vt_nil((*void*)) => stream_vt_nil()
end


and I have three questions. 

1. what is a?! 
2. why fopr takes &a, instead of just a?
3. what happened when val xs = xs 

Thanks, 

-- 
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/a443c141-c62d-49a3-88d9-68ab64640cbb%40googlegroups.com.


Thinking about moving this group to Discourse.

2016-07-14 Thread Steinway Wu
Hi friends, 

I'm thinking about moving Google Group to a self-hosted Discourse. 

Discourse is an online discussion kit, http://www.discourse.org, very much 
like a forum version of Stack Overflow. It's founded by the founder of 
StackOverflow. 

I think it is beneficial for several reasons. 

1. It promotes better organization of topics through "category". 
2. It has a better editor for writing posts. It supports several formats 
including markdown, code snippets, and link preview. I think those features 
promotes a better way of presenting ideas/questions/tutorials. 
3. It has a better search functionality, though not just search, but also 
inter-post links, that make archived posts alive again. 
4. It support "wiki" post, which means a post can be collaboratively 
edited. This may be useful for examples/tutorials and other discussions. 
5. It also have support for reply-from-email, new-topic-through-email, and 
subscripting to new topics in email. It needs some configuration on the 
server side, but it should make transition from mailing list easier. 
6. It comes with other cool features too, like plugins and APIs.
7. It is founded by CodingHorror, one of the founder of StackOverflow. I 
consider that as trustworthy. 
8. and it looks cool. :) just kidding. 

There official website provides a better advertisement about their product. 

Downside being

1. Need to be self-hosted. There is a maintenance cost, both time and 
efforts. Currently it is hosted on a school machine (VM). 
2. Although having a good support of email, it is still considered 
web-centric. That being said, pure terminal email-list users may feel 
uncomfortable using it. 
3. Google group messages can be ported into Discourse, but it's currently 
not easy to sync back to Google group, unless someone develop some 
Discourse bots to do the sync upon events. That being said, the transition 
has to be a clean cut. 

That's my initial thoughts on this. I took some time and setup a demo 
sandbox at http://ats-lang.steinwaywu.com. If you are interested, please 
take a look and post whatever you want to test it out. Also, you can try 
out at their official sandbox https://try.discourse.org If you want to try 
something that needs more trust level, just leave a message here and I will 
do it. Please register using the same email address as here in Google Group 
so that your old post will link to your profile. It is a just sandbox for 
you to try out and let me collect feedbacks, I will eventually *delete* all 
posts and re-import Google group posts if you think Discourse is a good 
idea. 

Comments, suggestions, critics, any thoughts are welcomed. Please post 
feedback here in the Google groups. 

Thank you!


-- 
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/1cc5f533-bef6-4fb5-ab08-b6686d6f6182%40googlegroups.com.


Re: Linear component may be abandoned.

2016-07-14 Thread Steinway Wu
What about this? Let the worker function consume a. And in map, free the 
constructor, instead of unfold the constructor. 

fun {a,b:vt@ype} stream_vt_map_con (xs: stream_vt a): stream_vt_con b
fun {a,b:vt@ype} stream_vt_map$fopr (a - b): b



On Thursday, July 14, 2016 at 10:39:08 AM UTC-4, gmhwxi wrote:
>
> 1.
>
> When [a] is a linear type, a?! is only the data part of [a] (that is, 
> there is no view in a?!).
> When [a] is non-linear, then a?! is just [a].
>
> 2. When [a] is large (containing many bytes), call-by-reference can be 
> more efficient. The convention
> in ATS is to use call-by-reference when linear data is handled.
>
> 3. The 'xs' on the right-hand side is a variable (with address); its 
> content needs to be taken out before free@ can be called.
>
>
>
>
> On Thu, Jul 14, 2016 at 9:20 AM, Steinway Wu <> wrote:
>
>> Hi, 
>>
>> In `stream_vt.dats`, I saw the following snippets,
>>
>> fun {a:vt0p} {b:vt0p} stream_vt_map_con (xs: stream_vt (a)) : 
>> stream_vt_con (b) = let
>> val xs_con = !xs
>> in
>> case+ xs_con of
>> | @stream_vt_cons(x, xs) => let
>> val y = stream_vt_map$fopr (x) // fopr is of type {a,b:vt@ype} 
>> &a >> a?! -> b
>> val xs = xs
>> val () = free@ (xs_con)
>>   in
>> stream_vt_cons{b}(y, stream_vt_map (xs))
>>   end 
>> | ~stream_vt_nil((*void*)) => stream_vt_nil()
>> end
>>
>>
>> and I have three questions. 
>>
>> 1. what is a?! 
>> 2. why fopr takes &a, instead of just a?
>> 3. what happened when val xs = xs 
>>
>> Thanks, 
>>
>> -- 
>>
>>
>

-- 
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/f72cd27d-4084-41b6-a6fe-b94a7e3e1563%40googlegroups.com.


Re: Embedding differential equations into types

2016-07-16 Thread Steinway Wu
I'm a little confused. This is solved using z3, not using dReal, right? So 
what's the relation with dReal/dReach here? 

On Monday, June 13, 2016 at 6:08:13 PM UTC-4, gmhwxi wrote:
>
> The directory is renamed as follows:
>
>
> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/CPS/DREACH/SCRATCH/bouncing_ball
>
> Also, the constraints can now be solved if they are passed to patsolve_z3.
>
> On Wednesday, May 11, 2016 at 11:39:09 PM UTC-4, gmhwxi wrote:
>>
>> I skipped the constraint-solving part, which needs to be exported to Z3.
>>
>> On Wednesday, May 11, 2016 at 11:36:34 PM UTC-4, Artyom Shalkhakov wrote:
>>>
>>> On Thursday, May 12, 2016 at 5:56:56 AM UTC+6, gmhwxi wrote:

 Adding a 2d-oscillator example:


 http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/oscillator/

 http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/oscillator/oscillator_2d_anim.html


>>> What's this for?
>>>
>>> prval () =
>>>   $UN.prop_assert{false}()
>>>
>>>
>>>
>>> Is it asserting falsity?
>>>
>>> On Wednesday, May 11, 2016 at 7:54:58 PM UTC-4, gmhwxi wrote:
>
> Renaming Github to GitHub:
>
>
> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/
>
> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_anim.html
>
> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_with_drag_anim.html
>
>
> On Saturday, May 7, 2016 at 3:50:21 PM UTC-4, gmhwxi wrote:
>>
>>
>> I'd like to report an interesting example of using types in ATS.
>>
>> Here are two animations of bouncing balls:
>>
>>
>> http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/
>>
>> http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_anim.html
>>
>> http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_with_drag_anim.html
>>
>> The graphics is uninteresting. What is interesting here is that the 
>> differential equations governing the movement of the ball are
>> captured in the ATS types.
>>
>> 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/7a8d6b55-f8a2-4c0c-802e-c1bb48b36ac8%40googlegroups.com.


Re: Embedding differential equations into types

2016-07-17 Thread Steinway Wu
I see. Thanks!

On Saturday, July 16, 2016 at 11:58:44 PM UTC-4, gmhwxi wrote:
>
> In this case, the constraints do not involve transcendental functions 
> (sin, cos, exp, etc.).
> Once you have transcendental functions (and beyond), there is very little 
> that z3 can do.
> The hope is that dReal can be used to solve such constraints effectively 
> in practice.
>
> On Saturday, July 16, 2016 at 11:53:42 PM UTC-4, Steinway Wu wrote:
>>
>> I'm a little confused. This is solved using z3, not using dReal, right? 
>> So what's the relation with dReal/dReach here? 
>>
>> On Monday, June 13, 2016 at 6:08:13 PM UTC-4, gmhwxi wrote:
>>>
>>> The directory is renamed as follows:
>>>
>>>
>>> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/CPS/DREACH/SCRATCH/bouncing_ball
>>>
>>> Also, the constraints can now be solved if they are passed to 
>>> patsolve_z3.
>>>
>>> On Wednesday, May 11, 2016 at 11:39:09 PM UTC-4, gmhwxi wrote:
>>>>
>>>> I skipped the constraint-solving part, which needs to be exported to Z3.
>>>>
>>>> On Wednesday, May 11, 2016 at 11:36:34 PM UTC-4, Artyom Shalkhakov 
>>>> wrote:
>>>>>
>>>>> On Thursday, May 12, 2016 at 5:56:56 AM UTC+6, gmhwxi wrote:
>>>>>>
>>>>>> Adding a 2d-oscillator example:
>>>>>>
>>>>>>
>>>>>> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/oscillator/
>>>>>>
>>>>>> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/oscillator/oscillator_2d_anim.html
>>>>>>
>>>>>>
>>>>> What's this for?
>>>>>
>>>>> prval () =
>>>>>   $UN.prop_assert{false}()
>>>>>
>>>>>
>>>>>
>>>>> Is it asserting falsity?
>>>>>
>>>>> On Wednesday, May 11, 2016 at 7:54:58 PM UTC-4, gmhwxi wrote:
>>>>>>>
>>>>>>> Renaming Github to GitHub:
>>>>>>>
>>>>>>>
>>>>>>> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/
>>>>>>>
>>>>>>> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_anim.html
>>>>>>>
>>>>>>> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_with_drag_anim.html
>>>>>>>
>>>>>>>
>>>>>>> On Saturday, May 7, 2016 at 3:50:21 PM UTC-4, gmhwxi wrote:
>>>>>>>>
>>>>>>>>
>>>>>>>> I'd like to report an interesting example of using types in ATS.
>>>>>>>>
>>>>>>>> Here are two animations of bouncing balls:
>>>>>>>>
>>>>>>>>
>>>>>>>> http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/
>>>>>>>>
>>>>>>>> http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_anim.html
>>>>>>>>
>>>>>>>> http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_with_drag_anim.html
>>>>>>>>
>>>>>>>> The graphics is uninteresting. What is interesting here is that the 
>>>>>>>> differential equations governing the movement of the ball are
>>>>>>>> captured in the ATS types.
>>>>>>>>
>>>>>>>> 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/8a958078-8a5e-48a5-88ea-720cf0ce9fd4%40googlegroups.com.


StackOverflow Documentation Beta

2016-07-21 Thread Steinway Wu
Hi, @Hongwei

I received an ad from StackOverflow, introducing their "Documentation" 
feature in beta, here http://stackoverflow.com/tour/documentation. It seems 
useful for us, too. You can have a look. 

It needs at least five requests for the #ats tag to allow us to create 
documents. Anyone interested is welcomed to click the following link to 
help make it happen. http://stackoverflow.com/documentation/ats/commit

-- 
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/7b480df3-ce69-4a19-9b72-569e0b9be3c9%40googlegroups.com.


Re: Pats2xhtmlization as a service

2016-08-01 Thread Steinway Wu
Neat!

On Monday, July 25, 2016 at 12:58:55 PM UTC-4, gmhwxi wrote:
>
>
> I am thinking about building some on-line services for easing the
> use of the ATS programming language system. For the moment,
> I managed to finish one that supports syntax-hiliting for ATS code:
>
> http://www.ats-lang.org/Resources.html#Pats2xhtmlization_service
>
> Basically, one can now readily include ATS code in HTML and then
> activate the service to syntax-hilite the code. In the near future, I would
> like to support similar services for typechecking and compilting ATS code.
>
> 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/5b24f212-5459-44b6-9ba3-1acab19b5476%40googlegroups.com.


ATS Tutorials

2016-08-05 Thread Steinway Wu
Hi, 

Following up on Hongwei's *ats-as-a-service*, I wrote a pandoc plugin for 
automating some of the tasks of writing interactive ats tutorials, shown 
here https://steinwaywhw.github.io/ats-tutorials/. If you a familiar with 
pandoc, then my small script is just a pandoc filter in python, that takes 
in a code block in original markdown input, and turn it into interactive or 
just highlighted html snippets. 

The project home page https://steinwaywhw.github.io/ats-tutorials/ itself 
is rendered using this plug-in. Hope it is useful for anyone who want to 
write code-related webpages. Contributions are welcomed. The tool is MIT 
licensed. 

-- 
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/85d5c38e-492d-4a60-b8dc-3911a7061d6f%40googlegroups.com.


Re: ATS Tutorials

2016-08-05 Thread Steinway Wu
Sadly, there is a https related issue. I hope to fix it soon... for now, it 
works with Safari at least. I'm not particularly familiar of how to work 
with http requests in a https served pages. Any one has any idea? Please 
let me know. Thanks.

On Friday, August 5, 2016 at 3:12:42 PM UTC-4, Steinway Wu wrote:
>
> Hi, 
>
> Following up on Hongwei's *ats-as-a-service*, I wrote a pandoc plugin for 
> automating some of the tasks of writing interactive ats tutorials, shown 
> here https://steinwaywhw.github.io/ats-tutorials/. If you a familiar with 
> pandoc, then my small script is just a pandoc filter in python, that takes 
> in a code block in original markdown input, and turn it into interactive or 
> just highlighted html snippets. 
>
> The project home page https://steinwaywhw.github.io/ats-tutorials/ itself 
> is rendered using this plug-in. Hope it is useful for anyone who want to 
> write code-related webpages. Contributions are welcomed. The tool is MIT 
> licensed. 
>

-- 
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/824c4be2-de3a-42f1-82b2-d47564808a29%40googlegroups.com.


exception and sats file

2016-08-10 Thread Steinway Wu
Hi, 

When I define an exception in SATS file `exn.sats`, I need to compile it 
like `patscc *.dats *exn.sats*` to have the symbol defined. However, when I 
define a normal datatype in some sats file, I usually can compile it by 
indicating only those DATS files, like `patscc *.dats`. Why are they 
different?

Thanks,

-- 
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/77da8592-57a7-4ea1-9338-ab48a35b5f28%40googlegroups.com.


Template and Effect

2016-08-11 Thread Steinway Wu
Hi, 

I'm trying to implement `gcompare_val_val` for a datatype `list`, but 
encounters an error saying "some disallowed effects may be incurred: 1"

```
datatype list (a:t@ype) = ...

fun {a:t@ype} list_compare ...

implement (a) gcompare_val_val (x, y) = list_compare (x, y)
```

What is that effect? And how should I implement that template for `list a`? 

Thanks,

-- 
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/c4495032-e055-4cda-8d5f-45fa34d23838%40googlegroups.com.


Template and Overloading

2016-08-12 Thread Steinway Wu
Hi, 

Is it possible to do overloadings like below?

```
fun {a:t@ype} gcomapre_val_val (a, a): int

symintr compare
overload compare with gcompare_val_val 
overload compare with gcompare_val_val 
```

I'm asking this since this. Say, we have a dummy `mycompare`

```
fun {a:t@ype} mycompare (a, a): int
implement {a} mycompare (x, y) = gcompare_val_val (x, y)

symintr comapre
overload compare with mycompare 
```

Then ATS seems to have a hard time figuring out template variables when 
instantiating. 
Whenever we use `compare`, we have to specify fully what type it is. I'm 
thinking if

```
overload compare with mycompare
overload compare with mycompare
``` 

could help in any way?

-- 
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/246342e5-b458-4e30-ad6b-adad7615e893%40googlegroups.com.


Re: Template and Effect

2016-08-12 Thread Steinway Wu
This definitely works. but I don't think list_compare has any effect. 
Explicitly marking list_comare as (a, a):<> int seems to do the job as well

On Thursday, August 11, 2016 at 5:21:01 PM UTC-4, gmhwxi wrote:
>
>
> Try:
>
> implement (a) gcompare_val_val (x, y) = $effmask_all( list_compare 
> (x, y) )
>
>
>
> On Thu, Aug 11, 2016 at 2:03 PM, Steinway Wu <> wrote:
>
>> Hi, 
>>
>> I'm trying to implement `gcompare_val_val` for a datatype `list`, but 
>> encounters an error saying "some disallowed effects may be incurred: 1"
>>
>> ```
>> datatype list (a:t@ype) = ...
>>
>> fun {a:t@ype} list_compare ...
>>
>> implement (a) gcompare_val_val (x, y) = list_compare (x, y)
>> ```
>>
>> What is that effect? And how should I implement that template for `list 
>> a`? 
>>
>> Thanks,
>>
>> -- 
>>
>

-- 
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/ba49d192-c9a5-481f-b9c6-3e9e757d6612%40googlegroups.com.


Re: Template and Overloading

2016-08-12 Thread Steinway Wu
I saw 
this, https://bluishcoder.co.nz/2011/10/19/overloading-functions-in-ats.html, 
which describes the same thing I would like to do. But those examples no 
longer work.

On Friday, August 12, 2016 at 12:13:12 PM UTC-4, Steinway Wu wrote:
>
> Hi, 
>
> Is it possible to do overloadings like below?
>
> ```
> fun {a:t@ype} gcomapre_val_val (a, a): int
>
> symintr compare
> overload compare with gcompare_val_val 
> overload compare with gcompare_val_val 
> ```
>
> I'm asking this since this. Say, we have a dummy `mycompare`
>
> ```
> fun {a:t@ype} mycompare (a, a): int
> implement {a} mycompare (x, y) = gcompare_val_val (x, y)
>
> symintr comapre
> overload compare with mycompare 
> ```
>
> Then ATS seems to have a hard time figuring out template variables when 
> instantiating. 
> Whenever we use `compare`, we have to specify fully what type it is. I'm 
> thinking if
>
> ```
> overload compare with mycompare
> overload compare with mycompare
> ``` 
>
> could help in any way?
>

-- 
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/c3897ba8-5d60-4d9a-bdfe-2a95bc89e1ed%40googlegroups.com.


Re: Template and Overloading

2016-08-15 Thread Steinway Wu
Black magic... Why does it work?

On Friday, August 12, 2016 at 6:09:40 PM UTC-4, gmhwxi wrote:
>
> Try:
>
>
> fun{a:t@ype}
>
> mycompare(INV(a), a): int
>
>
> Sent from my T-Mobile 4G LTE device
>
>
> ------ Original message--
>
> *From: *Steinway Wu
>
> *Date: *Fri, Aug 12, 2016 12:13 PM
>
> *To: *ats-lang-users;
>
> *Subject:*Template and Overloading
>
>
> Hi, 
>
> Is it possible to do overloadings like below?
>
> ```
> fun {a:t@ype} gcomapre_val_val (a, a): int
>
> symintr compare
> overload compare with gcompare_val_val 
> overload compare with gcompare_val_val 
> ```
>
> I'm asking this since this. Say, we have a dummy `mycompare`
>
> ```
> fun {a:t@ype} mycompare (a, a): int
> implement {a} mycompare (x, y) = gcompare_val_val (x, y)
>
> symintr comapre
> overload compare with mycompare 
> ```
>
> Then ATS seems to have a hard time figuring out template variables when 
> instantiating. 
> Whenever we use `compare`, we have to specify fully what type it is. I'm 
> thinking if
>
> ```
> overload compare with mycompare
> overload compare with mycompare
> ``` 
>
> could help in any way?
>
>
>

-- 
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/df0f6ef4-3b9a-4829-a80e-fb320082385d%40googlegroups.com.


Re: Lexical format for floating-point constants

2016-08-16 Thread Steinway Wu
Great job! 

On Tuesday, August 16, 2016 at 3:58:28 AM UTC-4, Artyom Shalkhakov wrote:
>
> On Tuesday, August 16, 2016 at 11:15:51 AM UTC+6, gmhwxi wrote:
>>
>> This is great news!
>>
>> I really want to try it for my upcoming class.
>>
>> Could you show me how to use the Monaco editor to
>> replace the textareas in the following page:
>>
>> http://myflask-tutoriats.rhcloud.com/assign01
>> view-source:http://myflask-tutoriats.rhcloud.com/assign01
>>
>
> Sure! I will see if I can do something ASAP. (Pretty busy with other stuff 
> lately...)
>
>
>>
>> Thanks!
>>
>> On Tuesday, August 16, 2016 at 12:07:35 AM UTC-4, Artyom Shalkhakov wrote:
>>>
>>> The PR adding ATS/Postiats colorization support to Monaco editor has 
>>> been merged.
>>>
>>> On Thursday, June 30, 2016 at 9:17:56 AM UTC+6, Artyom Shalkhakov wrote:

 On Wednesday, June 29, 2016 at 9:54:39 AM UTC+6, gmhwxi wrote:
>
>
> Thanks for the effort!
>
> These days I have been thinking about building some sort of on-line 
> coding
> system of ATS. The manaco editor looks pretty decent. When your syntax 
> definition
> is ready, I will give it a try.
>


 I'm currently in the process of writing unit-tests (caught a bug with a 
 comment already!).

 It's taking quite some time. Will let you know if something fruitful 
 comes out of it.
  

>
> On Monday, June 27, 2016 at 11:58:42 AM UTC-4, Artyom Shalkhakov wrote:
>>
>> Thanks Hongwei! I will take a look to see if this is what my syntax 
>> definition captures tomorrow.
>>
>> Here's the code, in a gist:
>>
>> https://gist.github.com/ashalkhakov/a86dfb4770cff12d0cdf298405a58d74
>>
>> It can be tested by visiting:
>>
>> https://microsoft.github.io/monaco-editor/monarch.html
>>
>> and pasting the syntax definition into the textbox. I've also 
>> provided an example input (some rubbish to help figure out if hilighting 
>> is 
>> well-behaved).
>>
>> This needs more testing and tuning, but seems like a worthwhile 
>> effort!
>>
>> On Monday, June 27, 2016 at 9:20:16 PM UTC+6, gmhwxi wrote:
>>>
>>>
>>> Let
>>>
>>> INT0 = [0-9]*
>>> INT1 = (0 | [1-9](INT0))
>>> DOT = [.]
>>> EXP = [eE](INT1)
>>>
>>> Then FLOAT is
>>>
>>> (INT1)(EXP) | (INT1)(DOT)(INT0)(EXP)? | (DOT)(INT1)(EXP)?
>>>
>>> There are also hexadecimal floating point numbers:
>>>
>>> HEX0 = [0-9a-z]*
>>> HEX1 = (0 | [1-9a-z](HEX0))
>>> DOT = [.]
>>> EXP = [pP](INT1)
>>>
>>> HEXFLOAT = (HEX1)(EXP) | (HEX1)(DOT)(HEX0)(EXP?) | (DOT)(HEX1)(EXP?)
>>>
>>> In C, EXP? should be EXP for hexadecimal floating point numbers.
>>>
>>> On Monday, June 27, 2016 at 4:06:42 AM UTC-4, Artyom Shalkhakov 
>>> wrote:

 I'm doing a syntax highlighter for ATS based on the Monarch editor 
 (used in Visual Studio Code) and I'm interested to know what's the 
 lexical 
 grammar for floating-point constants?

 I've tried looking through the lexer source code, but I find it 
 quite complicated. I'd like some help on this one.

>>>

-- 
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/635fdde2-e35b-4cca-9f08-4c8a35b4ae9a%40googlegroups.com.


A demo of Union/Find algorithm in ATS

2016-09-09 Thread 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: A demo of Union/Find algorithm in ATS

2016-09-09 Thread Steinway Wu
Updated, thanks!

On Friday, September 9, 2016 at 7:07:55 PM UTC-4, gmhwxi wrote:
>
>
> I suggest:
>
> fun{} addr_of{a:t@ype} (pt a): ptr
>
> Casting a pointer(64bit) to an integer(32bit) is a bit dangerous.
>
>
> On Friday, September 9, 2016 at 5:36:35 PM UTC-4, Steinway Wu wrote:
>>
>> 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/d98740ad-66e4-4aaf-bb4e-4d150cdb0996%40googlegroups.com.


Share a Link: a Lisp Machine

2016-09-09 Thread Steinway Wu
Just share a link from hacker news, a lisp machine.

http://www.technoblogy.com/show?1GX1

-- 
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-Unv9ZnJZdjo1Snimq%3DA1-KbSdSeptgV9YNc6jo31B9kXU3A%40mail.gmail.com.


Sublime Text - Build/Type Check with hot key

2016-10-06 Thread 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.


Re: Ask/Answer ATS-related questions on StackOverflow

2016-10-16 Thread 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.


Re: Adding join patterns to ATS

2016-12-22 Thread 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: Adding join patterns to ATS

2016-12-22 Thread Steinway Wu
Since you already have some experience with JoCaml, would you mind sharing 
some code examples, or slides that you have? I would like to learn more 
about it. 

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/7d98649d-f296-408f-92f6-6ab5d3c4ee72%40googlegroups.com.


Re: Support in ATS for using external packages

2017-01-06 Thread Steinway Wu
I just played with it on my ats-utils package. I published it 
here, https://www.npmjs.com/package/ats-utils so that others can try out. 
It is under MIT license. 

On Tuesday, January 3, 2017 at 2:45:09 PM UTC-5, gmhwxi wrote:
>
>
>
> ##
> #
> # For the moment, I am using ats-lang-users for ats-lang-devel.
> #
> ##
>
> For people interested in this, please feel free to post your comments.
>
> In the near future, I hope to set up a packaging system for ATS. It is
> long overdue.
>
> I looked around and tried npm (JS) and composer (PHP). For the moment,
> I plan to use npm (but this choice should have minimal impact, if at all, 
> on
> the support for packaging system in ATS).
>
> One can say that being explicit is a theme in the design of ATS. There is
> no exception this time. A environment variable PATSHOMERELOCS is to
> be introduced (which may or may not replace the variable PATSHOMERELOC
> that is currently in use).
>
> PATSHOMERELOCS is essentially a collection of paths separation by colon (:)
> (or other characters).
>
> Say that you have used npm to install a package FOO globally. Then you may 
> have
>
> /usr/local/lib/node_modules/
> FOO
>
> on your system.
>
> Please make sure that /usr/local/lib/node_modules is one of the paths in 
> PATSHOMERELOCS.
>
> You may use FOO in your code in the following ways:
>
> #include "${PATSHOMERELOCS}/FOO/foo.hats"
> #staload "${PATSHOMERELOCS}/FOO/foo.sats"
> #staload _ = "${PATSHOMELOCS}/FOO/foo.hats"
>
> By mentioning PATSHOMERELOCS in a loading path is what I refer to as being 
> explicit.
>
> This should address the issue of compilation to C involving external 
> packages. Obviously, we also
> need to compile the generated C code into object files. This latter issue 
> can be addressed by making
> use of pkg-config properly. We just need some experiments and then form 
> certain guidelines for doing it.
>
> 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/fe68ffd2-83ae-4b4c-9d79-cb6fe5991625%40googlegroups.com.


Re: Support in ATS for using external packages

2017-01-19 Thread Steinway Wu
It seems that the change breaks the build of ATS-Postiats-contrib. I can no 
longer compile atscc2js/2erl/2clj etc. It can not find source files any 
more and reporting errors like ".PATSRELOCROOT-$USER/SATS/json.sats is not 
available". 

On Tuesday, January 3, 2017 at 2:45:09 PM UTC-5, gmhwxi wrote:
>
>
>
> ##
> #
> # For the moment, I am using ats-lang-users for ats-lang-devel.
> #
> ##
>
> For people interested in this, please feel free to post your comments.
>
> In the near future, I hope to set up a packaging system for ATS. It is
> long overdue.
>
> I looked around and tried npm (JS) and composer (PHP). For the moment,
> I plan to use npm (but this choice should have minimal impact, if at all, 
> on
> the support for packaging system in ATS).
>
> One can say that being explicit is a theme in the design of ATS. There is
> no exception this time. A environment variable PATSHOMERELOCS is to
> be introduced (which may or may not replace the variable PATSHOMERELOC
> that is currently in use).
>
> PATSHOMERELOCS is essentially a collection of paths separation by colon (:)
> (or other characters).
>
> Say that you have used npm to install a package FOO globally. Then you may 
> have
>
> /usr/local/lib/node_modules/
> FOO
>
> on your system.
>
> Please make sure that /usr/local/lib/node_modules is one of the paths in 
> PATSHOMERELOCS.
>
> You may use FOO in your code in the following ways:
>
> #include "${PATSHOMERELOCS}/FOO/foo.hats"
> #staload "${PATSHOMERELOCS}/FOO/foo.sats"
> #staload _ = "${PATSHOMELOCS}/FOO/foo.hats"
>
> By mentioning PATSHOMERELOCS in a loading path is what I refer to as being 
> explicit.
>
> This should address the issue of compilation to C involving external 
> packages. Obviously, we also
> need to compile the generated C code into object files. This latter issue 
> can be addressed by making
> use of pkg-config properly. We just need some experiments and then form 
> certain guidelines for doing it.
>
> 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/81f2487f-2dd2-49d3-827e-19eb3ec0b662%40googlegroups.com.


Re: (Co)monads in ATS

2017-03-17 Thread Steinway Wu
Great note!

On Thursday, March 16, 2017 at 11:20:54 AM UTC-4, August Alm wrote:
>
> Hi all!
>
> I just wrote down some sketchy thoughts on monads and comonads in ATS. ATS 
> has a very unique type system, so there are (co)monads in ATS that simply 
> do not exist in other languages. I'm wondering if this might be useful. See 
> the attached and let me know if you have ideas.
>
> Best wishes,
> August
>

-- 
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/35dbf704-c858-452f-b6d0-3a2d53b74c12%40googlegroups.com.


pandoc supports ATS syntax highlighting

2017-04-17 Thread 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: pandoc supports ATS syntax highlighting

2017-04-19 Thread Steinway Wu
Wow, thank you Kiwamu, you just made my document looks way more colorful :)

On Tuesday, April 18, 2017 at 2:04:40 AM UTC-4, Artyom Shalkhakov wrote:
>
> On Tuesday, April 18, 2017 at 10:34:48 AM UTC+6, Kiwamu Okabe wrote:
>>
>> Yes :)
>>
>
> Implement silently, don't tell anyone. Have it spring up from an unrelated 
> source. You just made my day, thanks, Kiwamu. :)
>  
>
>>
>> On Apr 18, 2017 7:45 AM, "gmhwxi"  wrote:
>>
>>> author="Kiwamu Okabe (...)" 
>>>
>>> On Monday, April 17, 2017 at 5:32:50 PM UTC-4, Steinway Wu wrote:
>>>>
>>>> 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-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/f294838e-d237-4ce0-956c-f30878fe3674%40googlegroups.com
>>>  
>>> <https://groups.google.com/d/msgid/ats-lang-users/f294838e-d237-4ce0-956c-f30878fe3674%40googlegroups.com?utm_medium=email&utm_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/cc95f263-f814-4d69-afbc-fc4b7fe0ca1f%40googlegroups.com.


Re: Declaring a static constant with an external name

2017-07-04 Thread Steinway Wu
I encountered a problem.

Say I have this in the ATS code

stacst set_emp: set = "ext@smt_set_emp"

and this in the smt2 code

(define-const smt_set_emp (Set) ((as const (Set)) false))

`--constraint-export` is able to translate all static applications of 
`smt_emp` to `smt_set_emp`. 

*However, it emits an extra definition which I don't want to have.* 

(declare-fun smt_set_emp () Set)

What is your usual use case? Maybe we should remove this from emitted code. 

On Wednesday, June 29, 2016 at 1:24:12 PM UTC-4, gmhwxi wrote:
>
>
> In ATS2-0.2.8, a static constant can now be declared with an external name:
>
> For instance:
>
> stacst sine_of_real : real -> real = "ext#sin"
>
> This is useful when constraints generated during typechecking are to be 
> exported
> for solving externally. If a static constant is given an external name, 
> then the external
> name is used in exported constraints (otherwise, a name like 
> sine_of_real!12345 is
> used, where 12345 is the stamp attached to the static constant).
>
> Here are some examples that you can try (using the given Makefile):
>
>
> https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST
>
> 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/0e7c266b-47a6-4890-8180-51bdeb81f43b%40googlegroups.com.


Re: Declaring a static constant with an external name

2017-07-04 Thread Steinway Wu
I put up a PR for your 
consideration. https://github.com/githwxi/ATS-Postiats/pull/170


On Tuesday, July 4, 2017 at 2:47:15 PM UTC-4, Steinway Wu wrote:
>
> I encountered a problem.
>
> Say I have this in the ATS code
>
> stacst set_emp: set = "ext@smt_set_emp"
>
> and this in the smt2 code
>
> (define-const smt_set_emp (Set) ((as const (Set)) false))
>
> `--constraint-export` is able to translate all static applications of 
> `smt_emp` to `smt_set_emp`. 
>
> *However, it emits an extra definition which I don't want to have.* 
>
> (declare-fun smt_set_emp () Set)
>
> What is your usual use case? Maybe we should remove this from emitted 
> code. 
>
> On Wednesday, June 29, 2016 at 1:24:12 PM UTC-4, gmhwxi wrote:
>>
>>
>> In ATS2-0.2.8, a static constant can now be declared with an external 
>> name:
>>
>> For instance:
>>
>> stacst sine_of_real : real -> real = "ext#sin"
>>
>> This is useful when constraints generated during typechecking are to be 
>> exported
>> for solving externally. If a static constant is given an external name, 
>> then the external
>> name is used in exported constraints (otherwise, a name like 
>> sine_of_real!12345 is
>> used, where 12345 is the stamp attached to the static constant).
>>
>> Here are some examples that you can try (using the given Makefile):
>>
>>
>> https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST
>>
>> 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/99550848-6084-4b66-bb3c-4dbaa3104de7%40googlegroups.com.


Re: Deech's talk and slides from StrangeLoop 2017

2017-10-02 Thread 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.


Re: Deech's talk and slides from StrangeLoop 2017

2017-10-02 Thread 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: Best way to handle short-living linear objects

2017-10-20 Thread 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.


Static Templates

2017-10-20 Thread Steinway Wu
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/f3f34dab-0bb7-4c5b-bc7e-c3453315bbdc%40googlegroups.com.


Re: Static Templates

2017-10-22 Thread 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: ATS3: ATS/Xanadu

2018-02-13 Thread 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: Theoretical underpinnings for ATS's type system

2018-03-07 Thread 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: Intro to ATS - How to code productively

2018-04-01 Thread Steinway Wu
Hi Artyom, 

This is awesome :)

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? 

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. 

On Saturday, March 31, 2018 at 7:49:39 AM UTC-4, Artyom Shalkhakov wrote:
>
> Hi Lance,
>
> I've put this 
>  
> 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 write up I am currently developing:
>>
>> https://github.com/galletti94/magnificATS/tree/master/INTRO
>>
>> If, like me, you are passionate about coding quality, methodology, 
>> productivity, or functional programming and, of course ATS, please reach 
>> out!
>>
>>
> First off, I chuckled when I saw the name of the repo. :-)
>
> I want to write something about the C-style programming for ATS, but 
> not quite have the time (or the guts or whatever it is I lack). It would 
> be 
> great to help fellow programmers learn more about ATS!
>  
>
>> I would be happy to collaborate on the write up and hear your 
>> thoughts about what drew YOU to ATS.
>>
>
> I still view ATS as C-with-proper-type-system. :) This is what drew  
> me to ATS: you can write safe, efficient systems-level programs but this 
> will require some theorem proving, bringing this academic discipline 
> close 
> to actual programming practice (or you can cast your way through the 
> types, 
> but then you're the one to blame if things go wrong). ATS helped me to 
> improve my knowledge of C.
>
> Regarding your write-up, have you seen HtDP (How to Design Programs)? 
> Their "design recipes" are somewhat similar IIRC (proceed top-down, 
> refine, 
> state pre- and post-conditions, provide examples of evaluation aka tests).
>
> Looking forward to connecting!
>>
>> Lance Galletti
>> gall...@bu.edu
>>
>>
>>

-- 
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/5da7c3c7-6090-4cb6-932d-8dfcdb66909b%40googlegroups.com.


Re: Intro to ATS - How to code productively

2018-04-11 Thread 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
>>>>>>>>
&g

Re: ATS3: ATS/Xanadu

2018-04-11 Thread 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: Blockchain + Smart Contract in ATS - looking for collaborators

2018-04-28 Thread Steinway Wu
Great work, Lance! You helped me understand what smart contract means :)

On Friday, April 27, 2018 at 12:17:01 PM UTC-4, Lance Galletti wrote:
>
> Hey ATS users!
>
> I recently had the chance to build a blockchain and smart contract 
> language in ATS - all with a nice CLI thanks to 
> https://github.com/ashalkhakov/colorado.
>
> I wrote a small blog post about it here:
>
> https://beta.observablehq.com/@galletti94/functional-blockchain
>
> and am looking for collaborators to take this to the next level. If you 
> would like to help me out with enhancing the language or CLI, or if you 
> have a grand vision / feedback you would like to share, please reach out!
>
> Thank you!
>
> Lance
>

-- 
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/70eca382-4f66-4abb-b72f-2233acb6d153%40googlegroups.com.


Re: ATS3: ATS/Xanadu

2018-04-28 Thread Steinway Wu
Speaking of formalization of templates, I came upon this essay 
http://okmij.org/ftp/Computation/typeclass.html. Personally this is such a 
good read, and I finally understand how type classes are done. I feel like 
our templates is almost "local type class" in Oleg's words, except that ATS 
uses late-binding.  

On Tuesday, February 13, 2018 at 2:52:29 PM UTC-5, Steinway Wu wrote:
>
> 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/895549c8-51c7-4d06-92a1-a99bc1861cef%40googlegroups.com.


Nix

2018-04-30 Thread Steinway Wu
Hi, 

I just noticed that there are some Nix scripts. I never knew we have Nix 
efforts. Could someone provide some insights into the experiences using Nix 
for ATS? Is it working? Does someone maintain a Nix package for ATS? 

-- 
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/cdb0af26-dc72-4955-9ffe-5591d05022e2%40googlegroups.com.


ATS-Redis

2018-05-01 Thread 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: Template-based implementation for functors

2018-05-01 Thread 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.


Re: Template-based implementation for functors

2018-05-01 Thread Steinway Wu
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/c017c5f6-9856-4952-9146-a3f1e8328778%40googlegroups.com.


Re: Template-based implementation for functors

2018-05-01 Thread 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: Nix

2018-05-01 Thread 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.


Templates and Closures

2018-05-03 Thread Steinway Wu
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/97235e35-5712-4528-be37-d12fca30d1b6%40googlegroups.com.


Re: Templates and Closures

2018-05-03 Thread 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: Templates and Closures

2018-05-03 Thread Steinway Wu
I kind of hope there's some sort of `-` besides `-` and 
`-` stuff. Just to mark that this is a template and should be resolved 
later. 

On Thursday, May 3, 2018 at 8:26:28 PM UTC-4, Steinway Wu wrote:
>
> 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/22451dcd-a8d3-4adc-b71c-2482cd621c94%40googlegroups.com.


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

2018-05-05 Thread 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: Linear lazy stream, $ldelay, and freeing a single element.

2018-05-05 Thread 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.


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

2018-05-05 Thread 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.

2018-05-06 Thread 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.

2018-05-06 Thread 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: Temptory Docs Website

2019-06-14 Thread 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.


Building ATS2 from Github head.

2020-12-31 Thread 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: Building ATS2 from Github head.

2020-12-31 Thread 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&utm_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.