Re: Non-consuming linear stream

[gmhwxi]

ost efficient 
>>>> version I could get now:
>>>> ```
>>>> patscc -O2 -DATS_MEMALLOC_LIBC -I"../libs/" -o test7   TEST/test7.dats 
>>>> /run/current-system/sw/bin/time ./test7
>>>> 1077871
>>>> 0.84user 0.01system 0:00.85elapsed 100%CPU (0avgtext+0avgdata 
>>>> 35108maxresident)k
>>>> 0inputs+0outputs (0major+8486minor)pagefaults 0swaps
>>>> ```
>>>> in comparison to haskell's:
>>>> ```
>>>> 1.16user 0.02system 0:01.18elapsed 99%CPU (0avgtext+0avgdata 
>>>> 74492maxresident)k
>>>> 0inputs+0outputs (0major+17827minor)pagefaults 0swaps
>>>> ```
>>>> I have to note, that test4 is more correct than test3: it is the same, 
>>>> except that it is using GC to collect stream()
>>>> ```
>>>> patscc -O2 -DATS_MEMALLOC_GCBDW -lgc -o test4   TEST/test4.dats
>>>> /run/current-system/sw/bin/time ./test4
>>>> 1077871
>>>> 2.13user 0.03system 0:02.13elapsed 101%CPU (0avgtext+0avgdata 
>>>> 97344maxresident)k
>>>> ```
>>>> which is expected to use less memory, but increases time to GC (as 
>>>> expected as well), but, technically, this version is the closest to 
>>>> haskell's one.
>>>>
>>>> for 2^30 constraint:
>>>> ```
>>>> patscc -O2 -DATS_MEMALLOC_LIBC -I"../libs/" -o test7   TEST/test7.dats
>>>> /run/current-system/sw/bin/time ./test7
>>>> 54400028
>>>> 227.79user 0.63system 3:48.43elapsed 99%CPU (0avgtext+0avgdata 
>>>> 1701428maxresident)k
>>>> 0inputs+0outputs (0major+425064minor)pagefaults 0swaps
>>>> ```
>>>> haskell version with GHC8.10:
>>>> ```
>>>> 54400028
>>>> 278.48user 0.62system 4:38.75elapsed 100%CPU (0avgtext+0avgdata 
>>>> 3016564maxresident)k
>>>> 0inputs+0outputs (0major+753319minor)pagefaults 0swaps
>>>> ```
>>>> and test4
>>>> ```
>>>> patscc -O2 -DATS_MEMALLOC_GCBDW -lgc -o test4   TEST/test4.dats
>>>> /run/current-system/sw/bin/time ./test4
>>>> 54400028
>>>> 704.39user 1.81system 11:46.22elapsed 99%CPU (0avgtext+0avgdata 
>>>> 4966216maxresident)k
>>>> 0inputs+0outputs (0major+1241156minor)pagefaults 0swaps
>>>> ```
>>>> I am wondering why test4 performs quite poor(I guess, Boehm GC is just 
>>>> too general/unoptimized), because, I had expected, that GC should free 
>>>> stream_con() instances as soon as they will be converted into 
>>>> stream_vt_con() by stream_t2vt... That is what haskell's GC is doing with 
>>>> intermediate data. I wish I was able to free stream_con() instance 
>>>> forcibly 
>>>> in stream_t2vt(). In this case, I expect it will be on par with haskell (I 
>>>> assume, that qlist is implemented as a flat array (I haven't actually 
>>>> checked, hehe))
>>>>
>>>> Meanwhile: 
>>>> 1. I had started this topic, because Haskell's source code is a good 
>>>> example of composability of lazy evaluation: it is short, but quite 
>>>> powerful as I had spent quite some time to produce an outperforming 
>>>> version 
>>>> which is more difficult as well. Basically, I had to implement memoization 
>>>> using qlist() which is built-in into Haskell's runtime;
>>>> 2. now I have an example of stateful lazy stream processing in ATS2 and 
>>>> it was very interesting as I had the impression that it is hard in ATS to 
>>>> keep an implicit state (as resource usage is harder without GC);
>>>> 3. I have a food for thoughts, because, even if Haskell's version is 
>>>> short but powerful, lazy-by-default evaluation has a side-effect of having 
>>>> to dig and decide what is worse in particular case: code being too lazy or 
>>>> code being too strict. Just a simple example is a `foldr` implementation (
>>>> https://downloads.haskell.org/~ghc/latest/docs/html/libraries/base-4.16.1.0/src/Data.Foldable.html#foldr):
>>>>  
>>>> which requires some time to understand how it is being done. Also it is 
>>>> hard to not to meet 
>>>> https://downloads.haskell.org/~ghc/latest/docs/html/libraries/deepseq-1.4.6.1/Control-DeepSeq.html
>>>>  for 
>>>> forcing evaluation. So Haskell hides laziness but requires understanding 
>>>> how to force evaluation and marshall data to fit GC's expectati

Re: Non-consuming linear stream

[gmhwxi]

I put my ATS2 code here:

https://github.com/githwxi/ATS-Postiats/tree/master/libats/TEST

I will put some code similar to what you did in test5 later. I think that 
test5-style
is going to be faster for a relative small input (e.g., 2^24) but it may 
not be able to
beat test02 for larger input (e.g., 2^30).


On Monday, July 11, 2022 at 8:46:02 AM UTC-4 gmhwxi wrote:

> There is 'qlist' in libats that does what you want.
>
> By using the two-stream approach I mentioned earlier, you can readily get 
> to 2^30:
>
> 54400028
> real18m47.053s
> user18m46.372s
> sys 0m0.424s
>
> (*
> This info is for the number of primes up to 2^28:
>
> ATS2:
> 14630843
> real2m35.548s
> user2m35.532s
> sys 0m0.000s
>
> Haskell (GHC-7.10.3)
> 14630843
> real7m41.733s
> user7m36.208s
> sys 0m1.688s
> *)
>
> I could not get the haskell implementation to finish for 2^30. I had to 
> stop its running once
> its memory usage reached 25% after about 10 minutes (I was monitoring 
> using 'top').
>
>
> On Mon, Jul 11, 2022 at 7:20 AM Dambaev Alexander  
> wrote:
>
>> I had checked some more and was able to make a stateful numbers generator 
>> using list_vt for accumulating of evaluated results here 
>> https://github.com/dambaev/mobt2/blob/master/ats2/src/TEST/test5.dats 
>> but for some reason, it takes forever to complete with default constraint 
>> <= g0int_npow( 2, 24) using linear streams
>>
>> I guess is due to list_vt_extent, which is O(n)
>>
>> I was trying to pass pointer to a tail of the list_vt data to pass 
>> through auxmain/auxmain_con to make extend to be O(1), but I was not able 
>> to satisfy type checker :) So I decided to ask if it is possible to use 
>> such pointer/hole to the tail in the environment of $ldelay?
>>
>> вс, 10 июл. 2022 г. в 03:12, gmhwxi :
>>
>>>
>>> I see.
>>>
>>> By the way, when I tried test1 and test3 on my machine, the latter is 
>>> only about 10% faster than the former.
>>>
>>> It should be easy to have a version in ATS that beats Haskell:
>>>
>>> You first produce a non-linear thePrimes. Then you produce a linear 
>>> thePrimes2 (where isPrime uses thePrimes).
>>> In this way, the memory foot print should be very small. And I bet the 
>>> running time is much faster. Try 2^28 or 2^30 :)
>>>
>>> On Saturday, July 9, 2022 at 10:37:03 PM UTC-4 ice.r...@gmail.com wrote:
>>>
>>>> I will check ATS3 version, meanwhile GHC 8.10 produces much more 
>>>> optimised code:
>>>>
>>>> ```
>>>> [nix-shell:/data/devel/mobt2/haskell]$ ghc --version
>>>> The Glorious Glasgow Haskell Compilation System, version 8.10.7
>>>> [nix-shell:/data/devel/mobt2/haskell]$ ghc -O2 --make app/Main.hs -o 
>>>> haskell
>>>> [1 of 1] Compiling Main ( app/Main.hs, app/Main.o )
>>>> Linking haskell ...
>>>> [nix-shell:/data/devel/mobt2/haskell]$ $(which time) ./haskell
>>>> 1077871
>>>> 1.04user 0.00system 0:01.05elapsed 100%CPU (0avgtext+0avgdata 
>>>> 72140maxresident)k
>>>> 0inputs+0outputs (0major+17298minor)pagefaults 0swaps
>>>> ```
>>>> in comparison to ATS2 versions from repo above:
>>>>
>>>> ```
>>>> [nix-shell:/data/devel/mobt2/ats2/src]$ make
>>>> patscc -O2 -DATS_MEMALLOC_LIBC -I"../libs/" -o test3   TEST/test3.dats
>>>> /run/current-system/sw/bin/time ./test3
>>>> 1077871
>>>> 1.11user 0.01system 0:01.12elapsed 100%CPU (0avgtext+0avgdata 
>>>> 102456maxresident)k
>>>> 0inputs+0outputs (0major+25327minor)pagefaults 0swaps
>>>> patscc -O2 -DATS_MEMALLOC_LIBC -I"../libs/" -o test1   TEST/test1.dats
>>>> /run/current-system/sw/bin/time ./test1
>>>> 1077871
>>>> 2.11user 0.03system 0:02.14elapsed 99%CPU (0avgtext+0avgdata 
>>>> 203448maxresident)k
>>>> 0inputs+0outputs (0major+50589minor)pagefaults 0swaps
>>>> ```
>>>> ie, non-linear version (test1) is twice slower and using 2x memory of 
>>>> test3 (which converts stream into stream_vt). But still, haskell version 
>>>> is 
>>>> faster and using less memory :)
>>>>
>>>> вс, 10 июл. 2022 г. в 02:21, gmhwxi :
>>>>
>>>>> Here is a version I wrote in ATS3:
>>>>>
>>>>>
>>>>> https://github.com/githwxi/ATS-Xanadu/blob/master/xatslib/libcats/T

Re: Non-consuming linear stream

[gmhwxi]

I see.

By the way, when I tried test1 and test3 on my machine, the latter is only 
about 10% faster than the former.

It should be easy to have a version in ATS that beats Haskell:

You first produce a non-linear thePrimes. Then you produce a linear 
thePrimes2 (where isPrime uses thePrimes).
In this way, the memory foot print should be very small. And I bet the 
running time is much faster. Try 2^28 or 2^30 :)

On Saturday, July 9, 2022 at 10:37:03 PM UTC-4 ice.r...@gmail.com wrote:

> I will check ATS3 version, meanwhile GHC 8.10 produces much more optimised 
> code:
>
> ```
> [nix-shell:/data/devel/mobt2/haskell]$ ghc --version
> The Glorious Glasgow Haskell Compilation System, version 8.10.7
> [nix-shell:/data/devel/mobt2/haskell]$ ghc -O2 --make app/Main.hs -o 
> haskell
> [1 of 1] Compiling Main ( app/Main.hs, app/Main.o )
> Linking haskell ...
> [nix-shell:/data/devel/mobt2/haskell]$ $(which time) ./haskell
> 1077871
> 1.04user 0.00system 0:01.05elapsed 100%CPU (0avgtext+0avgdata 
> 72140maxresident)k
> 0inputs+0outputs (0major+17298minor)pagefaults 0swaps
> ```
> in comparison to ATS2 versions from repo above:
>
> ```
> [nix-shell:/data/devel/mobt2/ats2/src]$ make
> patscc -O2 -DATS_MEMALLOC_LIBC -I"../libs/" -o test3   TEST/test3.dats
> /run/current-system/sw/bin/time ./test3
> 1077871
> 1.11user 0.01system 0:01.12elapsed 100%CPU (0avgtext+0avgdata 
> 102456maxresident)k
> 0inputs+0outputs (0major+25327minor)pagefaults 0swaps
> patscc -O2 -DATS_MEMALLOC_LIBC -I"../libs/" -o test1   TEST/test1.dats
> /run/current-system/sw/bin/time ./test1
> 1077871
> 2.11user 0.03system 0:02.14elapsed 99%CPU (0avgtext+0avgdata 
> 203448maxresident)k
> 0inputs+0outputs (0major+50589minor)pagefaults 0swaps
> ```
> ie, non-linear version (test1) is twice slower and using 2x memory of 
> test3 (which converts stream into stream_vt). But still, haskell version is 
> faster and using less memory :)
>
> вс, 10 июл. 2022 г. в 02:21, gmhwxi :
>
>> Here is a version I wrote in ATS3:
>>
>>
>> https://github.com/githwxi/ATS-Xanadu/blob/master/xatslib/libcats/TEST/test02_isPrime.dats
>>
>> Currently, I can only compile the ATS3 code to JS. The generated JS code 
>> runs about 10 times slower
>> than the C code generated from compiling a comparable ATS2 implementation:
>>
>> |thePrimes2| = 1077871
>>
>> real0m23.060s
>> user   0m23.380s
>> sys 0m0.188s
>> On Saturday, July 9, 2022 at 5:33:43 PM UTC-4 gmhwxi wrote:
>>
>>> I took a look. Your ATS code looks very fine to me.
>>>
>>> I did some profiling on my own. In my trials, your ATS code is actually 
>>> a lot faster than
>>> the Haskell code you posted. Note that my ghc version is very old: GHC 
>>> 7.10.3
>>>
>>> ## ATS ##
>>>
>>> (* Your code using non-linear stream *)
>>> hwxi@hongwei-t440p:/tmp$ patscc -O2 -o primes -DATS_MEMALLOC_LIBC 
>>> primes.dats
>>> hwxi@hongwei-t440p:/tmp$ time ./primes
>>> 1077871
>>>
>>> real0m3.118s
>>> user0m3.064s
>>> sys 0m0.048s
>>>
>>> ## Haskell ##
>>> (* Your haskell version *)
>>> (*
>>> Glasgow Haskell Compiler, Version 7.10.3, stage 2 booted by GHC version 
>>> 7.10.3
>>> *)
>>>
>>> hwxi@hongwei-t440p:/tmp$ ghc -O2 primes.hs
>>> Linking primes ...
>>> hwxi@hongwei-t440p:/tmp$ time ./primes
>>> 1077871
>>>
>>> real0m8.195s
>>> user0m8.152s
>>> sys 0m0.040s
>>>
>>> 
>>>
>>> ## ATS ##
>>> (*My version using linear stream that is based on yours*)
>>>
>>> hwxi@hongwei-t440p:/tmp$ patscc -O2 -o primes2 -DATS_MEMALLOC_LIBC 
>>> primes2.dats
>>> hwxi@hongwei-t440p:/tmp$ time ./primes2
>>> 1077871
>>>
>>> real0m2.120s
>>> user0m2.092s
>>> sys 0m0.000s
>>>
>>> On Saturday, July 9, 2022 at 12:50:11 PM UTC-4 ice.r...@gmail.com wrote:
>>>
>>>> My initial motivation was this Haskell source code: 
>>>> https://github.com/dambaev/mobt2/blob/master/haskell/app/Main.hs which 
>>>> is using lazy list (of course) and recursive binding and I decided to 
>>>> check 
>>>> if it will be possible to get something similar
>>>>
>>>> ATS version using non-linear stream is here: 
>>>> https://github.com/dambaev/mobt2/blob/master/ats2/src/TEST/test1.dats 
>>>> , but i

Re: Non-consuming linear stream

[gmhwxi]

Here is a version I wrote in ATS3:

https://github.com/githwxi/ATS-Xanadu/blob/master/xatslib/libcats/TEST/test02_isPrime.dats

Currently, I can only compile the ATS3 code to JS. The generated JS code 
runs about 10 times slower
than the C code generated from compiling a comparable ATS2 implementation:

|thePrimes2| = 1077871

real0m23.060s
user   0m23.380s
sys 0m0.188s
On Saturday, July 9, 2022 at 5:33:43 PM UTC-4 gmhwxi wrote:

> I took a look. Your ATS code looks very fine to me.
>
> I did some profiling on my own. In my trials, your ATS code is actually a 
> lot faster than
> the Haskell code you posted. Note that my ghc version is very old: GHC 
> 7.10.3
>
> ## ATS ##
>
> (* Your code using non-linear stream *)
> hwxi@hongwei-t440p:/tmp$ patscc -O2 -o primes -DATS_MEMALLOC_LIBC 
> primes.dats
> hwxi@hongwei-t440p:/tmp$ time ./primes
> 1077871
>
> real0m3.118s
> user0m3.064s
> sys 0m0.048s
>
> ## Haskell ##
> (* Your haskell version *)
> (*
> Glasgow Haskell Compiler, Version 7.10.3, stage 2 booted by GHC version 
> 7.10.3
> *)
>
> hwxi@hongwei-t440p:/tmp$ ghc -O2 primes.hs
> Linking primes ...
> hwxi@hongwei-t440p:/tmp$ time ./primes
> 1077871
>
> real0m8.195s
> user0m8.152s
> sys 0m0.040s
>
> 
>
> ## ATS ##
> (*My version using linear stream that is based on yours*)
>
> hwxi@hongwei-t440p:/tmp$ patscc -O2 -o primes2 -DATS_MEMALLOC_LIBC 
> primes2.dats
> hwxi@hongwei-t440p:/tmp$ time ./primes2
> 1077871
>
> real0m2.120s
> user0m2.092s
> sys 0m0.000s
>
> On Saturday, July 9, 2022 at 12:50:11 PM UTC-4 ice.r...@gmail.com wrote:
>
>> My initial motivation was this Haskell source code: 
>> https://github.com/dambaev/mobt2/blob/master/haskell/app/Main.hs which 
>> is using lazy list (of course) and recursive binding and I decided to check 
>> if it will be possible to get something similar
>>
>> ATS version using non-linear stream is here: 
>> https://github.com/dambaev/mobt2/blob/master/ats2/src/TEST/test1.dats , 
>> but it takes to much memory as `stream_take_while` duplicates data, as I 
>> have got, that datatype constructor can't be unfolded with `@stream_cons` 
>> pattern match
>>
>> There is another version, that generates primes with non-linear stream 
>> and then, converting it to linear stream 
>> https://github.com/dambaev/mobt2/blob/master/ats2/src/TEST/test3.dats . 
>> This is the closest version to haskell's one. but still is using more space 
>> and as twice as slow as Haskell, so I had started to think of how to 
>> eliminate intermediate data structure.
>>
>> So, not a production issue, hehe, just found an interesting topic to dig 
>> in :)
>>
>> сб, 9 июл. 2022 г. в 11:11, Hongwei Xi :
>>
>>> By looking at your first version, my simple answer is that a linear 
>>> stream cannot be used
>>> in this way. The second version is possible but I am not sure what you 
>>> wanted to do exactly.
>>> If you show me how to use a non-linear stream to do it, then I could 
>>> probably say more.
>>>
>>> On Sat, Jul 9, 2022 at 5:26 AM Dambaev Alexander  
>>> wrote:
>>>
>>>> Hi,
>>>>
>>>> I had tried to implement function of type:
>>>>
>>>> ```
>>>> fun
>>>>   {a:t0p}
>>>>   isPrime
>>>>   ( xs: !stream_vt( int)
>>>>   , x: int
>>>>   ):
>>>>   bool
>>>> ```
>>>>
>>>> Ie, I want to force evaluation of some portion of a stream, but I need 
>>>> to preserve it for a later use. 
>>>>
>>>> I had tried to make a similar version:
>>>> ```
>>>> fun
>>>>   {a:t0p}
>>>>   isPrime
>>>>   ( xs: stream_vt( int)
>>>>   , x: int
>>>>   ):
>>>>   ( stream_vt( int), bool)
>>>> ```
>>>>
>>>> but failed as well, so I decided to ask for a direction if someone had 
>>>> tried to do similar stuff
>>>>
>>>> -- 
>>>> 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 view this discussion on the web visit 
>>>> https://groups.google.com/d/msgid/ats-lang-users/CAHjn2KwFq7JH%2BiZE7bWCJ_L7oZ38K-kmGBFii7DZsdxWLDsGmg

Re: Non-consuming linear stream

[gmhwxi]

I took a look. Your ATS code looks very fine to me.

I did some profiling on my own. In my trials, your ATS code is actually a 
lot faster than
the Haskell code you posted. Note that my ghc version is very old: GHC 
7.10.3

## ATS ##

(* Your code using non-linear stream *)
hwxi@hongwei-t440p:/tmp$ patscc -O2 -o primes -DATS_MEMALLOC_LIBC 
primes.dats
hwxi@hongwei-t440p:/tmp$ time ./primes
1077871

real0m3.118s
user0m3.064s
sys 0m0.048s

## Haskell ##
(* Your haskell version *)
(*
Glasgow Haskell Compiler, Version 7.10.3, stage 2 booted by GHC version 
7.10.3
*)

hwxi@hongwei-t440p:/tmp$ ghc -O2 primes.hs
Linking primes ...
hwxi@hongwei-t440p:/tmp$ time ./primes
1077871

real0m8.195s
user0m8.152s
sys 0m0.040s



## ATS ##
(*My version using linear stream that is based on yours*)

hwxi@hongwei-t440p:/tmp$ patscc -O2 -o primes2 -DATS_MEMALLOC_LIBC 
primes2.dats
hwxi@hongwei-t440p:/tmp$ time ./primes2
1077871

real0m2.120s
user0m2.092s
sys 0m0.000s

On Saturday, July 9, 2022 at 12:50:11 PM UTC-4 ice.r...@gmail.com wrote:

> My initial motivation was this Haskell source code: 
> https://github.com/dambaev/mobt2/blob/master/haskell/app/Main.hs which is 
> using lazy list (of course) and recursive binding and I decided to check if 
> it will be possible to get something similar
>
> ATS version using non-linear stream is here: 
> https://github.com/dambaev/mobt2/blob/master/ats2/src/TEST/test1.dats , 
> but it takes to much memory as `stream_take_while` duplicates data, as I 
> have got, that datatype constructor can't be unfolded with `@stream_cons` 
> pattern match
>
> There is another version, that generates primes with non-linear stream and 
> then, converting it to linear stream 
> https://github.com/dambaev/mobt2/blob/master/ats2/src/TEST/test3.dats . 
> This is the closest version to haskell's one. but still is using more space 
> and as twice as slow as Haskell, so I had started to think of how to 
> eliminate intermediate data structure.
>
> So, not a production issue, hehe, just found an interesting topic to dig 
> in :)
>
> сб, 9 июл. 2022 г. в 11:11, Hongwei Xi :
>
>> By looking at your first version, my simple answer is that a linear 
>> stream cannot be used
>> in this way. The second version is possible but I am not sure what you 
>> wanted to do exactly.
>> If you show me how to use a non-linear stream to do it, then I could 
>> probably say more.
>>
>> On Sat, Jul 9, 2022 at 5:26 AM Dambaev Alexander  
>> wrote:
>>
>>> Hi,
>>>
>>> I had tried to implement function of type:
>>>
>>> ```
>>> fun
>>>   {a:t0p}
>>>   isPrime
>>>   ( xs: !stream_vt( int)
>>>   , x: int
>>>   ):
>>>   bool
>>> ```
>>>
>>> Ie, I want to force evaluation of some portion of a stream, but I need 
>>> to preserve it for a later use. 
>>>
>>> I had tried to make a similar version:
>>> ```
>>> fun
>>>   {a:t0p}
>>>   isPrime
>>>   ( xs: stream_vt( int)
>>>   , x: int
>>>   ):
>>>   ( stream_vt( int), bool)
>>> ```
>>>
>>> but failed as well, so I decided to ask for a direction if someone had 
>>> tried to do similar stuff
>>>
>>> -- 
>>> 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 view this discussion on the web visit 
>>> https://groups.google.com/d/msgid/ats-lang-users/CAHjn2KwFq7JH%2BiZE7bWCJ_L7oZ38K-kmGBFii7DZsdxWLDsGmg%40mail.gmail.com
>>>  
>>> 
>>> .
>>>
>> -- 
>> You received this message because you are subscribed to the Google Groups 
>> "ats-lang-users" group.
>> To unsubscribe from this group and stop receiving emails from it, send an 
>> email to ats-lang-user...@googlegroups.com.
>>
> To view this discussion on the web visit 
>> https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLqp62MaoG8hugJ8h2mUt%2BsSAJ2eu6uRuJ%3D5nMOc4EbcfQ%40mail.gmail.com
>>  
>> 
>> .
>>
>

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/70a43cb2-4f67-414a-b8b0-1a9cef9a5537n%40googlegroups.com.

Re: A vision for future programming in ATS

[gmhwxi]

Here is project for compiling ATS3 to JS:

https://github.com/xanadu-lang/Xats2js-H0

H0 refers to a high-level abstract syntax tree generated by xatsopt, which
mostly does parsing and fixity resolution and binding resolution and 
(non-dependent)
type-checking and template resolution.

I put the code for xatsopt in a git submodule. The compiler from ATS3 to JS 
is referred
to as xats2js, which turns ATS3 code into Javascript code; the obtained JS 
code needs
to be combined with some code for various basic JS functions (which I call 
run-time);
and the code combination is done through copying/pasting code :)

You can try some of the JS code generated by xats2js from ATS3 source:

https://xanadu-lang.github.io/

Cheers!

--Hongwei

PS: Sorry, I won't have time to write a detailed documentation for xats2js. 
However,
if you have high-level (or maybe not so high-level) questions, I will try 
to answer them
to the extent I can.


On Saturday, January 29, 2022 at 2:19:54 PM UTC-5 gmhwxi wrote:

> Hi, there,
>
> HX-2022-01-29:
>
> A vision for future programming in ATS
>
> Before I start, I would like to quote captain Woodrow F. Call,
> a character played by Tommy Lee Jones in Lonesome Dove:
>
> "Man of Vision you say...? Yeah. Hell of a vision." ~ Woodrow Call
>
> By the way, here is the end of the Lonesome Dove miniseries where
> Woodrow Call uttered the above line when interviewed by a reporter:
>
>
> https://www.facebook.com/caldwellwritesdotcom/videos/lonesome-dove-tells-the-story-of-two-friends-who-were-legendary-texas-rangers-an/440279033007270
>
> Ideally, a programming language should be simple and general, and
> it should permit extensive error checking, facilitate proofs of
> program properties such as correctness, and possess a correct and
> efficient implementation. Invariably there will be some conflicts
> among these goals which must be resolved with careful attention to the
> needs of the user. I learned the above from Prof. John Reynolds when I
> was a PhD student at CMU.
>
> ATS3 is not an ordinary programming language. It is more like a
> programming language for support meta-programming of all sorts.
> Suppose we want to have programs written in some language X. Then we
> traditionally write these programs manually in X. ATS3 provides an
> alternative: We can implement a compiler from ATS3 to X to allow us to
> write programs in ATS3 and then compile them to code in X.  In
> practice, we hope to do co-programming with ATS3 and X; code in X
> generated from ATS3 source can be combined with code in X obtained
> otherwise. By programming in ATS3, we can benefit greatly from the
> advanced type-checking that allows many varities of bugs to be flushed
> out at compile-time; we can also benefit greatly from the extensive
> use of templates that allows massive amount of quality code to be
> generated in an automated manner.
>
> In a following post, I will use a concrete example (co-programming
> with ATS3 and Javascript) to outline some of the big steps involved
> in building a compiler to support co-programing with ATS3 and X,
> where X is just a placeholder for some programming language of one's
> choice.
>
> Cheers,
>
> --Hongwei
>
> ##
>
> For previously post messages:
>
> https://github.com/githwxi/ATS-Xanadu/tree/master/docgen/NOTES
>
> ##
>
>
>

-- 
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/0d51765c-2f28-4d1a-96a1-82c312ae9a25n%40googlegroups.com.

A vision for future programming in ATS

[gmhwxi]

Hi, there,

HX-2022-01-29:

A vision for future programming in ATS

Before I start, I would like to quote captain Woodrow F. Call,
a character played by Tommy Lee Jones in Lonesome Dove:

"Man of Vision you say...? Yeah. Hell of a vision." ~ Woodrow Call

By the way, here is the end of the Lonesome Dove miniseries where
Woodrow Call uttered the above line when interviewed by a reporter:

https://www.facebook.com/caldwellwritesdotcom/videos/lonesome-dove-tells-the-story-of-two-friends-who-were-legendary-texas-rangers-an/440279033007270

Ideally, a programming language should be simple and general, and
it should permit extensive error checking, facilitate proofs of
program properties such as correctness, and possess a correct and
efficient implementation. Invariably there will be some conflicts
among these goals which must be resolved with careful attention to the
needs of the user. I learned the above from Prof. John Reynolds when I
was a PhD student at CMU.

ATS3 is not an ordinary programming language. It is more like a
programming language for support meta-programming of all sorts.
Suppose we want to have programs written in some language X. Then we
traditionally write these programs manually in X. ATS3 provides an
alternative: We can implement a compiler from ATS3 to X to allow us to
write programs in ATS3 and then compile them to code in X.  In
practice, we hope to do co-programming with ATS3 and X; code in X
generated from ATS3 source can be combined with code in X obtained
otherwise. By programming in ATS3, we can benefit greatly from the
advanced type-checking that allows many varities of bugs to be flushed
out at compile-time; we can also benefit greatly from the extensive
use of templates that allows massive amount of quality code to be
generated in an automated manner.

In a following post, I will use a concrete example (co-programming
with ATS3 and Javascript) to outline some of the big steps involved
in building a compiler to support co-programing with ATS3 and X,
where X is just a placeholder for some programming language of one's
choice.

Cheers,

--Hongwei

##

For previously post messages:

https://github.com/githwxi/ATS-Xanadu/tree/master/docgen/NOTES

##


-- 
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/55680613-d404-4419-aa3a-8852bd10f3dbn%40googlegroups.com.

Re: general questions about ats postiats and upcoming xanadu compatibility

[gmhwxi]

Postiats and Xanadu use the same data representation (when compiled to C).
So they should be compatible at the level of C.

--Hongwei




On Friday, January 21, 2022 at 11:28:32 AM UTC-5 saif.ras...@gmail.com 
wrote:

> hi everyone, sorry for noob questions
> 1. will there be support added for msvc?
> 2. does ats code compile to c89 and/or c99?
> 3. does it support  pre-processor?
> 4.  a) if it does would you be able to use win32-threads aswell as 
> pthreads?
>   b) if not can i jam win32-thread code into the "<% %>" delimiters
> 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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/74ee4387-a08d-4f3f-9303-5215b1c57697n%40googlegroups.com.

Re: FAQ for ATS : is it of any benefit ? Is anyone willing to help ?

[gmhwxi]

Hi Yann,

Thanks for your enthusiasm.

>>@Hongwei : does it make any sense at this time given ATS3 looks well on 
its way to arrive on the scene ?

I would say that let's wait for some time. At this point, ATS3/Xanadu is 
far from a certainty.

If I am finally able to pull this off, that is, finishing a usable and 
useful compiler for compiling ATS3 to C, then
I would feel it is time to push ATS3/Xanadu to the world. But right now, it 
seems a bit too early for such a FAQ
for ATS.

--Hongwei



On Wednesday, January 26, 2022 at 1:16:21 PM UTC-5 Yann Le Du wrote:

> Hi,
>
> I'm going through the users group and I realize that it would probably be 
> much user-friendly if there was a FAQ for ATS based on the exchanges found 
> here.
>
> @Hongwei : does it make any sense at this time given ATS3 looks well on 
> its way to arrive on the scene ?
>
> If the above is positive, is anyone interested in helping make one (which 
> published parts would have to be validated by Hongwei I guess) ?
>

-- 
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/1f7e9cd3-24d5-480f-9d1e-965623408234n%40googlegroups.com.

Re: What are the references behind the names "postiats" and "xanadu" ?

[gmhwxi]

FYI.

I just made up the name Postiats. There is no particular meaning to it.
Just like the letter 'lambda' in lambda-calculus was chosen for no 
particular reason
(which I learned from Dana Scott, who learned it from the son-in-law of 
Alonzo Church,
the inventor of lambda-calculus).

I once designed and implemented a language called Xanadu. I chose the name 
Xanadu
for that language to mean something powerful, exotic and mysterious. See 
the following
poem by Coleridge:

https://www.poetryfoundation.org/poems/43991/kubla-khan

So I recycled the name Xanadu here. When writing ATS/Xanadu, I mean that 
the language is
called ATS and the implementation is called Xanadu. More precisely, it 
should be ATS3/Xananu
(ATS3 for the third edition of ATS).

Cheers,

--Hongwei


On Wednesday, January 26, 2022 at 1:31:28 PM UTC-5 Yann Le Du wrote:

> I see "ats" in "postiats", and "post" so maybe the "i" is "1" so it would 
> mean "after the 1st ATS" ?
>
> Whereas for "xanadu" maybe the famous Mongol metropolis, not sure, but 
> that would fit with the "unleashing" aspect of 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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/2cc2f9b2-dd31-45b3-af6c-3a50e6454791n%40googlegroups.com.

Re: About scientific computing with ATS and notation

[gmhwxi]

After reading and re-reading your message, I think that what you need is 
some kind of extension of ATS.

>> It's a big pile of questions, I just want to know if learning ATS could 
make those features possible. 

I feel that ATS and these programming features are kind of orthogonal. 

Say you want some code in a language called XYZ. For instance, XYZ can be 
C, Javascript or some assembly.
You can build a compiler from ATS to XYZ so that *some* (not all) code in 
XYZ that you need can be generated
from ATS source. By taking such an approach, you get the chance to use the 
type system of ATS to flush out a
large variety of potential bugs in your code. Also, the hope is that you 
can be a lot more productive at writing code
by making extensive use of the templates in ATS library.

While we all love concise and elegant syntax, the syntax of ATS (as of now) 
is quite verbose. One big reason for this
is that ATS aims to provide extensive debugging support at compile-time. 
Say you have just finished writing a Python
program. Then it is only logical that you test it by running it. After 
finishing writing an ATS program, you could run it or
you could find ways strength the types used in it so as to flush out 
potential bugs.

Now let me say a few words about the following syntax:

`for i,j: C.i.j = A.i.k * B.k.j`

Clearly, this syntax indicates that the sizes (nrow and ncol) of a matrix 
needs to be attached to the matrix. This would
cause serious problems if you want to process submatrices (e.g., when 
implementing Strassen's matrix multiplication).
In order to process arrays efficiently, the sizes of arrays really need to 
be detached from the arrays themselves.

Another issue with "elegant" syntax is that it does not go well with 
debugging. Often, "elegant" code is only obtained at
the end of a "messy" debugging process.

Hope this can clarify a few things on ATS for you.

--Hongwei

On Sunday, January 23, 2022 at 12:46:12 PM UTC-5 Yann Le Du wrote:

> Dear ATSites,
>
> First, impressed by the power of ATS which unfortunately for me is still 
> inaccessible even after spending the typical time I spend overviewing other 
> languages. For sure, I've listened to many people saying how hard it was, 
> so that didn't help ;-) Maybe they want to keep ATS for themselves and 
> frighten away potential new users ?
>
> I'm a physicist, cosmologist, currently working on setting up a project 
> involving image reconstruction, around what the Chebfun matlab toolbox 
> implements. Now, I've been looking at Dex, he new google research language, 
> because that's typically what I need,for exactly the same reason the 
> designers made Dex (escape Matlab and go for more than its clone on juice, 
> Julia) but it looks very experimental and doesn't really have all I need, 
> especially interfacing with C.
>
> So first, would I be able to massage ATS into allowing some nice syntax, I 
> mean can I code a library (using whatever tools I totally don't understand 
> today) that would allow me to write 
>
> `for i,j: C.i.j = A.i.k * B.k.j`
>
> In a very similar way to Dex (who has ranged integer type for the 
> indices), i.e. which would be interpreted as :
>
> ```
> for i in rows range of A:
>   for j in colums range of B:
> for k in cols of A == rows of B:
>   C[i,j] = A[i,k] * B[k,j]
> ```
>
> or whatever equivalent in ATS.
>
> You will notice that it loops implicitly on k (Einstein summation), thus 
> without me specifying k, and all the indices getting checked like in Dex at 
> compile time, with inference wherever needed. This means I want to be able 
> to write M.2.3 = 25 (meaning M[2,3]=5) without casting overhead like in Dex 
> (they have to cast from integers to ranged ordinals if I remember).
>
> I would also need support for 128 bit integers and all for cryptographic 
> uses, the possibility of defining
>
> foo(m `Matrix[12 rows, any u32 in [0,23] columns, any float type for the 
> elements, unknown variance]`)
>
> and then call foo with `foo(b)` and b is checked to fit the type declared 
> for foo's arguments, so it wold tell me if I try to put in a matrix with 
> too many rows, but accept a matrix with 12 rows and 21 columns filled with 
> f32, the possibility of defining a set of accepted types, including 
> constants, and check if what I use belongs to that set, abstractions like 
> OO to better contain the math abstractions we manipulate.
>
> Also, the possibility to implement the right structures for SIMD and all 
> that, SOA, etc. This organizing my memory as I want, perhaps not from the 
> start, but as the project progresses.
>
> The possibility of multicores, and distributed computing.
>
> Proving that some functions are right.
>
> And last but not least, how much will I have to [un|re]learn when ATS3 is 
> released ?
>
> And maybe other questions will follow if the above receives positive 
> answers...
>
> By the way, why no Discord channel ? It's so helpful for a community.
>
> It's a big pile of 

Re: About scientific computing with ATS and notation

[gmhwxi]

Hi Yann,

It is difficult to keep up with your questions :)

On Tuesday, January 25, 2022 at 7:29:39 PM UTC-5 Yann Le Du wrote:

> Thanks for your interest in my questions. Just to clarify a few things :
>
> 1. Can I use some form of macros like in rust or Julia to allow new syntax 
> inside ATS ? My goal is to allow writing directly something like `A.i.j = 
> 12` or something more complex like I showed in my original mail.
>

There is a macro language within ATS. I believe that you could write 
something like A[i,j] = 12 or A[i][j]  = 2. 

2. If adding some new syntax is not possible, can I write a parser with ATS 
> itself to do that and generate ATS code behind ?
>

 I like this approach. This is the way I intend to build various ATS 
extensions to support special programming (or DSLs).

3. In the meantime I looked into more detail into the possibilities of ATS 
> with regards to ranged indexing, and indeed I can do exactly what I want, 
> but again I would like to know if I can create a specific syntax for some 
> manipulations,.
>

See above.

4. You mention writing FFI but can I keep all of ATS advantages (proofs, 
> types, etc.) while writing FFI ? In my mind, if I go to another language, I 
> lose all guarantees.
>

 Of course, you have to assume some form of correctness of the "foreign" 
code.

5. Concerning syntax again, it looks like ATS does not support UTF-8 names 
> for `var` or `fn` : is there a way around this ? Or maybe this goes back to 
> question 2. ?
>

Maybe this could be first tried in an extension.
 

> 6. As for concurrency, how does the actor model make sense within ATS ? Is 
> the ATS type-system a superset of the actor model as implemented in Pony 
> for example ? To finish, does using pthreads mean I write some wrappers on 
> top of libpthread or similar like Rust does and have ATS bring me 
> guarantees with my concurrent code ?
>

ATS  itself is not tied to pthreads. Yes, you can use pthreads by writing 
some wrappers (of zero runtime cost) on top of libpthread.
The type system of ATS  can detect a variety of concurrency related issues 
during type-checking (e.g., potential race conditions and deadlocks).

--Hongwei


> On Wednesday, January 26, 2022 at 12:28:30 AM UTC+1 d4v3y_5c0n3s wrote:
>
>> Hi Yann,
>>   I'm glad to see others showing interest in ATS :D.  I'm not very 
>> familiar with the sort of scientific programming that you are talking 
>> about, but I'll do my best to respond to your questions regardless.
>>   You asked whether you could use 128 bit integers, SIMD, multicore, and 
>> even distributed computing.  Like, holy moly man.  :D  But yea, ATS can do 
>> basically anything C can, with the caveat that you may need to write FFI 
>> code due to the small size of the ATS ecosystem.
>>   As for the static capabilities of ATS, this I believe to be the 
>> strongest quality of ATS.  Indexing into arrays/matrices is verified at 
>> compile time so your example should be recreate-able in ATS.  And no, ATS' 
>> type system doesn't require you to constantly cast to verify the range of 
>> an integer, but it will force you write your code in such a way that the 
>> system knows without a doubt that the integer is not out of range.  It's 
>> hard to explain, but if you are interested I'd recommend working through 
>> the Intro to ATS book in the documentation on the website.
>>   I'm not involved with the development of ATS3, so gmhwxi would know 
>> more about how much it will change.  I'd recommend reading previous posts 
>> about ATS3 to find out more.
>> Good luck.
>>
>> On Sunday, January 23, 2022 at 12:46:12 PM UTC-5 Yann Le Du wrote:
>>
>>> Dear ATSites,
>>>
>>> First, impressed by the power of ATS which unfortunately for me is still 
>>> inaccessible even after spending the typical time I spend overviewing other 
>>> languages. For sure, I've listened to many people saying how hard it was, 
>>> so that didn't help ;-) Maybe they want to keep ATS for themselves and 
>>> frighten away potential new users ?
>>>
>>> I'm a physicist, cosmologist, currently working on setting up a project 
>>> involving image reconstruction, around what the Chebfun matlab toolbox 
>>> implements. Now, I've been looking at Dex, he new google research language, 
>>> because that's typically what I need,for exactly the same reason the 
>>> designers made Dex (escape Matlab and go for more than its clone on juice, 
>>> Julia) but it looks very experimental and doesn't really have all I need, 
>>> especially interfacing with C.
>>>
>>> So first, would I be able to massage ATS into allowing some nice syntax, 
>>

Re: Concerning optimizations

[gmhwxi]

Hi Yann,

I will try to answer the questions you raised in an earlier post later.

Regarding optimizations, I find that feeding to gcc the C code generated 
from ATS source
is a reasonable choice. Yes, one could probably generate significantly more 
efficient code
by taking advantage of the rich type information inside ATS programs. But 
doing so is highly
non-trivial; it would require a very big effort.

Yes, the compiler of SAC can do amazing optimizations. But SAC as a 
programming language
often lacks features that can help construct efficient programs. Let me use 
a concrete example.

Say that I want to process all the lines in a given file. I could do this 
by calling fgets in a loop to
read in each line and process it, but this is very inefficient. I could do 
much better if I use mmap
to map the content of the file to some virtual address space, but this 
requires a lot more effort.
Naturally, I would expect a library function of some sort for fast 
processing lines in a file, but what
would be a good interface for such a function? Sometimes, I want to process 
all these lines sequentially,
and, sometimes, I want to process them in parallel. This is a very thorny 
issue in programming language
design. One key focus of ATS3 is on providing support for the programmer to 
write efficient code that
would often require much more effort if done elsewhere.

Cheers,

--Hongwei

On Monday, January 24, 2022 at 7:49:48 AM UTC-5 Yann Le Du wrote:

> Hello again,
>
> I hope I'll get some answer to my previous post, but in the neantime I 
> have a question about optimizations.
>
> I've been looking at SAC  , the 
> amazing FP array language that has a 30 years mature optimizer, and the 
> same number of users as ATS ;-) The main designer, Sven-Bodo Scholz, told 
> me something that prompts my present post.
>
> I have a very simple kind-of fiboncacci loop inside loop, and some of the 
> computations bear no effect on the result, and if I use : `sac2c`, the SAC 
> compiler, it just CRUSHES `gcc -O3` (factor 100x in running time for the 
> same result).
>
> So I asked Scholz how he managed it :
>
> "If you write some code that computes stuff that does not contribute in 
> any which way to the results, it is nice if the compiler can get rid of it. 
> FP ensures that all effects are explicit. Once the compiler knows all of 
> them it can elide everything else. But in gcc it is very hard to figure out 
> whether there is a hidden side-effect somewhere, therefore, the guys in 
> general do not even bother to try for the simple cases."
>
> But I very often hear this about ATS :
>
> "oh, ATS actually doesn’t optimize anything, except tail calls, produces 
> the c intermediate code, and thus leaves gcc do its job, which is like 
> *awesome"*
>
> which to me sounds like (I may be wrong) :
>
> "people who optimize before passing the baby to gcc are like dummies”
>
> So why would ATS, which is functional, abandon its performance to gcc if 
> it could do more (side-effects ?) optimizations thanks to being FP ? Is it 
> because optimizing, like SAC, is a 30 years craft best left to future 
> developers of ATS_n>=3 or is there something deeper ?
>
> Is it because ATS is a systems programming language, and thus cannot risk 
> eliding stuff that could be elided in an array language like SAC ?
>
> Cheers,
>
> Yann
>

-- 
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/de69b561-e102-4fe7-9b32-4d895fe041fbn%40googlegroups.com.

Re: Help with Templates, cannot find missing implementation somewhere...

[gmhwxi]

Or you could supply a template parameter (bucket(a) in this case) to
arrayptr_freelin:

implmnt{a} dict_delete_lin ( d ) = let
  implmnt array_uninitize$clear (i, x) = 
bucket_delete_recursive(x)
in
  arrayptr_freelin(d.buckets, size_of_int(d.size))
end
On Thursday, December 30, 2021 at 9:00:48 PM UTC-5 gmhwxi wrote:

> Just need to replace bucket(a) with BUCKET(a) as is shown below:
>
>   implmnt array_uninitize$clear (i, x) = 
> bucket_delete_recursive(x)
>
> On Thursday, December 30, 2021 at 6:07:31 PM UTC-5 d4v3y_5c0n3s wrote:
>
>> Here are the files, with some of the functions that are never used in the 
>> example removed.
>> The code was compiled with:  *patscc -c -DATS_MEMALLOC_LIBC dict.dats*
>> | | |
>> (*
>> ###  dict.sats  ###
>>
>>
>> *)
>>
>> #include "share/atspre_staload.hats"
>>
>> (*  buckets (aka linked lists)  *)
>> absvtype bucket (a:vt@ype) = ptr
>>
>> fn{a:vt@ype} bucket_new ( string, a ) : bucket(a)
>>
>> fn{a:vt@ype} bucket_map ( !bucket(a) ) : void
>> fn{a:vt@ype} bucket_filter_map ( b: !bucket(a) ) : void
>>
>>
>> fn{a:vt@ype} bucket_item$delete ( x: a ): void
>> fn{a:vt@ype} bucket_item$map ( x:  ): void
>> fn{a:vt@ype} bucket_item$filter ( x: !a ): bool
>> fn{a:vt@ype} bucket_item$to_string ( x: !a ): string
>>
>>
>> fun{a:vt@ype} bucket_delete_recursive ( b: bucket(a) ) : void
>>
>> fn{a:vt@ype} bucket_print ( b: !bucket(a) ) : void
>>
>> (*  dictionaries  *)
>>
>> sortdef dsz = {s:int | s > 0}
>> absvt@ype dict (a:vt@ype, n:int) = @{size=int,buckets=ptr}
>>
>>
>> fn{a:vt@ype} dict_new {s:dsz} ( int s ) : dict(a, s)
>> fn{a:t@ype} dict_delete {s:dsz} ( d: dict(a, s) ) : void
>> fn{a:vt@ype} dict_delete_lin {s:dsz} ( d: dict(a, s) ) : void
>> fn{a:vt@ype} dict_delete_fun {s:dsz} ( d: dict(a, s), (a) -> void ) : void
>> | | |
>> (*
>> ###  dict.dats  ###
>>
>>
>> *)
>>
>> #include "share/atspre_staload.hats"
>>
>> staload "./dict.sats"
>>
>> fn hash {n:int | n>0}{s:int | s>0}
>> ( s: string(s), size: int(n) ) : [o:int | o >= 0; o < n] int o = let
>> fun hash_num {i:nat | i <= s}
>> ( i: int i, h: int, str_sz: int(s) ) : int =
>> if i < str_sz then let
>> val c_at_i = string_get_at_gint(s, i)
>> in
>> hash_num(i+1, h * 101 + g0int_of_char(c_at_i), 
>> str_sz)
>> end else h
>> in
>> g1int_nmod(abs(g1ofg0(hash_num(0, 0, sz2i(strlen(s), size)
>> end
>>
>> local
>>
>> datavtype BUCKET (a:vt@ype) =
>> | bucket_empty of ()
>> | bucket_filled of (Strptr1, a, BUCKET(a))
>>
>> assume bucket(a:vt@ype) = BUCKET(a)
>> assume dict(a:vt@ype, n:int) = @{
>>   size=int n,
>>   buckets=arrayptr(bucket(a), n)
>> }
>>
>> extern fn{a:vt@ype} bucket_operate ( !bucket(a) ) : void
>>
>>
>> in
>>
>> implement{a} dict_new {s} ( size ) = let
>> val size_st = size_of_int(size)
>> val bucket_arr = arrayptr_make_uninitized(size_st)
>> implmnt array_initize$init (i, x) = x := bucket_empty()
>> val () = arrayptr_initize(bucket_arr, size_st)
>> in
>> @{size=size, buckets=bucket_arr}:dict(a, s)
>> end
>>
>> implmnt{a} dict_delete ( d ) = let
>>   implmnt(a2:t@ype) bucket_item$delete ( x ) = ()
>> in
>>   dict_delete_lin(d)
>> end
>>
>> implmnt{a} bucket_delete_recursive ( b ) =
>> case+ b of
>> | ~bucket_empty() => ()
>> | ~bucket_filled(str, x, next_bucket) => let
>> val () = strptr_free(str)
>> val () = bucket_item$delete(x)
>> in
>> bucket_delete_recursive(next_bucket)
>> end
>>
>> implmnt{a} dict_delete_lin ( d ) = let
>>   implmnt array_uninitize$clear (i, x) = 
>> bucket_delete_recursive(x)
>> in
>>   arrayptr_freelin(d.buckets, size_of_int(d.size))
>> end
>>
>> implmnt{a} dict_delete_fun ( d, dltr ) = let
>>   implmnt bucket_item$delete ( x ) = dltr(x)
>> in
>>   dict_delete_lin(d)
>> end
>>
>>
>> implmnt{a} bucket_new ( key, item ) = 
>> bucket_filled($UNSAFE.castvwtp0{Strptr1}(key), item, bucket_empty())
>>
>> implmnt{a} bucket_map ( b ) =
>>   case+ b of
>>   | bucket_empty() => ()
>>   | @bucket_filled(_, x, next_bucket) => {
>> val () = bucket_item$map(x)
>

Re: Help with Templates, cannot find missing implementation somewhere...

[gmhwxi]

Just need to replace bucket(a) with BUCKET(a) as is shown below:

  implmnt array_uninitize$clear (i, x) = 
bucket_delete_recursive(x)

On Thursday, December 30, 2021 at 6:07:31 PM UTC-5 d4v3y_5c0n3s wrote:

> Here are the files, with some of the functions that are never used in the 
> example removed.
> The code was compiled with:  *patscc -c -DATS_MEMALLOC_LIBC dict.dats*
> | | |
> (*
> ###  dict.sats  ###
>
>
> *)
>
> #include "share/atspre_staload.hats"
>
> (*  buckets (aka linked lists)  *)
> absvtype bucket (a:vt@ype) = ptr
>
> fn{a:vt@ype} bucket_new ( string, a ) : bucket(a)
>
> fn{a:vt@ype} bucket_map ( !bucket(a) ) : void
> fn{a:vt@ype} bucket_filter_map ( b: !bucket(a) ) : void
>
>
> fn{a:vt@ype} bucket_item$delete ( x: a ): void
> fn{a:vt@ype} bucket_item$map ( x:  ): void
> fn{a:vt@ype} bucket_item$filter ( x: !a ): bool
> fn{a:vt@ype} bucket_item$to_string ( x: !a ): string
>
>
> fun{a:vt@ype} bucket_delete_recursive ( b: bucket(a) ) : void
>
> fn{a:vt@ype} bucket_print ( b: !bucket(a) ) : void
>
> (*  dictionaries  *)
>
> sortdef dsz = {s:int | s > 0}
> absvt@ype dict (a:vt@ype, n:int) = @{size=int,buckets=ptr}
>
>
> fn{a:vt@ype} dict_new {s:dsz} ( int s ) : dict(a, s)
> fn{a:t@ype} dict_delete {s:dsz} ( d: dict(a, s) ) : void
> fn{a:vt@ype} dict_delete_lin {s:dsz} ( d: dict(a, s) ) : void
> fn{a:vt@ype} dict_delete_fun {s:dsz} ( d: dict(a, s), (a) -> void ) : void
> | | |
> (*
> ###  dict.dats  ###
>
>
> *)
>
> #include "share/atspre_staload.hats"
>
> staload "./dict.sats"
>
> fn hash {n:int | n>0}{s:int | s>0}
> ( s: string(s), size: int(n) ) : [o:int | o >= 0; o < n] int o = let
> fun hash_num {i:nat | i <= s}
> ( i: int i, h: int, str_sz: int(s) ) : int =
> if i < str_sz then let
> val c_at_i = string_get_at_gint(s, i)
> in
> hash_num(i+1, h * 101 + g0int_of_char(c_at_i), 
> str_sz)
> end else h
> in
> g1int_nmod(abs(g1ofg0(hash_num(0, 0, sz2i(strlen(s), size)
> end
>
> local
>
> datavtype BUCKET (a:vt@ype) =
> | bucket_empty of ()
> | bucket_filled of (Strptr1, a, BUCKET(a))
>
> assume bucket(a:vt@ype) = BUCKET(a)
> assume dict(a:vt@ype, n:int) = @{
>   size=int n,
>   buckets=arrayptr(bucket(a), n)
> }
>
> extern fn{a:vt@ype} bucket_operate ( !bucket(a) ) : void
>
>
> in
>
> implement{a} dict_new {s} ( size ) = let
> val size_st = size_of_int(size)
> val bucket_arr = arrayptr_make_uninitized(size_st)
> implmnt array_initize$init (i, x) = x := bucket_empty()
> val () = arrayptr_initize(bucket_arr, size_st)
> in
> @{size=size, buckets=bucket_arr}:dict(a, s)
> end
>
> implmnt{a} dict_delete ( d ) = let
>   implmnt(a2:t@ype) bucket_item$delete ( x ) = ()
> in
>   dict_delete_lin(d)
> end
>
> implmnt{a} bucket_delete_recursive ( b ) =
> case+ b of
> | ~bucket_empty() => ()
> | ~bucket_filled(str, x, next_bucket) => let
> val () = strptr_free(str)
> val () = bucket_item$delete(x)
> in
> bucket_delete_recursive(next_bucket)
> end
>
> implmnt{a} dict_delete_lin ( d ) = let
>   implmnt array_uninitize$clear (i, x) = 
> bucket_delete_recursive(x)
> in
>   arrayptr_freelin(d.buckets, size_of_int(d.size))
> end
>
> implmnt{a} dict_delete_fun ( d, dltr ) = let
>   implmnt bucket_item$delete ( x ) = dltr(x)
> in
>   dict_delete_lin(d)
> end
>
>
> implmnt{a} bucket_new ( key, item ) = 
> bucket_filled($UNSAFE.castvwtp0{Strptr1}(key), item, bucket_empty())
>
> implmnt{a} bucket_map ( b ) =
>   case+ b of
>   | bucket_empty() => ()
>   | @bucket_filled(_, x, next_bucket) => {
> val () = bucket_item$map(x)
> val () = bucket_map(next_bucket)
> prval () = fold@(b)
>   }
>
> implmnt{a} bucket_filter_map ( b ) =
>   case+ b of
>   | bucket_empty() => ()
>   | @bucket_filled(_, x, next_bucket) =>
>   if bucket_item$filter(x) then {
>   val () = bucket_item$map(x)
>   val () = bucket_filter_map(next_bucket)
>   prval () = fold@(b)
>   }
>   else {
> val () = bucket_filter_map(next_bucket)
> prval () = fold@(b)
>   }
>
> implmnt{a} bucket_print ( b ) =
> case+ b of
> | bucket_empty() => ()
>
> | bucket_filled(str, x, next_bucket) => let
> val () = print("\(")
> val () = print(str)
> val () = print(" : ")
> val () = print( bucket_item$to_string(x) )
> val () = print(")"

Re: What is the best way to turn a file into a lazy linear stream?

[gmhwxi]

Sorry, I didn't get a chance to read this post until now.

If you use a (linear) FILEptr to create a linear stream (of chars), then 
the FILEptr is "buried" inside
the stream and thus it can no longer be accessed.

>>My solution was to essentially combine the view for the file pointer and 
the stream into a single type, and thus requiring both to be freed at once.

To me, this seems to be the only type-safe solution (as the alternative you 
mentioned above must make use of some unsafe features).

--Hongwei


On Sunday, October 17, 2021 at 9:14:04 AM UTC-4 d4v3y_5c0n3s wrote:

> Okay, so looking back I should have provided more details in the last 
> post, as it does not explain the issues I was encountering etc.  I posted 
> it right before I went to bed, and that's why I rushed it.
> Anyways, I wanted to explain how I solved my problem so that others 
> could learn.  Basically, I was using ATS' built-in libc binding to open and 
> read a file.  The pointer for the file was a linear type, I wasn't using 
> the prelude's non-linear file type.  What my code did is read characters to 
> a 'stream_vt' with the 'getc' function until it reached the end of the 
> file.  I also planned to have other functions that would discard parts of 
> the stream I didn't need so that I could turn the values I needed into 
> other values (AKA, typical file-parsing stuff.)  The problem came when I 
> needed to close the file.  Despite the use of linear types, freeing the 
> file pointer would not prevent the stream from being access due to its 
> laziness.  My solution was to essentially combine the view for the file 
> pointer and the stream into a single type, and thus requiring both to be 
> freed at once.
> Moral of the story?  Linear types are amazing, one of the reasons I 
> love ATS, but they are *not* a silver bullet.  They too are limited by 
> what can be statically inferred by the compiler, and effects such as lazy 
> values cannot be predicted by the compiler.  I hope someone was able to 
> learn something from my post, and let me know if you have any questions.
>
> On Monday, October 4, 2021 at 9:17:38 PM UTC-4 d4v3y_5c0n3s wrote:
>
>>
>> What the title says.  Basically, I want to use a solution that:
>>  - does not require GC
>>  - uses the type system to prevent the user from freeing the file before 
>> they are done with the lazy evaluation
>>  - is not too inconvenient for the user to use
>> Let me know if you need an example of what I'm talking about.
>>
>

-- 
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/4264b891-e9e1-403e-8e4a-ca3057ba8657n%40googlegroups.com.

Re: Help with Templates, cannot find missing implementation somewhere...

[gmhwxi]

After taking a quick look at dict.sats, I spotted the following line:

absvtype bucket(a:vt@ype)

which should be change to the following one:

absvtype bucket(a:vt@ype) = ptr // ptr takes the compiler the size of bucket

The simple reason is that the compiler needs to know the size of an 
abstract type in order to compile it to a type in C.


On Wednesday, December 1, 2021 at 12:16:34 AM UTC-5 gmhwxi wrote:

> I don't quite understand.
> Templates in ATS2 are supposed to be working with abstract types.
>
> If I could try precisely what you did on your machine, then I may be able 
> to suggest something.
>
>
>
> On Tue, Nov 30, 2021 at 8:27 PM d4v3y_5c0n3s  wrote:
>
>> Update 2:
>> After investigating the prelude, I've determined that templates in ATS2 
>> just conflict with abstract types in some instances.  For this reason, it 
>> seems that in many parts of the prelude avoided the use of the "assume" 
>> keyword with template-heavy code.
>>
>> On Tuesday, November 30, 2021 at 7:08:48 PM UTC-5 d4v3y_5c0n3s wrote:
>>
>>> Update:
>>> I was able to get the code I provided above running by staloading the 
>>> dict.dats file from the dict_test.dats file using " staload _ = 
>>> "./dict.dats" ".  Now, my only problem is that if I make the "dict" & 
>>> bucket types abstract, the templates stop working.
>>>
>>> On Tuesday, November 30, 2021 at 1:39:39 PM UTC-5 d4v3y_5c0n3s wrote:
>>>
>>>> You are right, including " share/atspre_staload.hats" causes the code 
>>>> to compile.  However, I'm still having issues.  You see, the code I 
>>>> provided I had taken from a static (.sats) and dynamic (.dats) file in 
>>>> order to make it more presentable when asking for help.  Your fix only 
>>>> fixes the issue in the single-file version, and when including the 
>>>> external 
>>>> static file it doesn't work.  Do you know what might be going wrong?  I'll 
>>>> provide the (simplified) contents of each of these files below.
>>>>
>>>> *dict.sats*:
>>>> #include "share/atspre_staload.hats"
>>>>
>>>>
>>>> datavtype BUCKET (a:vt@ype) =
>>>> | bucket_empty of ()
>>>> | bucket_filled of (Strptr1, a, BUCKET(a))
>>>>
>>>> vtypedef bucket(a:vt@ype) = BUCKET(a)
>>>>
>>>> fn{a:vt@ype} bucket_item$delete ( x: a ): void
>>>>
>>>> fun{a:vt@ype} bucket_delete_recursive ( b: bucket(a) ) : void
>>>>
>>>> sortdef dsz = {s:int | s > 0}
>>>>
>>>> vtypedef dict(a:vt@ype, n:int) =
>>>> @{
>>>> size=int n,
>>>> buckets=arrayptr(bucket(a), n)
>>>> }
>>>>
>>>> fn{a:vt@ype} dict_new {s:dsz} ( int s ) : dict(a, s)
>>>> fn{a:t@ype} dict_delete {s:dsz} ( d: dict(a, s) ) : void
>>>> fn{a:vt@ype} dict_delete_lin {s:dsz} ( d: dict(a, s) ) : void
>>>>
>>>>
>>>> *dict.dats*:
>>>> #include "share/atspre_staload.hats"
>>>>
>>>> staload "./dict.sats"
>>>>
>>>> local
>>>> in
>>>>
>>>>
>>>> implement{a} dict_new {s} ( size ) = let
>>>> val size_st = size_of_int(size)
>>>> val bucket_arr = arrayptr_make_uninitized(size_st)
>>>> implmnt array_initize$init (i, x) = x := bucket_empty()
>>>> val () = arrayptr_initize(bucket_arr, size_st)
>>>> in
>>>> @{size=size, buckets=bucket_arr}:dict(a, s)
>>>> end
>>>>
>>>> implmnt{a} dict_delete ( d ) = let
>>>>   implmnt(a2:t@ype) bucket_item$delete ( x ) = ()
>>>> in
>>>>   dict_delete_lin(d)
>>>> end
>>>>
>>>> implmnt{a} bucket_delete_recursive ( b ) =
>>>> case+ b of
>>>> | ~bucket_empty() => ()
>>>> | ~bucket_filled(str, x, next_bucket) => let
>>>> val () = strptr_free(str)
>>>> val () = bucket_item$delete(x)
>>>> in
>>>> bucket_delete_recursive(next_bucket)
>>>> end
>>>>
>>>> implmnt{a} dict_delete_lin ( d ) = let
>>>>   implmnt array_uninitize$clear (i, x) = 
>>>> bucket_delete_recursive(x)
>>>> in
>>>>   arrayptr_freelin(d.buckets, size_of_int(d.size))
>>>> end
>>>> end
>>>>
>>>

Re: Why aren't the MUL() prop functions in the prelude docs? (on the site, that is)

[gmhwxi]

Yes, please open an issue about it. Thanks!

On Saturday, October 30, 2021 at 10:20:03 AM UTC-4 d4v3y_5c0n3s wrote:

> I just noticed that the MUL() proof functions like "mul_gte_gte_gte()" are 
> actually not listed in the prelude reference on the "ats-lang.org" site.  
> Is this intended?  Should open an issue on Github about it or something?
>

-- 
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/09dd7315-8b0c-4dec-bee0-f0c6500dbe53n%40googlegroups.com.

Re: FILEREF type is non-linear?

[gmhwxi]

FILEref is abstract; it is just FILE* in C. As it is non-linear, you
need to remember to close an opened file handle of this type.

BTW, FILEptr is linear; so the type system help you keep track of
file handles of the type FILEptr.

--Hongwei

PS: I often use FILEref first. If needed later, I can always change
it to FILEptr and the typechecker will then lead me to all the places
where subsequent changes are needed for such a change.

On Sunday, July 11, 2021 at 8:02:39 PM UTC-4 d4v3y_5c0n3s wrote:

> Just a quick question: I noticed that the "FILEREF" type in ATS is 
> non-linear.  Does this mean that I need to enable garbage collection to 
> work with files?  Or is the value freed but hidden from the linear type 
> system?

-- 
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/c521ce5b-a311-4d65-a1a3-669b1488c2b2n%40googlegroups.com.

Re: ATS3 and stuff

[gmhwxi]

>>Very optimistically, I expect to see some version of ATS3 that is
>>able to compile to C/C++

Sorry, I meant to say that I expect to see it by the end of this year.


On Sunday, July 4, 2021 at 5:27:11 PM UTC-4 gmhwxi wrote:

>
> Thanks for your interest in ATS3!
>
> I am still in the midst of implementing ATS3. More precisely, I am
> in the midst of implementing a type-checker for dependent types
> and linear types. The required effort seems to have far exceeded
> what I expected.
>
> Up to ATS2, ATS was largely a vehicle for experimentation.
> If I remember correctly, ATS0 (that is, ATS/Proto) is probably the most
> feature-rich one among all editions of ATS so far; it contains many 
> features
> (e.g., OOP and typed meta-programming based on macros) that are removed
> in later editions of ATS.
>
> As I feel that ATS3 is very likely the last edition of ATS that I will 
> ever be implementing,
> I tend to think a lot more before I actually write down code. So the 
> implementation
> does take a lot longer this time. The good news is that I should be able 
> to move a bit
> faster once I finish this type-checker, which undoubtedly is the most 
> challenging part
> of implementing ATS3. Very optimistically, I expect to see some version of 
> ATS3 that is
> able to compile to C/C++. Keep tuned :)
>
> Cheers!
>
> --Hongwei
>
> On Monday, June 28, 2021 at 9:00:00 AM UTC-4 Timmy Jose wrote:
>
>> Also, in any case, I think I'll wait for ATS3, and this time go through 
>> full learning process, and start doing some projects in it. I'm excited, 
>> and hopefully it won't be too long coming!
>>
>> On Monday, June 28, 2021 at 6:28:55 PM UTC+5:30 Timmy Jose wrote:
>>
>>>
>>> Hello,
>>>
>>> I had dabbled with ATS2 a couple of years back, and I happened to have a 
>>> look back at the ATS ecosystem a couple of days back. It is interesting to 
>>> see ATS3 being actively developed, and it's also exciting to see that 
>>> ergonomics is a key focus for this version of the language (this is what I 
>>> gleaned from some of the posts here).
>>>
>>> About learning the language (I've unfortunately forgotten most of it), I 
>>> looked at the learning materials again, and they are of very good quality, 
>>> but I was thinking that someone from the community could create something 
>>> from their own perspective, for beginners. That would also help get people 
>>> interested in the language - a more gentle introduction to the core selling 
>>> points of ATS (or at least the basic viable features of ATS). What do you 
>>> think? 
>>>
>>> I know the community is small, but time and again I keep thinking that 
>>> ATS has so much potential that it's a shame that it's not getting much more 
>>> attention from people (a lot of it has to do with the fact that most people 
>>> are not even aware of its existence).
>>>
>>> Cheers,
>>>
>>> Timmy
>>>
>>

-- 
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/236e699a-ebc4-4479-a8a5-6757bd07007cn%40googlegroups.com.

Re: ATS3 and stuff

[gmhwxi]

Thanks for your interest in ATS3!

I am still in the midst of implementing ATS3. More precisely, I am
in the midst of implementing a type-checker for dependent types
and linear types. The required effort seems to have far exceeded
what I expected.

Up to ATS2, ATS was largely a vehicle for experimentation.
If I remember correctly, ATS0 (that is, ATS/Proto) is probably the most
feature-rich one among all editions of ATS so far; it contains many features
(e.g., OOP and typed meta-programming based on macros) that are removed
in later editions of ATS.

As I feel that ATS3 is very likely the last edition of ATS that I will ever 
be implementing,
I tend to think a lot more before I actually write down code. So the 
implementation
does take a lot longer this time. The good news is that I should be able to 
move a bit
faster once I finish this type-checker, which undoubtedly is the most 
challenging part
of implementing ATS3. Very optimistically, I expect to see some version of 
ATS3 that is
able to compile to C/C++. Keep tuned :)

Cheers!

--Hongwei

On Monday, June 28, 2021 at 9:00:00 AM UTC-4 Timmy Jose wrote:

> Also, in any case, I think I'll wait for ATS3, and this time go through 
> full learning process, and start doing some projects in it. I'm excited, 
> and hopefully it won't be too long coming!
>
> On Monday, June 28, 2021 at 6:28:55 PM UTC+5:30 Timmy Jose wrote:
>
>>
>> Hello,
>>
>> I had dabbled with ATS2 a couple of years back, and I happened to have a 
>> look back at the ATS ecosystem a couple of days back. It is interesting to 
>> see ATS3 being actively developed, and it's also exciting to see that 
>> ergonomics is a key focus for this version of the language (this is what I 
>> gleaned from some of the posts here).
>>
>> About learning the language (I've unfortunately forgotten most of it), I 
>> looked at the learning materials again, and they are of very good quality, 
>> but I was thinking that someone from the community could create something 
>> from their own perspective, for beginners. That would also help get people 
>> interested in the language - a more gentle introduction to the core selling 
>> points of ATS (or at least the basic viable features of ATS). What do you 
>> think? 
>>
>> I know the community is small, but time and again I keep thinking that 
>> ATS has so much potential that it's a shame that it's not getting much more 
>> attention from people (a lot of it has to do with the fact that most people 
>> are not even aware of its existence).
>>
>> Cheers,
>>
>> Timmy
>>
>

-- 
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/dd0dc738-96e4-4777-a6b6-904bbd3e2b04n%40googlegroups.com.

Functional imperative programming in ATS

[gmhwxi]

FYI.

Functional programming (FP) puts emphasis on "purity" these days.
In particular, it preaches all sorts of benefits gained from avoiding
updates in programming. This somewhat leaves one with the impression
that "pure" programs cannot have updates. How wrong! A novelty of ATS
precisely lies in that "pure" programs can have updates.

I am from the camp of FP. As a matter of fact, the core of ATS is
ML-like; it supports type inference, polymorphism, higher-order
functions, datatypes and pattern matching, etc. However, I also want
to stress that ATS offers much more than the usual kind of ML-like
functional programming, which, in my opinion, is far from being
adequate for systems programming (that is, implementing low-level
systems).

Once upon a time, we had LISP machines and operating systems written
in LISP.  I suppose that most people would call LISP a functional
language.  But LISP is not ML-like; it does not preach "purity" at
all. In particular, typical LISP programs make pervasive use of
updates. Maybe we should just refer to LISP as a functional imperative
programming (FIP) language.

What is so attractive about FIP? Let us first see a serious issue
with ML-like functional programming. With functional data structures
(that do not support modifications), it is often difficult, if
possible at all, to give an efficient tail-recursive implementation of
certain simple recursive functions. For instance, a famous example is
the following 'append' for concatenation two lists:

fun
append
(xs, ys) =
(
case xs of
| nil() => ys
| cons(x1, xs) => cons(x1, append(xs, ys))
)

Assume that the direct style of compilation is used to compile
'append'. Since 'append' is recursive but not tail-recursive, each
recursive call to 'append' requires allocating a new frame on the call
stack. This simply implies that calling 'append(xs, ys)' on a long
list 'xs' requires a deep stack for otherwise it causes the call stack
to overflow.

One possible attempt to implement 'append' in a tail-recursive manner
leads to the following terribly inefficient implementation:

fun
append
(xs, ys) =
rappend(reverse(xs), ys)
{
fun
reverse(xs) = rappend(xs, nil)
and
rappend
(xs, ys) =
(
case xs of
| nil() => ys
| cons(x1, xs) => rappend(xs, cons(x1, ys))
)
} (* end of [append] *)

Note that the implementation of 'rappend' is tail-recursive.  The
tail-recusive version of 'append(xs, ys)' traverses 'xs' once to
construct its reverse and then traverses the reverse to perform
reverse-appending; the constructed reverse of 'xs' becomes garbage at
the end.

While using non-tail-recursion is probably fine in the construction of
a compiler, it is not the case in systems programming, where it is not
uncommon to see the requirement that only tail-recursive functions
(that is, loops) be allowed.

ATS offers much more than the usual ML-like FP. It supports so-called
linearly typed FIP where (linear) data structures can be updated in a
type-safe manner. With it, one can write in ATS type-safe programs
that are very close to their counterparts in C in terms of both
functionalities and performances.  Also, ATS supports type-safe manual
memory management of C-style, obviating the need for a big run-time
memory management system if the programmer so chooses.



For previously post messages:

https://github.com/githwxi/ATS-Xanadu/tree/master/docgen/NOTES

#

-- 
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/9f893be9-cde3-42bc-867a-8c17f3be53can%40googlegroups.com.

DML-style dependent types in ATS

[gmhwxi]

The dependent types in ATS are not the kind of full spectrum dependent types
as formulated in Martin-Lof's constructive type theory. I now refer to the 
dependent
types in ATS as DML-style dependent types, which I first formulated in 
Dependent ML
(DML), a language I designed and implemented as a part of my PhD thesis. 
Here
is a link to my paper on DML:

https://hwxi.github.io/PUBLICATION/MYDATA/DML-jfp07.pdf

People often claim that the type system of ATS is less powerful when 
compared to languages based on Martin-Lof's type theory. This claim is 
misleading at best. Let me
clarify.

There is a static component (statics) and a dynamic component (dynamics) in 
ATS;
types are in the statics and programs are in the dynamics. If we do want to 
support full spectrum dependent types in ATS, then the statics can be 
extended as such. However,
the statics and the dynamics are still separate. This separation is by 
design; it is really the
most salient feature of ATS.

Say we somehow find a way to merge the statics and the dynamics. This could 
only mean that many features in the dynamics must be abandoned, resulting 
in a language that may have more expressive types but fewer programming 
features. For instance, regardless how powerful Martin-Lof's type theory 
is, one simply cannot give in it an efficient tail-recursive implementation 
of the list-append function. But this can be readily done in ATS.

--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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/9ce2fe29-5b3b-424b-ba3f-b18e5524cb47n%40googlegroups.com.

Re: Some ATS2 library updates...

[gmhwxi]

>>Ideally, ATS package manager should be written in ATS :D (as in the worst 
case, it will require just a C compiler to be built)

For ATS3, the design I have is to support some form of internet-based code 
search.
This would make package management in ATS3 quite different. We could use 
tools
like npm and Connan after template resolution is completed. However, we do 
need a
"native" package management system for handling template resolution.

Speaking of template resolution, I'd like to mention a surprise I got not 
too long ago.

I wrote some ATS3 code and compiled it to JS and tested it successfully. 
Later l noticed that
I had not implemented the string comparison used in the ATS3 code. Why did 
my code work?
I realized that the compiler actually generated a function in JS for 
comparing strings by treating
a string as a sequence of characters and using the generic comparison 
function for sequences
to compare strings. In short, the sheer complexity of template resolution 
in ATS3 would  make
it very difficult for you to know what kind of code is generated by the 
compiler even if you yourself
wrote the source code.

On Sunday, May 30, 2021 at 9:42:43 PM UTC-4 ice.r...@gmail.com wrote:

> I can confirm, that having ghc (1 GB+) just to build ats package is 
> overkill.
> I am not speaking of cross compiling ghc to another architecture/libc is 
> pain as well, as it requires big amounts of RAM and 2+ hours of building 
> for stage1/stage2 compilers Then, you need to build cabal and only then 
> you will be able to build atspkg...
>
> Having to have/build python is not a pleasure as well, but at least, it is 
> not required to bootstrap itself :)
>
> Ideally, ATS package manager should be written in ATS :D (as in the worst 
> case, it will require just a C compiler to be built)
>
> For now I am using git with libraries being a git modules in $REPO/libs 
> directory, like this: https://github.com/dambaev/text/tree/master/libs
> and staloading appropriate modules like this:
> ```
> #define LIBS_targetloc "../libs" (* search path for external libs *)
>   
> #include "./../HATS/text.hats"
> #include "{$LIBS}/ats-bytestring/HATS/bytestring.hats"
> staload "{$LIBS}/result/src/SATS/result.sats"
> staload "{$LIBS}/foldable/src/SATS/foldable.sats"
> ```
>
> it can be not ideal for the case when "library A depends on C 1.0 and on B 
> 1.0 and at the same time B depends on C 1.1", as $REPO/libs will contain 1 
> version. At the same time, for handling such case you need to at least 
> properly handle symbol prefixes with  ATS_PACKAGE and ATS_EXTERN_PREFIX, so 
> I am not thinking about such case yet
>
> Ah yes, I am using NixOS and nix package manager to handle C/C++ libraries 
> dependencies, so what I usually need to build a project:
> ```
> $ nix-shell shell.nix
> nix-shell $ make
> ```
>
> I should try to use Conan, though, to check how it handles the 
> dependencies and such...
>
>

-- 
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/bcf9b81f-e199-4609-86af-a75b0fac8b19n%40googlegroups.com.

Re: Some ATS2 library updates...

[gmhwxi]

Thanks for sending this report.

I ran into Conan not too long ago but have not got time trying it yet.
So it is really great to learn your very positive experience with Conan.

Cheers!



On Sunday, May 30, 2021 at 1:20:28 PM UTC-4 randy...@gmail.com wrote:

>
> Hey all,
>
> I just wanted to let everyone know that I updated a bunch of the libraries 
> that I created last year (ats-http , 
> ats-epoll , ats-result 
> , and a bunch of others). I was 
> sort of frustrated with the overall build experience when working with ATS 
> libraries. I wanted a similar experience to Rust's cargo tool. I found 
> conan (https://conan.io) and it works really well, so I reworked all my 
> libraries to use it to manage library dependencies. Using conan, you can 
> specify libraries that an app/library depends on and their specific 
> versions. You can specify build dependencies (like ats-unit-testing 
> ) and pre-built binaries 
> are used, if available, otherwise the dependencies are built from source 
> and cached locally. I created a simple python class to be used in a conan 
> recipe to set the correct ATS include paths for all the dependencies (
> https://github.com/xran-deex/atsconan). All of my ATS libraries on my 
> github account  have been converted to use 
> conan. I'm also hosting these packages in my self-hosted conan package repo 
> (https://pkg.us.to) in case anyone decides to try this out. You can 
> either depend on any of these packages and just include the binaries, or 
> you can build everything from source. Anyway, I think it's pretty neat that 
> I can fetch all the dependencies, (optionally) build all the deps from 
> source, and build my package all in a few simple commands. Finally, I 
> updated my docker image to include conan (
> https://github.com/xran-deex/ats-docker), the docker image is on 
> dockerhub at xrandeex/ats2:0.4.2 . 
> I removed nodejs and npm from the docker image only because it made the 
> image size huge. I'm pretty sure no one is using it anyways (lol). I can 
> add it back, if anyone is actually using it. Also, I updated the ATS2 
> version to the latest (0.4.2).
>
> Has anyone ever used conan? I'd love to hear about your experience with 
> it. Anyway, hopefully this makes it easier to create and share ATS2 
> libraries with other developers. 
>
> Thanks!
> Randy
>

-- 
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/6726b7d2-90bf-4fd8-9de6-f4b58fd59232n%40googlegroups.com.

Re: agez vs addr > null

[gmhwxi]

At this point, 'addr' is mapped to 'int' in ATS2 as far as 
constraint-solving is of the concern.
We could try to make sure that a pointer of the type ptr(l) can never be 
constructed for any
negative l.

For instance, ptr_diff can be given the following type:

fun ptr_diff{l1,l2:addr | l1 >= l2} (p1: ptr(l1), p2: ptr(l2)): ptr(l1-l2)

On Saturday, May 22, 2021 at 9:02:19 PM UTC-4 Elronnd _ wrote:

> On Sun, 23 May 2021, Dambaev Alexander wrote:
>
> > ./prelude/basics_pre.sats:sortdef alez = { l:addr | l <= null }
> > 
> > it seems, that addr can be less than null, by the way :)
>
> On AMD64, it is fairly sensible to think of addresses as signed values.
>
> There is a set of addresses that are 'non-canonical' and cannot be 
> used--they will never map to anything. If you think about addresses as 
> signed, these non-canonical addresses are in the _middle_ of the space of 
> representable pointers; so the actual usable address space is segmented, 
> with one half at the bottom and one half at the top.
>
> But a simpler way to think about it is that an address is a 48-bit 
> _signed_ integer, which is sign-extended to 64 bits.
>
> See wikipedia 
> https://en.wikipedia.org/wiki/X86-64#Canonical_form_addresses
>
> (Though note that you're not very likely to ever encounter a negative
> address; usually the kernel lives in the 'top half' of the address space
> and userspace lives in the 'bottom half'.)
>
> -E
>

-- 
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/60d61cc0-dda2-4aa2-be3d-d597b60bcfebn%40googlegroups.com.

Re: ATS templates vs. C++ templates

[gmhwxi]

ATS2 does support partial template specialization.
For instance,

implement
(a)
fprint_list0(out, xs) = ...


On Thursday, May 20, 2021 at 11:26:15 PM UTC-4 ice.r...@gmail.com wrote:

> can I confirm, that ATS2 does not supports partial template specialization?
>
> пн, 6 июл. 2020 г. в 20:14, Hongwei Xi :
>
>> Wow! This is wild C++ code :)
>>
>> Can't support variadic stuff in ATS3. The type system for type-checking
>> in the presence of variadicity would be too complicated.
>>
>> I did an imitation of your code in ATS3:
>>
>> #extern
>> fun
>> 
>>  // N = n-i 
>> 
>> > ,i:i0>
>> dotprodN2
>> ( i0: int(i)
>> , xs: array(a, n)
>> , ys: array(a, n)): a
>> (* ** ** *)
>> impltmp
>> {a:t0}
>> {n:i0
>> ,i:i0}
>> dotprodN2
>> (_, _, _) = g_0()
>> (* ** ** *)
>> impltmp
>> {a:t0}
>> {D:t0}
>> {n:i0
>> ,i:i0}
>> dotprodN2
>> 
>> {n-i >= 1}
>> (i0, xs, ys) =
>> sub(xs,i0)*sub(ys,i0)+
>> dotprodN2(i0+1, xs,ys)
>> (* ** ** *)
>> val ans3 =
>> dotprodN2(0, B3, B3)
>> (* ** ** *)
>>
>> Right now, dependent type-checking is not yet implemented. Once dependent
>> type-checking is available, one should be able to capture array-bounds 
>> errors
>> (even in template implementations).
>>
>> In C++, templates are not type-checked; only template instantiations are 
>> type-checked.
>> In ATS, templates are type-checked before they can be used in 
>> instantiations. I suppose
>> that these two designs are rooted in fundamentally different philosophies 
>> regarding program
>> correctness and program verification.
>>
>> --Hongwei
>>
>>
>>
>> On Mon, Jul 6, 2020 at 3:34 PM Matthias Wolff  
>> wrote:
>>
>>> Some thoughts about the example (c++).
>>>
>>> In general this pattern is often used. This special example has the 
>>> disadvantage, 
>>> that the type T and the size N must be in any case explicitely declared 
>>> in the call 
>>> DotProduct::result(...). So here are two alternatives - dp1 and 
>>> dp2. 
>>> The first one uses fold expressions in combination with variadic 
>>> templates and the 
>>> second "if constexpr" for breaking the recursion. 
>>> (btw. inline is default within the struct)
>>>
>>> #include 
>>> #include 
>>> #include 
>>>
>>> namespace detail {
>>> 
>>> template
>>> T dp_(T ()[N], T ()[N], std::index_sequence) {
>>> return ((a[I] * b[I])+...);
>>> }
>>> 
>>> }
>>>
>>> template
>>> T dp1(T ()[N], T ()[N]) {
>>>
>>> return detail::dp_(a,b,std::make_index_sequence{});
>>> }
>>>
>>>
>>> template
>>> T dp2(T ()[N], T ()[N]) {
>>>
>>> if constexpr (N == P) { return T{0}; } else {
>>> 
>>> return a[P] * b[P] + dotprod(a,b);
>>> }
>>> }
>>>
>>> int main()
>>> {
>>> int a[] = {1,2,3};
>>> int b[] = {4,5,6};
>>> 
>>> std::cerr << dp2<0>(a,b) << std::endl;
>>> 
>>> std::cerr << dp1(a,b) << std::endl;
>>>
>>> return 0;
>>> }
>>>
>>> Am 06.07.20 um 18:31 schrieb gmhwxi:
>>>
>>>
>>> Here is an example of template metaprogramming in ATS3:
>>>
>>> (* ** ** *)
>>> abstype Z
>>> abstype S(type)
>>> (* ** ** *)
>>> #extern
>>> fun
>>> 
>>> 
>>> 
>>> dotprodN
>>> ( xs: array(a, n)
>>> , ys: array(a, n)): a
>>> (* ** ** *)
>>> impltmp
>>> {a:t0}
>>> dotprodN
>>> <0>(_, _) = g_0()
>>> (* ** ** *)
>>> impltmp
>>> {a:t0}
>>> {N:t0}
>>> {n1:i0}
>>> dotprodN
>>> 
>>> {n1 > 0}(xs, ys) =
>>> head(xs)*head(ys)+dotprodN(tail(xs),tail(ys))
>>> (* ** ** *)
>>>
>>> The above ATS code roughly corresponds to the following C++ code:
>>>
>>> template
>>>
>>> struct DotProductT {
>>>
>>> stati

Re: Finding Strings within Strings in ATS

[gmhwxi]

Your question got me thinking :)

I feel that ATS3 is not yet suitable right now.

I am focusing on implementing a typechecker for linear and dependent types.
After that, I suppose I can polish it a bit and then make a release.

--Hongwei



On Monday, March 1, 2021 at 9:11:13 PM UTC-5 d4v3y_5c0n3s wrote:

> Thank you for the suggestions.  I decided to sidestep my need to _ for 
> now.  While atscntrb-hx-libpcre seems like it would suit my needs, I'd 
> rather not require people to install too many external libraries.  Is ATS3 
> suitable for writing libraries for currently?  Because if I were to 
> implement string processing functions it would make the most since to do it 
> for ATS3.
>
> On Sunday, February 28, 2021 at 11:35:29 AM UTC-5 gmhwxi wrote:
>
>> Thanks for the link. I will take a look.
>>
>>
>> On Saturday, February 27, 2021 at 6:04:13 PM UTC-5 Elronnd _ wrote:
>>
>>> On Sat, 27 Feb 2021, gmhwxi wrote: 
>>> > As for building an ecosystem for ATS3, I am thinking about a way for 
>>> > contributed packages to be hosted on-line. Not much progress is made 
>>> at 
>>> > this stage, though. 
>>>
>>> Have you seen 
>>> https://github.com/vmchale/atspkg/blob/master/ats-pkg/README.md ? 
>>>
>>

-- 
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/d5f5c0d2-13ff-42d9-8d12-0241ad93ef33n%40googlegroups.com.

Re: Finding Strings within Strings in ATS

[gmhwxi]

Thanks for the link. I will take a look.


On Saturday, February 27, 2021 at 6:04:13 PM UTC-5 Elronnd _ wrote:

> On Sat, 27 Feb 2021, gmhwxi wrote:
> > As for building an ecosystem for ATS3, I am thinking about a way for 
> > contributed packages to be hosted on-line. Not much progress is made at 
> > this stage, though.
>
> Have you seen 
> https://github.com/vmchale/atspkg/blob/master/ats-pkg/README.md ?
>

-- 
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/25e8671c-b752-4565-ba9e-ad541669e2d7n%40googlegroups.com.

Re: Finding Strings within Strings in ATS

[gmhwxi]

I myself have been using the PCRE library:

https://github.com/githwxi/ATS-Postiats/tree/master/contrib/atscntrb/atscntrb-hx-libpcre

There is also the SDSTRING library available.

You are welcome to implement a library of string manipulation functions. 
And I am happy to
add it to https://github.com/githwxi/ATS-Postiats-contrib for now.

As for building an ecosystem for ATS3, I am thinking about a way for 
contributed packages to
be hosted on-line. Not much progress is made at this stage, though.

--Hongwei




On Thursday, February 25, 2021 at 8:44:24 AM UTC-5 d4v3y_5c0n3s wrote:

> I was searching through the prelude looking for a way to find a 
> formatted string within another string in ATS, but there doesn't seem to be 
> a built-in way to do this.  Before I make something myself, I just wanted 
> to see what opinions there are on the best way to perform this operation in 
> ATS.
> Do you think I should use the C standard library through ATS' ability 
> to call inline C code?  Should I just loop through a strnptr and manually 
> check the chars?  Personally, I want to try using linear streams here to 
> take advantage of their low-memory overhead (and because I've fallen 
> straight into the "once you have a hammer everything looks like a nail" 
> trap with linear streams.)  But, I want to hear what others think, so 
> please let me know which solution you think is best.
> As a side note, should we add more string manipulation capabilities to 
> the prelude?  I don't know what Hongwei's stance on this is, but if he 
> thinks it would be a good idea I'd be willing to contribute these functions 
> to the prelude.
>

-- 
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/e340f663-2266-45df-8579-a4191a257c50n%40googlegroups.com.

Re: current status of libxatsopt

[gmhwxi]

Currently, libxatsopt supports the following functionalities:

1: parsing: source to level-0 syntax
2: trans01: translating from level-0 to level-1 (for resolving fixity 
issues)
3: trans12: translating from level-1 to level-2 (for resolving binding 
issues)
4: trans23: translating from level-2 to level-3 (for resolving overloading 
issues)
5: trans33: translating from level-3 to level-3 (for performing 
type-inference)
6: trans3t: translating from level-3 to level-3 (for performing template 
resolution)
7: trans3x: translating from level-3 to level-3 (for normalizing types and 
classifying variables)
8: tcomp30: translating from level-3 to XATSCML (C/ML-like intermediate 
language)

The following projects are currently built on the top of libxatsopt

1: xinterp: an interpreter for level-3 syntax
2: xats2js: a transpiler from XATSCML to JavaScript

I am actively working type-checking in ATS3 for dependent types and linear 
types.

Cheers!

--Hongwei


On Saturday, February 20, 2021 at 11:04:10 PM UTC-5 ice.r...@gmail.com 
wrote:

> Hi,
>
> HX: can you add anything to 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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/3eb57b98-6abd-419a-bc7b-aea04ec721e8n%40googlegroups.com.

A talk by Deech on ATS

[gmhwxi]

FYI.

I was recently told of the following video:

https://youtu.be/c4Z25DJusuo

Kudos to Aditya "Deech" Siram!

--Hongwei

BTW, please wait until the template stuff 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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/21eaf57a-b2e2-4423-9370-9b2020ac408en%40googlegroups.com.

Re: An interesting GCC (v5.4.0) bug

[gmhwxi]

Is there an easy way to trap individual arithmetic operations?

Here is some code I wrote a few year ago:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/MISC/arith_overflow.dats

It would nice to make sure that only provably non-wrapping arithmetic 
operations are not trapped.

Thanks!

On Saturday, January 30, 2021 at 7:57:19 PM UTC-5 Elronnd _ wrote:

> On Sat, 30 Jan 2021, gmhwxi wrote:
>
> > But this is kind of like punting the problem to the user :(
> > The compiler should really generate code that raises an exception
> > (just like in the case of 1/0).
>
> You can do that with -ftrapv.
>

-- 
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/ce542b4a-fbb9-4d0c-b607-8e831c3619b7n%40googlegroups.com.

Re: An interesting GCC (v5.4.0) bug

[gmhwxi]

To me, it would be a better design if -ftrapv was actually the default.


On Saturday, January 30, 2021 at 7:57:19 PM UTC-5 Elronnd _ wrote:

> On Sat, 30 Jan 2021, gmhwxi wrote:
>
> > But this is kind of like punting the problem to the user :(
> > The compiler should really generate code that raises an exception
> > (just like in the case of 1/0).
>
> You can do that with -ftrapv.
>

-- 
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/d5ef1f58-8af9-40d6-895f-90e1947702f4n%40googlegroups.com.

Re: An interesting GCC (v5.4.0) bug

[gmhwxi]

Oh, I see.

But this is kind of like punting the problem to the user :(
The compiler should really generate code that raises an exception
(just like in the case of 1/0).


On Saturday, January 30, 2021 at 7:04:22 PM UTC-5 Elronnd _ wrote:

> On Sat, 30 Jan 2021, gmhwxi wrote:
>
> > Without -O2, the executable generated by gcc returns 32. With -O2, it is 
> > a non-terminating loop. Clearly, gcc assumes (with -O2) that the sum of 
> > two positive integers is also positive (but it is obviously false when 
> > modulo arithmetic is involved). BTW, clang does NOT have this issue.
>
> It's actually not a bug!
>
> In c, signed integer overflow is considered undefined behaviour, so the 
> compiler is free to treat is as nonterminating instead of wrapping. And 
> in fact, my version of clang (11.0.1) returns 33 for that function.
>
> If you want the compiler to treat integer overflow as wrapping, you have 
> to pass it -fwrapv.
>
> -E
>

-- 
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/685bc21f-43b5-4915-b3c7-9b05deef910cn%40googlegroups.com.

Re: Effect tracking by omitting proof variables in calls

[gmhwxi]

This idea sounds familiar to me. I thought along similar lines.

The current support for '!' is hard-baked in the type-checker for ATS2.
All I could say for now is that we really need to think about an extension
of ATS where this kind of proof synthesis can be effectively supported.


On Friday, January 29, 2021 at 11:52:57 PM UTC-5 ice.r...@gmail.com wrote:

> and this is my playground just in case if someone do not like to read code 
> in the email: 
> https://github.com/dambaev/ats-complexity/blob/master/src/TEST/
>

-- 
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/cbc08cac-fbc1-4fc7-abdd-7afcd7340641n%40googlegroups.com.

An interesting GCC (v5.4.0) bug

[gmhwxi]

I tried the following example today.

Without -O2, the executable generated by gcc returns 32.
With -O2, it is a non-terminating loop. Clearly, gcc assumes
(with -O2) that the sum of two positive integers is also positive
(but it is obviously false when modulo arithmetic is involved).
BTW, clang does NOT have this issue.

This kind of bug is really scary, isn't it ?!

implement
int_test() =
(
  loop(0, 1)
) where
{
fun
loop
(n: int, i: int): int =
(
println!
("loop(", n, ", ", i, ")");
if i = 0 then n else loop(n+1, i+i)
)
}

--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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/e40e8674-5951-423a-9f74-b5cec878e5fcn%40googlegroups.com.

Re: Support for OOP in some ATS3 extension (2)

[gmhwxi]

As I have planned so far, an ATS3 extension is supposed to be compiled to 
ATS3 proper, which is then compiled to XATSCML.

If I understand what you said above, what is needed is some sort of 
XATSCML++ to which an ATS3 extension can target directly.
And from XATSCML++ one can then get to C++ (or Java).

One big reason for me to like C and ML is that data representation in them 
is transparent. From the (concrete) type of a value, you
can readily tell how such a value is represented in the memory. And XATSCML 
follows this tradition.


On Wednesday, January 20, 2021 at 10:36:14 PM UTC-5 ice.r...@gmail.com 
wrote:

> Hi,
> It might be offtopic, but the primary goal of my question in the past 
> about OOP support in ATS was to understand if it will be possible to:
> 1. write bindings  to use gtk2+ - style of OOP;
> 2. write bindings/generate source code of classes in a target language. 
> Although, C ABI is probably still provides the best support for FFI between 
> different languages, I noticed, that quite few projects/frameworks provide 
> C API nowadays. So, if we imagine, that at some point, we will have a 
> translators into C++ (say, for using wth Unreal Engine) or Java (say for 
> android): will it be possible to render a proper classes on the target 
> languages or are we still damned for a pain of providing FFI glue? I guess, 
> that I know the answer myself, but sometimes I like to imagine, that no FFI 
> glue should be needed at some point :)
>
> вт, 19 янв. 2021 г. в 00:01, Hongwei Xi :
>
>>
>> > This time I would like to do something a bit more interesting:
>>> > 
>>> > class
>>> > >> > , b:type>
>>> > mygpair(a, b)
>>> > *snip*
>>>
>>> Do we need to say both  and (a,b)?  It seems redundant, 
>>> since we already know the class is parametrized according to a and b, 
>>> but 
>>> maybe I'm missing something?
>>>
>>
>> Again this is an issue with the OOP syntax. We have the following 
>> possibilities
>> for the interface of mygpair_copy:
>>
>> fun mypair_copy{a:type,b:type}(obj: !mypair(a, b)): mypair(a, b)
>> fun mypair_copy(obj: !mypair(a, b)): mypair(a, b)
>>
>> Given that OOP syntax is quite restrictive anyway, we could decide to 
>> always
>> choose the second possibility. If so, we can just write:
>>
>> class mypair(a:type, b:type) {
>>...
>> }
>>
>> --Hongwei
>>
>> On Mon, Jan 18, 2021 at 3:51 AM Elijah Stone  wrote:
>>
>>> On Sun, 17 Jan 2021, gmhwxi wrote:
>>>
>>> > This time I would like to do something a bit more interesting:
>>> > 
>>> > class
>>> > >> > , b:type>
>>> > mygpair(a, b)
>>> > *snip*
>>>
>>> Do we need to say both  and (a,b)?  It seems redundant, 
>>> since we already know the class is parametrized according to a and b, 
>>> but 
>>> maybe I'm missing something?
>>>
>>>
>>> > The mygpair(T1, T2) is a so-called generic class parameterized over 
>>> > types T1 and T2. For an object of the type mygpair(T, T), a method for 
>>> > swapping the fst and snd components of the object can be supported. 
>>> But 
>>> > this is difficult to do with the OOP syntax. BTW, how would be done in 
>>> > Java? Such a method can be readily implemented with the following 
>>> > syntax:
>>> > 
>>> > fun
>>> > 
>>> > swap(pp: mygpair(a, a)): void =
>>> > let
>>> > val tmp = pp.fst in pp.fst := pp.snd; pp.snd := tmp
>>> > end
>>>
>>> Hmmm.  In a language like c++ where templates are not checked until 
>>> they're instantiated, you would be able to just make that a template 
>>> method.  That doesn't work so well in practice, however...
>>>
>>> One possible solution is subtyping.  As in:
>>>
>>> class  mypair(a, b) {
>>> var fst: a
>>> var snd: b
>>> //...
>>> }
>>>
>>> class  mysamepair(a): mypair(a, a) {
>>> method swap(): void = ...
>>> }
>>>
>>>   -E
>>>
>>> -- 
>>> 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/snZWQK2YePY/unsubscribe
>>> .
>>> To unsubscribe from this group and all its topics, send an email to 
>>> ats

Linearly typed OOP

[gmhwxi]

Over the years, I read a lot of OOP stuff. Once I understand that
types for objects should be linear, I realize that people writing OOP
stuff often just talk about "philosophy". And we all know that people
talk about philosophy tend to quarrel a lot :)

OOP is all about changing encapsulated states. However, if you take
a look at typed OOP as is done is C++ and Java, the type of an object
never changes due to a method.

Say we have a rectangle class; in the class, there is a method of doubling
the width of an rectangle object. People realize that this method turns a
square into a non-square rectangle. So they say that square is not a 
subclass
of rectangle; it is actually the other way around: a rectangle is a 
subclass of
square; and subclass is not like subtype; etc., etc., etc., ...

Linear types in ATS helped me understand OOP; they saved me from the 
insanity
of people talking about OOP "philosophy".

--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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/49114d56-2daa-437d-a3da-0418f4118213n%40googlegroups.com.

Support for OOP in some ATS3 extension (2)

[gmhwxi]

This time I would like to do something a bit more interesting:

class

mygpair(a, b)
{
 var fst: a
 var snd: b
   
 cnstor // constructor
 mygpair(x1: a, x2: b) =
 (this.fst := x1; this.snd := x2; this)

 method get_fst(): a = this.fst
 method set_fst(x1: a): void = this.fst := x1

 method copy(): mygpair(a, b) = mygpair(this.fst, this.snd)
}

The mygpair(T1, T2) is a so-called generic class parameterized over types 
T1 and T2.
For an object of the type mygpair(T, T), a method for swapping the fst and 
snd components
of the object can be supported. But this is difficult to do with the OOP 
syntax. BTW, how would
be done in Java? Such a method can be readily implemented with the 
following syntax:

fun
 
swap(pp: mygpair(a, a)): void =
let
val tmp = pp.fst in pp.fst := pp.snd; pp.snd := tmp
end

In summary, the OOP syntax is a form of syntactic sugar; it brings 
convenience; its limitation can
be easily remedied.

--Hongwei


On Monday, January 18, 2021 at 2:27:48 AM UTC-5 gmhwxi wrote:

>
> FYI.
>
> While I am still working on type-checking for linear types and dependent 
> types
> right now, I do occasionally think about how meta-programming support can 
> be
> added to an ATS3 extension. I would like to outline as follows one way to 
> support
> OOP, trying to clarify and also solicit some feedback.
>
> First, I would like to point out that (linear) objects can already be 
> constructed in
> ATS. The support for OOP I outline can be seen as a form of syntactic 
> sugar for
> meta-programming (that is, the OOP syntax is supposed to be translated 
> back into
> ATS). Also I leave out the issue of supporting inheritance here for a 
> simplified
> presentation.
>
> Let us first see some pseudo code:
>
> class
> mypair {
>
> var fst: int
> var snd int 
>
> cnstor // constructor
> mypair(x1: int, x2: int) =
> (this.fst := x1; this.snd := x2; this)
>
> method get_fst(): int = this.fst
> method set_fst(x1: int): void = this.fst := x1
>
> method copy(): mypair = mypair(this.fst, this.snd)
> }
>
> This pseudo code can be translated into the following ATS code:
>
> absvwtp mypair // abstract
>
> local
>
> absimpl mypair = $(int, int)
>
> in
>
> fun
> mypair(x1: int, x2: int): mypair = $(x1, x2)
> fun get_fst(pp: !mypair): int = pp.0
> fun set_fst(pp: !mypair, x1: int): void = pp.0 := x1
> fun copy(pp: !mypair): mypair = mypair(pp.0, pp.1)
>
> end
>
> So the pseudo OOP syntax is helpful but does not seem to buy a lot.
> I will point out in the next message that the OOP syntax is actually quite
> restrictive.
>
> --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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/e4b77bc0-265d-47b7-b725-22a7f4e094b7n%40googlegroups.com.

Support for OOP in some ATS3 extension (1)

[gmhwxi]

FYI.

While I am still working on type-checking for linear types and dependent 
types
right now, I do occasionally think about how meta-programming support can be
added to an ATS3 extension. I would like to outline as follows one way to 
support
OOP, trying to clarify and also solicit some feedback.

First, I would like to point out that (linear) objects can already be 
constructed in
ATS. The support for OOP I outline can be seen as a form of syntactic sugar 
for
meta-programming (that is, the OOP syntax is supposed to be translated back 
into
ATS). Also I leave out the issue of supporting inheritance here for a 
simplified
presentation.

Let us first see some pseudo code:

class
mypair {

var fst: int
var snd int 

cnstor // constructor
mypair(x1: int, x2: int) =
(this.fst := x1; this.snd := x2; this)

method get_fst(): int = this.fst
method set_fst(x1: int): void = this.fst := x1

method copy(): mypair = mypair(this.fst, this.snd)
}

This pseudo code can be translated into the following ATS code:

absvwtp mypair // abstract

local

absimpl mypair = $(int, int)

in

fun
mypair(x1: int, x2: int): mypair = $(x1, x2)
fun get_fst(pp: !mypair): int = pp.0
fun set_fst(pp: !mypair, x1: int): void = pp.0 := x1
fun copy(pp: !mypair): mypair = mypair(pp.0, pp.1)

end

So the pseudo OOP syntax is helpful but does not seem to buy a lot.
I will point out in the next message that the OOP syntax is actually quite
restrictive.

--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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/0b9b2e49-5fa3-49e8-9dff-89c3b783a7b7n%40googlegroups.com.

Re: Is It Possible to Pass a Function Template as a Parameter?

[gmhwxi]

Sorry, this is still a bit unclear to me. What does a typical instance of 
map_test look like?
On Sunday, January 3, 2021 at 1:19:38 AM UTC-5 d4v3y_5c0n3s wrote:

> Here's what I'm talking about:
> I know that I can currently create a function template which takes in a 
> function as a parameter, which can be observed below:
> fn{a:vt@ype} map_test ( t: , mapper: a - void ) : void
>
> But, let's say that the 'test' typedef is as follows:
> vtypedef test = [a:vt@ype] ( a )
>
> In this instance, the function 'map_test()' will not work for the type 
> 'test' because the passed mapping function 'mapper' may not necessarily 
> take in the correct type (the 'test' type essentially hides the type it 
> contains.)  Of course, 'test' could be rewritten to take in a type, 
> allowing the type checker to verify that the type within 'test' matches.  
> Doing so would look like this:
> vtypedef test(a:vt@ype) = ( a ) 
>
> But, what if I want the type within 'test' to remain hidden?  If 'mapper,' 
> instead of being a function, was a template, then it would compile (given 
> said template had the proper implementations.)  Essentially, instead of me 
> wanting to verify that 'mapper' will take in the given vt@ype 'a', I want 
> 'mapper' to reference a function template which then will be specifically 
> implemented for any needed types.  Then, I could create a generic map 
> function template that would work on a type which hides its contained 
> generic type.  I'll admit, this is a pretty niche use case, but I wanted to 
> know whether I could indeed do this.
>
> I've already found a way to work around this via the use of local template 
> instantiation, which may be the better way to handle things anyways.
>
> Please let me know if this example is insufficient.
> On Saturday, January 2, 2021 at 9:59:20 PM UTC-5 gmhwxi wrote:
>
>> Yes, I would like to see an example of this kind.
>>
>>
>> On Sat, Jan 2, 2021 at 9:19 PM d4v3y_5c0n3s  wrote:
>>
>>> So, I know that  it's possible to pass a function to another function as 
>>> a parameter, but what if I want to pass a function template specifically?  
>>> If anyone would like some clarification, I can try to provide some examples 
>>> of what I'm trying to achieve. 
>>>
>>> -- 
>>> 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 view this discussion on the web visit 
>>> https://groups.google.com/d/msgid/ats-lang-users/96fc4ec0-8355-4b32-883a-30f2293b4861n%40googlegroups.com
>>>  
>>> <https://groups.google.com/d/msgid/ats-lang-users/96fc4ec0-8355-4b32-883a-30f2293b4861n%40googlegroups.com?utm_medium=email_source=footer>
>>> .
>>>
>>

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/bf4940d2-a5e6-42ec-af41-50285914bc08n%40googlegroups.com.

Re: Building ATS2 from Github head.

[gmhwxi]

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 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/87cbe011-5997-4d96-a439-2522ced8e8adn%40googlegroups.com.

Building packages for ATS3

[gmhwxi]

Hi, there,

HX-2020-12-12:

##
#
# Building packages for ATS3
#
##

I have long been contemplating on building an ecosystem for ATS.

In the past, I did various experiments and, in particular, played
with an idea of using npm for distributing packages written in/for
ATS. And Ryan King even started to build a package management
system (PMS) for ATS (see https://github.com/RyanTKing/wombats for
more details). As always, you are welcome to share your ideas!

One thing seems rather clear to me is that any PMS for ATS should be
closely connected to the support for template resolution in ATS3. At
this stage, I have to stress that I am not yet clear as to how such a
connection can and should be made. Instead of forging something that
is yet to become more concrete, I plan to keep options open maximally
by simply using the github to distribute packages for now.

##

I created the following repo:

https://github.com/xanadu-lang/contrib

for hosting contributed packages. I put some of my packages there
for people to see. Mostly I intend to put links there to packages
stored elsewhere.

So far you can find the following packages:

https://github.com/xanadu-lang/contrib/tree/master/githwxi/StreamDemo
https://github.com/xanadu-lang/contrib/tree/master/githwxi/StreamDemo2

I suggest that a directory of the name TEST be included in a package;
this directory should contain at least one example that shows how the
package can actually be used. Of course, more documentation is better.

##

StreamDemo:

In the package StreamDemo, there are some functions for displaying
streams. Essentially, StreamDemo can turn a given stream into another
stream that allows the items in the given stream to be displayed in a
webpage. An an analogy, if we see a stream as a tape of some sort,
StreamDemo provides functions for building a machine to view such a
tape. StreamDemo is entirely template-based.

Animating the involved depth-first search for solving the 8-queen puzzle:
https://xanadu-lang.github.io/contrib/githwxi/StreamDemo/TEST/QueenPuzzle/2020-12-10/

##

StreamDemo2:

In the package StreamDemo2, which builds on top of StreamDemo, there
is a webpage for viewing a stream; some contents of the webpage can be
specialized for any chosen stream. As StreamDemo2 needs to interact
with JavaScript (JS), it cannot be entirely template-based. Instead.
it contains a template portion (StreamDemo2.dats) and a non-template
portion (StreamDemo2_.dats); the latter provides functions that can
be called directly in JS.

Enumerating prime numbers:
https://xanadu-lang.github.io/contrib/githwxi/StreamDemo2/TEST/PrimeNums/2020-12-12/

Enumerating Fibonacci numbers:
https://xanadu-lang.github.io/contrib/githwxi/StreamDemo2/TEST/Fibonacci/2020-12-12/

Animating the involved depth-first search for solving the 8-queen puzzle:
https://xanadu-lang.github.io/contrib/githwxi/StreamDemo2/TEST/QueenPuzzle/2020-12-12/

##

I hope you find it interesting. Moreever, you can use these packages (or 
something
of your own) to build more packages for displaying streams and share them.

##

Cheers!

--Hongwei

##

For previously post messages:

https://github.com/githwxi/ATS-Xanadu/tree/master/docgen/NOTES

##

-- 
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/a645c195-5149-4587-bb86-e1995dc8d29bn%40googlegroups.com.

Re: Read IO and Write IO

[gmhwxi]

>>You may be right. Can you provide some scatch of your view just to check 
it out? :)

Unfortunately, I don't have concrete stuff to show at this moment.

To me, effect-tracking is not type-theoretic; it is just a form of 
so-called flow analysis.
The approach described in your message traverses the syntax tree by 
piggy-backing
on the Haskell type-checker. 

Tracking exceptions has been done many times by many different people 
(e.g., David Gifford,
Alex Aiken, K-G. Yi). I remember attending a POPL talk (about 20 years ago) 
by Xavier Leroy;
it was about some kind of effect-tracking system he implemented for OCaml. 
Immediately after
he finished the talk, Matthias Felleison, who was standing behind me, 
shouted out a comment
claiming that they did something similarly for Racket(?) and found it to be 
USELESS :)

In the presence of higher-order functions, accurate flow analysis is very 
difficult to achieve if not
practically impossible. To me, the key to success lies in flow-analyzing 
code containing very few
higher-order functions (if they cannot be completely removed). Instead of 
performing effect-tracking
on source code, it is likely more effective to do it on intermediate 
representations (e.g., XATSCML and
XATSCL0).

Cheers!

--Hongwei


On Tuesday, November 24, 2020 at 1:38:45 AM UTC-5 ice.r...@gmail.com wrote:

> You may be right. Can you provide some scatch of your view just to check 
> it out? :)
>
> вт, 24 нояб. 2020 г. в 06:24, gmhwxi :
>
>> Thanks for the message!
>>
>> What I said is not in conflict with what you described in the message.
>>
>> An external tool for tracking effects can be quite useful in large scale 
>> programming.
>> Deciding what effects should be tracked is often open-ended; what is 
>> decided today
>> may not be what is wanted tomorrow.
>>
>> The type-based approach you described becomes quite burdensome once 
>> higher-order
>> functions are present. A big difficulty in effect-tracking lies precisely 
>> in handling higher-order
>> functions.
>>
>> On Monday, November 23, 2020 at 10:57:41 PM UTC-5 ice.r...@gmail.com 
>> wrote:
>>
>>> Maintaining some external file seems to me as something, which is easy 
>>> to ignore or easy to forget about and without some scatch of of example of 
>>> usage, I can't see how it will be helpful at all.
>>>
>>> For example:
>>> ```
>>> fn foo(): void = println!("hello")
>>> implement main0() = foo()
>>> ```
>>> and the external file contains:
>>> ```
>>> console: println
>>> ```
>>> Do you mean, that such external tool should require foo and main0 to be 
>>> listed in such file?
>>> In this case, it will still be absent in types so it will be hard to 
>>> answer a questions like: "what effects contains foo?" or main0 as well.
>>>
>>> In contrast, by using proof arguments you will actually see, that in 
>>> order to use foo you need to pass IO:
>>> so it is clearer to understand, but more verbose as well, as main0 will 
>>> be probably a source of all kind of effects, like:
>>> ```
>>> extern prfn use_console( !IO): Console
>>> fn
>>>   foo
>>>   ( console: !Console
>>>   |
>>>   ): void = println!( console, "hello")
>>> implement main0(io | ) = {
>>>   prval console = use_console( io)
>>>   val () = foo( console | )
>>> }
>>> ```
>>>
>>> another interesting approach will be to wrap the exceptions (ie, the 
>>> goal is to see in types which exceptions are possible to be thrown from 
>>> function), so $raise should have type like:
>>> ```
>>> extern fn
>>>   $raise
>>>   {a:type}{b:type| // is there an exception sort?
>>>   ( !Throws(a)
>>>   | a
>>>   ): b
>>> ```
>>> then `try` should require `!IO` and bring `Throws(a)` for all branches 
>>> in `with`, like:
>>> ```
>>> fn
>>>foo
>>>   ( Throws( DivisionByZero)
>>>   , Throws(FileNotFound)
>>>   | a: int
>>>   , b :int
>>>   ): int = a / b
>>>
>>> implement main0() = 
>>> try 
>>>   ( try foo() with // I am not sure if foo() will be able to use 
>>> Throws(..) implicitely
>>>   | ~DivisionByZero() => ... // this brings Throws(DivisionByZero) into 
>>> the scope and only within this block of try ... with
>>>   ) with
>>>   | ~FileNotFound() => ... // this brings Throws(FileNotFound) into the 
>>> scope
>>> ```
>

Re: Current Status of ATS3 (2020-11-22)

[gmhwxi]

Hi Andreas,

First, thanks for your past postings. I picked up a lot info from reading 
them.

As for as I can tell, this vision of architecting ATS/Xanadu as a network 
of AST-to-AST transform-based extension points is currently
being put into practice. So far, this network is just a line connectomg 
some AST transform functions: parse, trans01, trans12, trans 23, etc.
This line is expected to be turned into a tree (or even a graph) in the 
future.
On Monday, November 23, 2020 at 5:17:35 PM UTC-5 zuercher...@outlook.com 
wrote:

> Hongwei,
> In your 16dec2019 posting & its replies
> https://groups.google.com/g/ats-lang-users/c/TnL5h-_mDOQ/m/35X4gneUBgAJ
> you mentioned that your intended software architecture for the ATS3 
> compiler under development would have stages at which AST-to-AST transforms 
> would be a key facilitator of extension functionality.  Some such 
> AST-to-AST transforms might include, e.g., alternative syntax, full OOP 
> that partially impairs programming-by-proofs, partial OOP that does not 
> impair programming-by-proofs at all, alternative logic solvers, LLVM 
> backend, and so forth.
>
> In your reply on 29aug2020
> https://groups.google.com/g/ats-lang-users/c/fJWbXeOraDU/m/lcfFdhQfAgAJ
> it might seem that OOP might be such an extension that fits somewhere in 
> the AST-to-AST transforms.
>
> Has this vision of architecting the ATS3 compiler as having the 
> originally-intended AST-to-AST transform-based extension points come to 
> fruition (perhaps in some early not-final form) at this release?  Or did 
> some trade-offs along the way cause these AST-to-AST transform-based 
> extension points to be postponed for a while into the future?
>
> On Sunday, November 22, 2020 at 8:31:16 AM UTC-6 gmhwxi wrote:
>
>>
>>
>> Hi, there, 
>>
>> HX-2020-11-22: 
>>
>> (* 
>> HX-2018-04-07: Let us get started!!! 
>> *) 
>>
>> As of today, I am pleased to announce that ATS3 has reached a stage 
>> where it can be realistically used in software construction. This is 
>> achieved after slightly more than two and one-half years of continual 
>> development by yours truly :) 
>>
>> ## 
>> # 
>> # The current status 
>> # 
>> ## 
>>
>> XATSOPT: 
>>
>> Xatsopt is a functioning compiler implemented in ATS2 for translating 
>> ATS3 into a typed intermediate language of the name XATSCML, which is 
>> both C-like and ML-like. It is planned for xatsopt to further 
>> translate XATSCML into XATSCL0, a low-level C-like language. I now 
>> primarily see xatsopt as a library (libxatsopt) for implementing tools 
>> to support programming with ATS3. 
>>
>> XATS2JS: 
>>
>> Xats2js is a functioning compiler implemented in ATS2 for translating 
>> XATSCML into JavaScript (or JS for short). It should be noted that 
>> xats2js can compile tail-recursive calls into local jumps, effectively 
>> supporting the common practice in functional programming of writing 
>> loops as tail-recursive functions. 
>>
>> I will give detailed explanation elsewhere on using xats2js. Generally 
>> speaking, one can now practice a form of co-programming with ATS3 and 
>> JS. The JS code generated by xats2js from compiling ATS3 source can be 
>> directly combined with other JS code (as if the generated code were 
>> manually written in JS) 
>>
>> ## 
>> # 
>> # Future Development 
>> # 
>> ## 
>>
>> Documenting Xatsopt: 
>>
>> This has been assigned a high priority. It is hoped that other 
>> people interested in ATS3 can start developing tools for ATS3 after 
>> a minimal amount of documentation on xatsopt is made available. 
>>
>> Advanced Type-Checking: 
>>
>> While one can specify with linear types and dependent types in ATS3, 
>> there is no type-checking for such advanced types in xatsopt. I plan 
>> to concentrate on implementing support for such type-checking in the 
>> next phase of ATS3 development. 
>>
>> ## 
>> # 
>> # A little history of ATS3 
>> # 
>> ## 
>>
>> Essentially, ATS3 refers to the third edition of ATS, and ATS/Xanadu 
>> is currently the only implementation of ATS3. Note that the names ATS3 
>> and ATS/Xanadu are often used interchangeably. 
>>
>> In the ATS family of languages, the first implementation is named 
>> ATS/Proto (2004) and the language it implements is referred to as 
>> ATS0. Please note that the implementation of ATS/Proto is written in 
>> OCaml. The next implementation is ATS/Geizella (2007), which is also 
>> written in OCam

Re: Current Status of ATS3 (2020-11-22)

[gmhwxi]

>> *will this change affect the execution speed of ATS3 code compared to 
ATS2?* 

The short answer is no. If anything, I would bet that ATS3 code should run 
faster :)
I will strive to structure the compiler in a way that should be easy for 
others to contribute.

On Monday, November 23, 2020 at 11:20:59 PM UTC-5 d4v3y_5c0n3s wrote:

> Thanks for the update, Hongwei.  It's really awesome to hear about the 
> progress being made on ATS3!  I have a question I'd like to ask about 
> ATS3's compilation.  You mentioned that rather than compiling ATS code 
> straight into a C file, that ATS3 first compiles it into XATSCML, and in 
> the future into XATSCL0.  You said this was to make it easier to compile 
> ATS into languages other than C, which is awesome and I can definitely 
> appreciate that.  My question is, *will this change affect the execution 
> speed of ATS3 code compared to ATS2?*  I ask because I am currently 
> working on building a game engine in ATS, and so performance is very 
> important to my use case.  If ATS3 could potentially be slower than ATS2 
> was, please let me know, I'd be willing to try and contribute to the 
> project to improve this aspect.
> Thanks, and good luck with ATS3.
>
> On Sunday, November 22, 2020 at 9:31:16 AM UTC-5 gmhwxi wrote:
>
>>
>>
>> Hi, there, 
>>
>> HX-2020-11-22: 
>>
>> (* 
>> HX-2018-04-07: Let us get started!!! 
>> *) 
>>
>> As of today, I am pleased to announce that ATS3 has reached a stage 
>> where it can be realistically used in software construction. This is 
>> achieved after slightly more than two and one-half years of continual 
>> development by yours truly :) 
>>
>> ## 
>> # 
>> # The current status 
>> # 
>> ## 
>>
>> XATSOPT: 
>>
>> Xatsopt is a functioning compiler implemented in ATS2 for translating 
>> ATS3 into a typed intermediate language of the name XATSCML, which is 
>> both C-like and ML-like. It is planned for xatsopt to further 
>> translate XATSCML into XATSCL0, a low-level C-like language. I now 
>> primarily see xatsopt as a library (libxatsopt) for implementing tools 
>> to support programming with ATS3. 
>>
>> XATS2JS: 
>>
>> Xats2js is a functioning compiler implemented in ATS2 for translating 
>> XATSCML into JavaScript (or JS for short). It should be noted that 
>> xats2js can compile tail-recursive calls into local jumps, effectively 
>> supporting the common practice in functional programming of writing 
>> loops as tail-recursive functions. 
>>
>> I will give detailed explanation elsewhere on using xats2js. Generally 
>> speaking, one can now practice a form of co-programming with ATS3 and 
>> JS. The JS code generated by xats2js from compiling ATS3 source can be 
>> directly combined with other JS code (as if the generated code were 
>> manually written in JS) 
>>
>> ## 
>> # 
>> # Future Development 
>> # 
>> ## 
>>
>> Documenting Xatsopt: 
>>
>> This has been assigned a high priority. It is hoped that other 
>> people interested in ATS3 can start developing tools for ATS3 after 
>> a minimal amount of documentation on xatsopt is made available. 
>>
>> Advanced Type-Checking: 
>>
>> While one can specify with linear types and dependent types in ATS3, 
>> there is no type-checking for such advanced types in xatsopt. I plan 
>> to concentrate on implementing support for such type-checking in the 
>> next phase of ATS3 development. 
>>
>> ## 
>> # 
>> # A little history of ATS3 
>> # 
>> ## 
>>
>> Essentially, ATS3 refers to the third edition of ATS, and ATS/Xanadu 
>> is currently the only implementation of ATS3. Note that the names ATS3 
>> and ATS/Xanadu are often used interchangeably. 
>>
>> In the ATS family of languages, the first implementation is named 
>> ATS/Proto (2004) and the language it implements is referred to as 
>> ATS0. Please note that the implementation of ATS/Proto is written in 
>> OCaml. The next implementation is ATS/Geizella (2007), which is also 
>> written in OCaml. And the language implemented by ATS/Geizella is 
>> referred to as ATS1. ATS/Anairiats (2008) is an implementation of ATS1 
>> in itself; the implementation is first compiled by ATS/Geizella and 
>> then by itself, succeeding in so-called bootstrapping. The next 
>> edition of ATS is ATS2, which is given an implementation of the name 
>> ATS/Postiats (2013) written in ATS1. 
>>
>> ATS/Xanadu implements ATS3 and the implementation is written in ATS2. 
&

Re: Read IO and Write IO

[gmhwxi]

Thanks for the message!

What I said is not in conflict with what you described in the message.

An external tool for tracking effects can be quite useful in large scale 
programming.
Deciding what effects should be tracked is often open-ended; what is 
decided today
may not be what is wanted tomorrow.

The type-based approach you described becomes quite burdensome once 
higher-order
functions are present. A big difficulty in effect-tracking lies precisely 
in handling higher-order
functions.

On Monday, November 23, 2020 at 10:57:41 PM UTC-5 ice.r...@gmail.com wrote:

> Maintaining some external file seems to me as something, which is easy to 
> ignore or easy to forget about and without some scatch of of example of 
> usage, I can't see how it will be helpful at all.
>
> For example:
> ```
> fn foo(): void = println!("hello")
> implement main0() = foo()
> ```
> and the external file contains:
> ```
> console: println
> ```
> Do you mean, that such external tool should require foo and main0 to be 
> listed in such file?
> In this case, it will still be absent in types so it will be hard to 
> answer a questions like: "what effects contains foo?" or main0 as well.
>
> In contrast, by using proof arguments you will actually see, that in order 
> to use foo you need to pass IO:
> so it is clearer to understand, but more verbose as well, as main0 will be 
> probably a source of all kind of effects, like:
> ```
> extern prfn use_console( !IO): Console
> fn
>   foo
>   ( console: !Console
>   |
>   ): void = println!( console, "hello")
> implement main0(io | ) = {
>   prval console = use_console( io)
>   val () = foo( console | )
> }
> ```
>
> another interesting approach will be to wrap the exceptions (ie, the goal 
> is to see in types which exceptions are possible to be thrown from 
> function), so $raise should have type like:
> ```
> extern fn
>   $raise
>   {a:type}{b:type| // is there an exception sort?
>   ( !Throws(a)
>   | a
>   ): b
> ```
> then `try` should require `!IO` and bring `Throws(a)` for all branches in 
> `with`, like:
> ```
> fn
>foo
>   ( Throws( DivisionByZero)
>   , Throws(FileNotFound)
>   | a: int
>   , b :int
>   ): int = a / b
>
> implement main0() = 
> try 
>   ( try foo() with // I am not sure if foo() will be able to use 
> Throws(..) implicitely
>   | ~DivisionByZero() => ... // this brings Throws(DivisionByZero) into 
> the scope and only within this block of try ... with
>   ) with
>   | ~FileNotFound() => ... // this brings Throws(FileNotFound) into the 
> scope
> ```
> but of course, this looks like Haskell's typeclasses from 
> https://www.well-typed.com/blog/2015/07/checked-exceptions/
>

-- 
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/e90611de-5efc-46e2-8d45-61db522c73f1n%40googlegroups.com.

Re: Read IO and Write IO

[gmhwxi]

At this point, I would say that effect tracking is to be supported
by an external tool. Here is the basic design that has gradually formed
in my mind:

Say that you want to know whether a specific kind of effect (e.g, sending
email, drawing, locking/unlocking) is to be generated at run-time. You can
supply a file in which you list the names of the functions that can 
potentially
generate such effects; the tool takes the information given in the file to 
generate
a report. Of course, there are a lot of details and varieties :)

On Sunday, November 22, 2020 at 12:57:58 PM UTC-5 brandon...@gmail.com 
wrote:

> Good point! 
>
> Delayed reply, though the updated status on ATS3 lead me to revisit this 
> discussion.
>
> Is there a current (or planned update) on how pure function tracking can 
> be achieved? 
>
> Best,
>
> On Friday, August 9, 2019 at 9:34:32 PM UTC-4 gmhwxi wrote:
>
>>
>> >>So practically speaking, not much trouble, though it does leave room for
>> >>erroneous modeling of effects.
>>
>> Well, this is really unavoidable. 
>>
>> If you think about it, there is a even bigger issue. Say you call 
>> function 'foo'
>> in your code. How do you even know that 'foo' should be called in the 
>> first place?
>> Usually, it is all based on your understanding of 'foo'? How do you even 
>> know that
>> your understanding of 'foo' is correct? I think I should stop here :)
>>
>>
>>
>> On Fri, Aug 9, 2019 at 9:23 PM Brandon Barker  
>> wrote:
>>
>>> I like this. Also, this later discussion reminds me of ZIO in Scala.
>>> The trouble only really starts when you import the non-pure code and
>>> want to use it from pure code. In that case, you can either go with
>>> the default assumption it has all effects ("regular IO"), or annotate
>>> it as having specific effects, if you really know what is going on. So
>>> practically speaking, not much trouble, though it does leave room for
>>> erroneous modeling of effects.
>>>
>>> On Fri, Aug 9, 2019 at 9:17 PM Hongwei Xi  wrote:
>>> >
>>> > >>I can write my code without any IO?
>>> >
>>> > Yes, you should be able to program in the same way as you do now.
>>> >
>>> > --Hongwei
>>> >
>>> > On Fri, Aug 9, 2019 at 8:43 PM Kiwamu Okabe  
>>> wrote:
>>> >>
>>> >> Dear all,
>>> >>
>>> >> On Fri, Aug 9, 2019 at 8:53 PM gmhwxi  wrote:
>>> >> > If you don't want to track IO effects, then you don't really
>>> >> > feel the difference.
>>> >>
>>> >> Umm... There will be an option to write ATS3 code without any IO 
>>> effects.
>>> >>
>>> >> Example:
>>> >> If I create my own prelude library without IO effect,
>>> >> I can write my code without any IO?
>>> >>
>>> >> Best regards,
>>> >> --
>>> >> 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-user...@googlegroups.com.
>>> >> To view this discussion on the web visit 
>>> https://groups.google.com/d/msgid/ats-lang-users/CAEvX6d%3DJnwDYDzC4%3Dj--dcYqLh4AJYr2pqdtmBA2AioDqngH%3Dg%40mail.gmail.com
>>> .
>>> >
>>> > --
>>> > You received this message because you are subscribed to the Google 
>>> Groups "ats-lang-users" group.
>>> > To unsubscribe from this group and stop receiving emails from it, send 
>>> an email to ats-lang-user...@googlegroups.com.
>>> > To view this discussion on the web visit 
>>> https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrC5K7Zcya6tw-RV8DMFGjH0oaQW7PiSJrkE0QQfS5foA%40mail.gmail.com
>>> .
>>>
>>>
>>>
>>> -- 
>>> Brandon Barker
>>> brandon...@gmail.com
>>>
>>> -- 
>>> You received this message because you are subscribed to the Google 
>>> Groups "ats-lang-users" group.
>>> To unsubscribe from this group and stop receiving emails from it, send 
>>> an email to ats-lang-user...@googlegroups.com.
>>>
>> To view this discussion on the web visit 
>>> https://groups.google.com/d/msgid/ats-lang-users/CAORbNRr5PN7ye6u1FgfWGKRfynmEhQq3hn3_TY2h%2BLb%2BffXjgA%40mail.gmail.com
>>> .
>>>
>>

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/9edd4e6a-e25e-41cf-b031-0e3a80a05ff6n%40googlegroups.com.

Current Status of ATS3 (2020-11-22)

[gmhwxi]

Hi, there, 

HX-2020-11-22: 

(* 
HX-2018-04-07: Let us get started!!! 
*) 

As of today, I am pleased to announce that ATS3 has reached a stage 
where it can be realistically used in software construction. This is 
achieved after slightly more than two and one-half years of continual 
development by yours truly :) 

## 
# 
# The current status 
# 
## 

XATSOPT: 

Xatsopt is a functioning compiler implemented in ATS2 for translating 
ATS3 into a typed intermediate language of the name XATSCML, which is 
both C-like and ML-like. It is planned for xatsopt to further 
translate XATSCML into XATSCL0, a low-level C-like language. I now 
primarily see xatsopt as a library (libxatsopt) for implementing tools 
to support programming with ATS3. 

XATS2JS: 

Xats2js is a functioning compiler implemented in ATS2 for translating 
XATSCML into JavaScript (or JS for short). It should be noted that 
xats2js can compile tail-recursive calls into local jumps, effectively 
supporting the common practice in functional programming of writing 
loops as tail-recursive functions. 

I will give detailed explanation elsewhere on using xats2js. Generally 
speaking, one can now practice a form of co-programming with ATS3 and 
JS. The JS code generated by xats2js from compiling ATS3 source can be 
directly combined with other JS code (as if the generated code were 
manually written in JS) 

## 
# 
# Future Development 
# 
## 

Documenting Xatsopt: 

This has been assigned a high priority. It is hoped that other 
people interested in ATS3 can start developing tools for ATS3 after 
a minimal amount of documentation on xatsopt is made available. 

Advanced Type-Checking: 

While one can specify with linear types and dependent types in ATS3, 
there is no type-checking for such advanced types in xatsopt. I plan 
to concentrate on implementing support for such type-checking in the 
next phase of ATS3 development. 

## 
# 
# A little history of ATS3 
# 
## 

Essentially, ATS3 refers to the third edition of ATS, and ATS/Xanadu 
is currently the only implementation of ATS3. Note that the names ATS3 
and ATS/Xanadu are often used interchangeably. 

In the ATS family of languages, the first implementation is named 
ATS/Proto (2004) and the language it implements is referred to as 
ATS0. Please note that the implementation of ATS/Proto is written in 
OCaml. The next implementation is ATS/Geizella (2007), which is also 
written in OCaml. And the language implemented by ATS/Geizella is 
referred to as ATS1. ATS/Anairiats (2008) is an implementation of ATS1 
in itself; the implementation is first compiled by ATS/Geizella and 
then by itself, succeeding in so-called bootstrapping. The next 
edition of ATS is ATS2, which is given an implementation of the name 
ATS/Postiats (2013) written in ATS1. 

ATS/Xanadu implements ATS3 and the implementation is written in ATS2. 
While there is currently no plan to bootstrap ATS3 by implementing it 
in itself, it is perceivable that ATS/Xanadu can be readily translated 
(manually) into such an implementation since the difference between 
ATS2 and ATS3 in terms of both syntax and semantics is fairly minor 
(for the part being used in compiler implementation). 

## 

Cheers! 

--Hongwei 

## 

For previously post messages: 

https://github.com/githwxi/ATS-Xanadu/tree/master/docgen/NOTES 
##


-- 
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/3601c4d6-1c7c-4eb3-97fa-726b1ec60a72n%40googlegroups.com.

Re: The current status of ATS3

[gmhwxi]

That would be great!

When things are a bit more stable, I will announce again.

I expect that we will see more and more "meta-programming" support in ATS3,
which should make programming a lot more interesting and productive.

Cheers!

On Monday, November 2, 2020 at 11:44:11 AM UTC-5 d4v3y_5c0n3s wrote:

> Thanks for the update!  I've still got much to learn about ATS2, but ATS3 
> has got me very excited.  I'll check out the Github page, perhaps I could 
> help the project by doing some tests or the like.  Please post if you could 
> use some help on anything.
>
> On Sunday, November 1, 2020 at 9:42:19 AM UTC-5 gmhwxi wrote:
>
>> Hi,
>>
>> I would like to give you a quick report on the current status of ATS3.
>> I spent most of my time working on xatsopt and xats2js in the past two 
>> months.
>>
>> What is Xatsopt?
>>
>> Xatsopt is a compiler that translates source code in ATS3 into a target 
>> language
>> called the ATSCML that is both C-like and ML-like. The key steps in this 
>> translation
>> include type inference (of Hindley-style) and template resolution.
>>
>> What is Xats2js?
>>
>> Xats2js is a compiler that translates from ATSCML to JavaScript. 
>> Currently, xats2js
>> translates directly without performing optimizations. In particular, 
>> there is no optimization for handling tail-recursive calls. Xats2js is 
>> functioning and I myself am using it for some of my own work. Here is the 
>> github repo for xats2js:
>>
>> https://github.com/xanadu-lang/xats2js
>>
>> If you git-clone the repo, you can play with xats2js in the following 
>> directory:
>>
>> https://github.com/xanadu-lang/xats2js/tree/master/docgen/pground
>>
>> 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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/d48a5dba-382c-4cf1-ae45-f0df925fd715n%40googlegroups.com.

The current status of ATS3

[gmhwxi]

Hi,

I would like to give you a quick report on the current status of ATS3.
I spent most of my time working on xatsopt and xats2js in the past two 
months.

What is Xatsopt?

Xatsopt is a compiler that translates source code in ATS3 into a target 
language
called the ATSCML that is both C-like and ML-like. The key steps in this 
translation
include type inference (of Hindley-style) and template resolution.

What is Xats2js?

Xats2js is a compiler that translates from ATSCML to JavaScript. Currently, 
xats2js
translates directly without performing optimizations. In particular, there 
is no optimization for handling tail-recursive calls. Xats2js is 
functioning and I myself am using it for some of my own work. Here is the 
github repo for xats2js:

https://github.com/xanadu-lang/xats2js

If you git-clone the repo, you can play with xats2js in the following 
directory:

https://github.com/xanadu-lang/xats2js/tree/master/docgen/pground

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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/5e01d5b8-58fc-48b7-9311-4173592ce006n%40googlegroups.com.

Re: Current Status of ATS3

[gmhwxi]

>>As I guess, "someone" can try to work on ATS3-ML->C/C++ translator in 
parallel to xats2js at the point, when ATS3-ML should not have planned 
backward incompatibility changes.

Yes, this is the plan.

ATS3 is designed to be an "open" programming language platform. In 
particular,
the design of ATS3 should readily allow people to build such translators on 
their own.
For instance, xats2js is the first example of such. This is just like 
compiling C to all kinds
of assembly languages.

Cheers!

--Hongwei


On Saturday, October 17, 2020 at 10:54:53 PM UTC-4 ice.r...@gmail.com wrote:

> Thanks for the report. I think all of us can't  wait to try ATS3, 
> especially if it will improve user-experience in comparison to ATS2.
>
> As I guess, "someone" can try to work on ATS3-ML->C/C++ translator in 
> parallel to xats2js at the point, when ATS3-ML should not have planned 
> backward incompatibility changes.
>

-- 
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/61cd913a-90a6-45b8-baea-0f323a64bf6bn%40googlegroups.com.

Re: Current Status of ATS3

[gmhwxi]

>>Am I correct: ATS3-ML, being intermediate language, does not aware of 
dependent/linear types and 

That is correct. ATS3-ML is typed; its type system is ML-like. In 
particular, the types in ATS3-ML are algebraic
(that is, they are free of explicit quantifiers).

On Saturday, October 17, 2020 at 10:53:58 PM UTC-4 ice.r...@gmail.com wrote:

> Thanks for the report. I think all of us can't  wait to try ATS3, 
> especially if it will improve user-experience in comparison to ATS2.
>
> As I guess, "someone" can try to work on ATS3-ML->C/C++ translator in 
> parallel to xats2js at the point, when ATS3-ML should not have planned 
> backward incompatibility changes.
> Am I correct: ATS3-ML, being intermediate language, does not aware of 
> dependent/linear types and 
>
>

-- 
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/47c832cb-b63e-4bdc-9a00-ae3916d320ean%40googlegroups.com.

Re: Current Status of ATS3

[gmhwxi]

Yes, JS is the first working target.

The 'ML' in ATS3-ML is used in rather a loose sense.

By ML, I basically refer to a language that supports function closures and 
recursive datatypes/pattern matching.
This is a broad category. ATS3-ML should readily be able to be compiled to 
any ML-like languages that I can think of.

I may change the name ATS3-ML to ATS3-CML to reflect the fact that this 
language supports flat data representation
(in contrast to the boxed data representation used by ML-like languages).

Cheers!

On Saturday, October 17, 2020 at 5:52:57 PM UTC-4 brandon...@gmail.com 
wrote:

> Thanks for your continued efforts! That all sounds wonderful, just one 
> question for now: it sounds like ATS3-ML's first working target will be 
> Javascript. I wonder if ATS3-ML is similar enough to some existing ML to 
> support an ML target? Or maybe I misunderstood and the ML target can 
> already be executed standalone.
>
> On Tuesday, September 1, 2020 at 12:52:11 PM UTC-4 gmhwxi wrote:
>
>>
>> Hi, there,
>>
>> I would like to say a few words on the current status of ATS3.
>>
>> Originally, I planned to complete a compiler from ATS3 to C/C++ by
>> the end of Summer, 2020. On the way, my plan changed somewhat.
>> This is the current status of ATS3:
>>
>> 1. In the following repository, there is a compiler from ATS3 to an 
>> intermediate
>> language ATS3-ML (which is ML-like):
>>
>> https://github.com/githwxi/ATS-Xanadu
>>
>> This compiler is functioning. And it will be polished and improved 
>> gradually. This
>> is the core for all of the future development of ATS3. Essentially, the 
>> compiler first
>> does the so-called Hindley-style of type-inference, and then it performs 
>> template resolution.
>>
>> 2. In the following repository, there is a running interpreter for 
>> testing the aforementioned
>> compiler:
>>
>> https://github.com/xanadu-lang/xinterp
>>
>> This interpreter is not meant for practical use; it is mainly for testing 
>> and documenting
>> the syntax of ATS3.
>>
>> 3. I am working on a compiler from ATS3-ML to JS:
>>
>> https://github.com/xanadu-lang/xats2js
>>
>> This compiler is meant for practical use. For instance, I plan to use it 
>> for building a website for ATS3. Hopefully, this compiler will be 
>> functioning in a couple of months.
>>
>> After xats2js, I will be working on dependent and linear type-checking 
>> for ATS3 and then
>> a compiler from ATS-ML to C/C++. Will keep everyone informed.
>>
>> 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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/0e54d77d-52bd-41fe-b5c6-5d0ca6b74d74n%40googlegroups.com.

Re: How to avoid to return uninitialized value on ATS2?

[gmhwxi]

>>what does the `?` syntax stand for? 

Given a viewt@ype VT, VT? (? is a postfix operator here)  is a t@ype such 
that
sizeof(VT) = sizeof(VT?).

? : viewt@ype -> t@ype // this is the sort assigned to '?'

Note that VT? is completely opaque; the only information on VT? is its size.

On Friday, September 18, 2020 at 4:50:35 AM UTC-4 artyom.s...@gmail.com 
wrote:

> пт, 18 сент. 2020 г. в 02:00, Kiwamu Okabe :
>
>> Dear Hongwei,
>>
>> On Thu, Sep 17, 2020 at 9:51 PM Hongwei Xi  wrote:
>> > >>BTW. Can we create a polymorphic `sbuf_bcat` function to avoid
>> > >>returning uninitialized value?
>> >
>> > You can do something like:
>> >
>> >absprop INITIALIZED(a:vt@ype)
>> >
>> >fun
>> >sbuf_bcat
>> >{a:vt@ype}{l:addr}
>> >(pf0: INITIALIZED(a), pf1: !a @ l | p: ptr l): void = undefined()
>>
>> Oh, `absprop`. But...
>>
>> > The problem with this approach is that the user of sbuf_bcat is 
>> burdened with
>> > the need for explicitly constructing a proof to show that 'a' is 
>> initialized.
>>
>> I can't understand this clearly.
>> Should I introduce `INITIALIZED(a)` with some proof function as the user?
>>
>
> Hongwei, what does the `?` syntax stand for? Is it a type constructor? Is 
> it something of the sort vt0ype -> t0ype, so that, together with the 
> axiom(?) that any type is a viewtype with an empty view part, gives us this 
> behavior? Are there any special rules to it?
>
>
>> Best regards,
>> -- 
>> 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-user...@googlegroups.com.
>>
> To view this discussion on the web visit 
>> https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dmvx%3Dj%2B1cGF7%2BOSbUNXUiOuNkTvzb20MbvFDtozRynJRA%40mail.gmail.com
>> .
>>
>
>
> -- 
> Cheers,
> Artyom Shalkhakov
>

-- 
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/680641d2-71d0-4bb1-95d3-63f7b2d91ce8n%40googlegroups.com.

Re: How to assign a `shared` value onto a member of vtype?

[gmhwxi]

You could also do it by using a type-annotation:

implement main0 () = let
var opts: ip6_pktopts
var inp: inpcb
val () = inp.in6p_outputopts := addr@opts
val () = inp.sh := shared_make(view@opts | addr@opts)
val (pf_oopts | x, count) = shared_unref(inp.sh)
val () = assertloc(count <= 1)
prval Some_v(pf_opts) = pf_oopts
val () = assertloc(x = addr@opts)
prval () = view@opts := (pf_opts: (ip6_pktopts?)@opts)
  in
ignoret(usleep(1000u))
  end

When a proof is assigned to view@opts, the proof is required to be of the 
view T@opts.
Without the annotation, the proof is of the view T@l for some l. Yes, opts 
and l are equal
but the type-checker requires that opts and l are *syntactically identical* 
in this case.
On Sunday, August 30, 2020 at 1:10:04 AM UTC-4 ice.r...@gmail.com wrote:

> 1. the reason why we need to prove, that x = addr@opts is that 
> shared_unref's type says, that it's return type defines *some* 'l':
> ```
> extern fun shared_unref{a:vt@ype} (shared(a)): *[l:addr]*[c:int] 
> (option_v(a@l, c <= 1) | ptr l, int c)
> ```
> this *l* can be the same as addr@opts, but can be some other, so we need 
> to check;
> 2. For now I can only guess why version with view@ didn't work (maybe 
> Hongwei will tell us the actual reason, especially if this is a bug or a 
> feature), but I think it is related to how both views are behave:
>
> when we consume view@opts in make_shared, view@opts is still available at 
> 'main' and we can show it's type with '$showtype', which tells us, that now 
> it is ' without(ip6_pktopt) @ opts'
>
> ```
> **SHOWTYPE[UP]**(/data/devel/ats2/closure/main.dats: 2970(line=109, 
> offs=26) -- 2979(line=109, offs=35)): S2Eat(S2Ewithout(S2Etyrec(flt0; 
> npf=-1; ip6po_hlim=S2Etop(knd=0; S2Ecst(int; S2Evar(opts(8624))): 
> S2RTbas(S2RTBASimp(7; view))
> ```
>
> but if we will use view alias like this:
>
> ```
> implement main0 () = let
> var opts: ip6_pktopts with opts_pf
> var inp: inpcb
> val () = inp.in6p_outputopts := addr@opts
> prval _ = $showtype (opts_pf)
>
> val () = inp.sh := shared_make(opts_pf | addr@opts)
> val (pf_oopts | x, count) = shared_unref(inp.sh)
> val () = assertloc(count <= 1)
> prval Some_v(pf_opts) = pf_oopts
> val () = assertloc( x = addr@opts)
> (*prval _ = $showtype (opts_pf) can't use it here, because opts_pf is 
> no longer available, as it was consumed *)
> prval () = opts_pf := pf_opts (* restore opts_pf *)
> prval _ = $showtype (opts_pf)
>   in
> ignoret(usleep(1000u))
>   end
> ```
> it will show types:
> ```
> **SHOWTYPE[UP]**(/data/devel/ats2/closure/main.dats: 2733(line=103, 
> offs=26) -- 2740(line=103, offs=33)): S2Eat(S2Etyrec(flt0; npf=-1; 
> ip6po_hlim=S2Etop(knd=0; S2Ecst(int))); S2Evar(opts(8624))): 
> S2RTbas(S2RTBASimp(7; view))
> **SHOWTYPE[UP]**(/data/devel/ats2/closure/main.dats: 3021(line=110, 
> offs=26) -- 3028(line=110, offs=33)): S2Eat(S2EVar(5372); 
> S2Evar(l$8793$8795(14582))): S2RTbas(S2RTBASimp(7; view))
> ```
> meaning, that we no longer have a prove of 'ip6_pktopt @ opts', but we 
> have a prove of 'ip6_pktopt @ l', where *l* is some address, even though 
> we have an assertloc(), that should confirn, that 'l = addr@opts'.
> It may be, that for compiler 'opts' is not a pointer, but a variable and 
> that is why we can't prove that l = opts, but in case of using view alias, 
> compiler thinks 'ok, prove with '@opts' has gone now and we got new proof 
> with some 'l', it's type 'a' is the same as type of 'opts', so it is the 
> same size and I can replace consumed view with that one'.
> But as I said, this is only a guess
>

-- 
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/746814d3-a29a-404a-80e7-08a8e40140d6n%40googlegroups.com.

Be Forgetful!

[gmhwxi]

Kiwamu cited the following security issue in his earlier message

>>Dear all, 

>>There is a security issue on FreeBSD: 

* Security Advisory: 
https://www.freebsd.org/security/advisories/FreeBSD-SA-20:20.ipv6.asc 
* The patch: 
https://github.com/freebsd/freebsd/commit/5707de0ed806712f53752acd433313a39f63f15c

Basically, someone wrote the following line:

error = ip6_pcbopts(>in6p_outputopts,  m, so, sopt); 

The code should have been written as follows:

INP_WLOCK(inp); 
error = ip6_pcbopts(>in6p_outputopts, m,  so, sopt);
INP_WUNLOCK(inp);

In other words, the spin lock attached to 'inp' needs to be grabbed first
to avoid a potential race condition.

Of course, this kind of bug can be readily detected if ip6_pcbopts is 
required
to take a proof argument (to show that the aforementioned spin lock is 
grabbed):

error = ip6_pcbopts(pf | >in6p_outputopts, m,  so, sopt);

If you want to make sure that the grabbed lock is indeed the right one
for protecting 'inp', the type assigned to ip6_pcbopts is actually quite 
involved.
What I would like to say here is that you should probably *try to be 
forgetful*:

https://en.wikipedia.org/wiki/Forgetful_functor

A forgetful functor is a concept in category theory. It is really just a 
fancy word
to describe an act of ignoring details. For the ip6_pcbopts example, we 
know that
a proof of some sort is needed. And we don't have to get into details at 
this point:

pf = INP_WLOCK(inp); 
error = ip6_pcbopts(pf | >in6p_outputopts, m,  so, sopt);
INP_WUNLOCK(pf | inp);

We can introduce a (non-dependent) abstract view for the proof returned 
from calling INP_WLOCK. It is essential to keep it simple so that this 
approach can actually scale.

My very simple point is that

1) There are a lot of bugs out there
2) You rarely need the full rigor of ATS to uncover many of them

*Trying to be* *forgetful* can actually be a very successful strategy for 
handling
large code bases.

--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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/58f81db1-2d98-4779-8c37-fd8a8195e2bfn%40googlegroups.com.

Re: How to assign a `shared` value onto a member of vtype?

[gmhwxi]

shared(a) should be changed to shared(a, l) if you need to make sure that 
the returned
proof is also of the view a@l (instead of a@l2 for some l2). Otherwise, you 
may have to
do a bit of casting:

extern
prfun
vborrow
{a:view}(pf: !INV(a)): a

implement main0 () = let
var opts: ip6_pktopts
var inp: inpcb
prval pf = vborrow(view@opts)
val () = inp.in6p_outputopts := addr@opts
val () = inp.sh := shared_make(pf | addr@opts)
val (pf_oopts | x, count) = shared_unref(inp.sh)
val () = assertloc(count <= 1)
prval Some_v(pf_opts) = pf_oopts
prval () = $UN.castview0{void}(pf_opts)
  in
ignoret(usleep(1000u))
  end

On Saturday, August 29, 2020 at 9:26:38 PM UTC-4 Kiwamu Okabe wrote:

> Dear Hongwei,
>
> On Sun, Aug 30, 2020 at 10:19 AM Hongwei Xi  wrote:
> > Well, you did not prove that the one returned is the same as the one 
> borrowed :)
>
> Umm... Do you mean following eats original `a@l`:
>
> ```ats
> extern fun shared_make{a:vt@ype}{l:addr} (a@l | ptr l): shared(a)
> ```
>
> and the following introduces another one?
>
> ```ats
> extern fun shared_unref{a:vt@ype} (shared(a)): [l:addr][c:int]
> (option_v(a@l, c <= 1) | ptr l, int c)
> ```
>
> I would like to take more hints.
> If I prove they have same `l:addr` in `shared(a:vt@ype)`, ATS2 accepts
> them as the same?
>
> ```ats
> absvtype shared(a:vt@ype) = [l:addr] (a@l | ptr l)
> ```
>
> Best regards,
> -- 
> 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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/a6f5a77c-ea89-43d6-a7b0-4545b1d88c6en%40googlegroups.com.

Re: ATS and OOP

[gmhwxi]

The support for OOP in ATS2 was largely an experiment. There isn't really 
any
meaningful documentation for it.

OOP is not planned be a part of ATS3. But I suppose it can be supported in 
an extension.
Here is something I outlined quite a while ago:

http://www.cs.bu.edu/~hwxi/academic/papers/asia-pepm02.pdf

On Saturday, August 29, 2020 at 2:29:35 AM UTC-4 ice.r...@gmail.com wrote:

> Hi,
> I see, that ATS2 has support of OOP (in particular, as I see in GTK from 
> contrib package).
> Is OOP planned to be supported by ATS3?
>
> Is there any documentation about how to use OOP in ATS2 other than source 
> code?
>

-- 
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/4ef8d2ae-e30b-4150-a62b-f6e824276362n%40googlegroups.com.

MITRE shares this year's top 25 most dangerous software bugs

[gmhwxi]

FYI.

MITRE shares this year's top 25 most dangerous software bugs:

https://www.bleepingcomputer.com/news/security/mitre-shares-this-years-top-25-most-dangerous-software-bugs/

--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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/758e59b3-0bfa-4dfa-bb6a-1822eb14c79fn%40googlegroups.com.

Re: A small query about closures

[gmhwxi]

A linear closure (lincloptr1) is a linear value; like any other linear 
values,
it needs to be used (that is, called) once and only once.

A closure is a pair (f, env); where 'f' is a function pointer, which is 
non-linear,
and env is a record. If env contains a linear value, then the closure (f, 
env) is
linear. If you want to have a "linear" function that can be called multiple 
times,
you should try (in ATS2) to create a linear stream; evaluating the stream 
once
amounts to calling the function once.

It is possible that we support other forms of linear functions in ATS3. In 
any case,
I feel that this would just be a niche feature; its implementation tends to 
be involved
but its usefulness is rather limited.

--Hongwei

PS: For instance, the 'move' trick in Rust can be readily implemented in 
ATS2. But
doing it also complicates type-checking in a non-trivial way.

On Tuesday, August 18, 2020 at 3:53:51 PM UTC-4, Dambaev Alexander wrote:
>
> In fact, I had some issues to express the same thing in ATS2. The closest 
> sample (in case if Rust does stack allocation of the clone of the line in 
> closure) is:
> ```
> staload UN="prelude/SATS/unsafe.sats"
>
> extern prval hack{l:addr} ( pf: int @ l): void
>
> fn
>   linum
>   {l:addr}
>   (
>   ):
>   ( (int0 @ l)
>   | ( !(int0 @ l)
> | ()
> ) -
> void
>   ) = (pf | f) where {
>   var original:int0 with pf= 0 (* pf is a linear variable here *)
>   fn
> f
> ( pf: !(int0 @ original)
> | ()
> ):
> void = {
>   val () = original := original + 1
>   val () = println!("line = ", original)
> }
> }
>
> implement main0() = {
>   val (pf | f) = linum( )
>   val ( ) = f( pf | () )
>   val ( ) = f( pf | () )
>   prval () = hack( pf) (* tell type system, that pf had been consumed *)
>   val () = cloptr_free( $UN.castvwtp0(f))
> }
> ```
> But this will not compile, obviously, because *original* will be removed 
> at linum's exit.
>
> The compilable example uses heap to clone *original* value, which should 
> be freed explicitly. I am not sure if it follows the same semantic as Rust 
> sample (I guess, only valgrind/disassembler should give an answer if rust 
> uses heap for this as well) 
>
> ```
> staload UN="prelude/SATS/unsafe.sats"
>
> extern prval hack{l:addr} ( pf: int @ l): void
>
> fn
>   linum
>   (
>   ):
>   [l:addr]
>   ( mfree_gc_v l
>   | ptr l
>   , ( 
> ) -
> ( (int @ l)
> | (**)
> )
>   ) = ( free_pf | p, f) where {
>   var original:int = 0
>   val (pf, free_pf | p) = ptr_alloc_tsz(sizeof)
>   val () = !p := original (* clone value *)
>   val f = llam () = ( pf1 | (**)) where {
>   prval pf1 = pf
>   val () = !p := g0int_add_int( !p, 1) (* !p + 1 confuses a template 
> selector for some reason *)
>   val () = println!("line = ", !p)
> }
> }
>
> implement main0() = {
>   val ( free_pf | p, f) = linum( )
>   val ( pf | (**) ) = f( )
>   (* 
> *prval () = hack( pf) (* have to consume pf *)  val ( pf | (**) ) = f( )* 
> *)
>   val () = ptr_free( free_pf, pf | p)
>   val () = cloptr_free( $UN.castvwtp0(f))
> }
>
> ```
>
> the bold part had been commented out, because ATS does not allow to call 
> linear closure multiple times, so uncommenting leads to a compilation error.
> But I am not an experienced user of ATS, so I might not know some tricks 
> to either to reuse a linear closure, to capture linear variables in 
> non-linear closures or to return a new linear closure from the f ( but I 
> was not able to express the type of such function, and it seems, that the 
> example with lazy stream/stream_vt does similar thing)
>
>

-- 
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/213286ae-d06a-4230-ba71-b2cfe1207194o%40googlegroups.com.

Re: some resources recommendations for dependent types and possibly linear types?

[gmhwxi]

I don't feel that you need much of a theoretical background.

If you do want to dive into the theory behind ATS, here are a list of 
relevant papers:

http://www.ats-lang.org/Papers.html

On Monday, August 17, 2020 at 12:34:06 AM UTC-4, Timmy Jose wrote:
>
>
> Hello,
>
> I've been working through the first ATS tutorial (An introduction to 
> programming in ATS), and have finished books 1 & 2. I just started book 3 
> (dependent types), and the going has become a bit slow (not too much, but 
> sufficiently slow). 
>
> I realise that I lack the theoretical background needed for quite a few 
> topics that follow. I was just wondering if someone could recommend 
> approachable resources to supplement my learning for this part? 
>
> Thanks!
>
> Timmy
>

-- 
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/d7abc806-689c-490c-b3c6-f52d9ac480e1o%40googlegroups.com.

Re: some resources recommendations for dependent types and possibly linear types?

[gmhwxi]

Yes. There are quite a number of such functions in ATS2, which are no 
longer needed in ATS3.

On Monday, August 17, 2020 at 1:22:58 AM UTC-4, Timmy Jose wrote:
>
> Also, another related question . I deduce that `g0int2uint_int_size` is 
> the non-dependently-typed version whereas `g1int2uint_int_size1 is the 
> dependently-typed version. Is this assumption correct?
>
> Thanks!
>
> Timmy
>
> On Monday, August 17, 2020 at 10:04:06 AM UTC+5:30 Timmy Jose wrote:
>
>>
>> Hello,
>>
>> I've been working through the first ATS tutorial (An introduction to 
>> programming in ATS), and have finished books 1 & 2. I just started book 3 
>> (dependent types), and the going has become a bit slow (not too much, but 
>> sufficiently slow). 
>>
>> I realise that I lack the theoretical background needed for quite a few 
>> topics that follow. I was just wondering if someone could recommend 
>> approachable resources to supplement my learning for this part? 
>>
>> Thanks!
>>
>> Timmy
>>
>

-- 
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/cb055e04-dbdf-485b-ae62-c39029629d4co%40googlegroups.com.

Re: A small query about closures

[gmhwxi]

BTW, I don't quite understand what the Rust program does in terms of
memory management.

If you want a memory-clean implementation ATS, then you can do it as 
follows:

#include
"share/atspre_staload.hats"

fun
{a:t@ype}
stream_vt_uncons
(xs: _vt(a)): a =
let
val-
~stream_vt_cons(x0, tl) = !xs in (xs := tl; x0)
end

fun
linum
(line: int): stream_vt(int) =
$ldelay
let
val
line = line + 1
val () =
println!
("Current line number = ", line)
in
  stream_vt_cons(0, linum(line))
end

implement
main0() =
{
var f0 = linum(0)
val _1 = stream_vt_uncons(f0)
val _2 = stream_vt_uncons(f0)
val () = ~f0
var f0 = linum(0)
val _1 = stream_vt_uncons(f0)
val _2 = stream_vt_uncons(f0)
val () = ~f0
}

Valgrind confirms the memory-cleanness of the implementation:

==30566== Memcheck, a memory error detector
==30566== Copyright (C) 2002-2015, and GNU GPL'd, by Julian Seward et al.
==30566== Using Valgrind-3.11.0 and LibVEX; rerun with -h for copyright info
==30566== Command: ./abcde_dats
==30566==
Current line number = 1
Current line number = 2
Current line number = 1
Current line number = 2
==30566==
==30566== HEAP SUMMARY:
==30566== in use at exit: 0 bytes in 0 blocks
==30566==   total heap usage: 11 allocs, 11 frees, 1,184 bytes allocated
==30566==
==30566== All heap blocks were freed -- no leaks are possible
==30566==
==30566== For counts of detected and suppressed errors, rerun with: -v
==30566== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 0 from 0)


On Tuesday, August 11, 2020 at 10:29:38 AM UTC-4, gmhwxi wrote:
>
> The following header:
>
> fn 
> linum (): void - void =  
>
> should be changed to
>
> fn 
> linum (): () - void =
>
> But this does not give what you expected.
>
> You could use a reference:
>
> fn
> linum (): () - void=
> let
> val
> line = ref(0)
> in
> lam () =>
> let
> val () = !line := !line + 1
> in
> println! ("Current line number = ", !line);
> end
> end
>
> implement
> main0() =
> {
> val f0 = linum()
> val () = f0()
> val () = f0()
> val f1 = linum()
> val () = f1()
> val () = f1()
> }
>
>
> On Tue, Aug 11, 2020 at 10:10 AM Timmy Jose <...> wrote:
>
>> Hello,
>>
>> I have a small closure implementation in Rust which looks like so:
>>
>> fn linum() -> impl FnMut() {
>> let mut line = 0;
>>
>> Box::new(move || {
>> line = line + 1;
>> println!("Current line number is {}", line);
>> })
>> }
>>
>> fn main() {
>> let mut l = linum();
>> for _ in 0..5 {
>> l();
>> }
>>
>> l = linum();
>> for _ in 0..5 {
>> l();
>> }
>> }
>>
>> Basically, I simply want to capture the line variable in my closure. 
>> Running it:
>>
>> $ rustc linum.rs && ./linum
>> Current line number is 1
>> Current line number is 2
>> Current line number is 3
>> Current line number is 4
>> Current line number is 5
>> Current line number is 1
>> Current line number is 2
>> Current line number is 3
>> Current line number is 4
>> Current line number is 5
>>
>> as expected. Now, I was trying to replicate this behaviour in ATS (please 
>> note that I am totally new to ATS) using the chapter on functions, and this 
>> was my attempt:
>>
>> fn 
>> linum (): void - void= 
>>   let val line = 0 
>>   in
>>lam () => 
>>   let val line = line + 1 
>>   in
>>println! ("Current line number = ", line);
>>   end
>>   end
>>
>> which gives the following errors:
>>
>> $ make
>> acc pc -DATS_MEMALLOC_LIBC -O3 -o closures closures.dats
>>
>> /Users/z0ltan/dev/study/ats/introduction_to_programming_in_ats/revision/chapter3/closures.dats:
>>  
>> 12:4-16:10
>>
>>error(3): dynamic arity mismatch: more arguments are expected.
>>
>> patsopt(TRANS3): there are [1] errors in total.
>>   exit(ATS): (1025)
>> make: *** [closures] Error 1
>>
>> Can someone help me understand what the problem is? I'm pretty sure my 
>> knowledge of ATS is not enough right now to maybe fully implement this the 
>> way I want it, but I would like some pointers on this error message and 
>> maybe a nudge in the right direction to be able to implement this! 
>>
>> Thanks!
>>
>> Best Regards,
>>
>> Timmy
>>
>> (P.S: I hope it's all right if I keep posting questions every so often? I 
>> tried the IRC channel, but it appears to be inactive. Please let me know 
>> otherwise, in wh

Re: arrays' set_at/get_at functions and viewtypes

[gmhwxi]

You can also use array_v_split and array_v_unsplit to safely get/set linear
elements in an array.

On Saturday, August 1, 2020 at 11:01:56 AM UTC-4, Dambaev Alexander wrote:
>
> Hi,
>
> array and arrayptr have constraint {a:vt0p} for most of functions, except 
> array_set_at / arrayptr_set_at/array_get_at/arrayptr_get_at, which have 
> constraint {a:t0ype}
>
> So we can enumerate elements as viewtypes with foreach family of 
> functions, but the only way to set/get them is to use ptr_set/ptr_get, 
> right?
>
> Is it expected?
>

-- 
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/52b0cfd9-7248-410a-af95-693a6c7ec652o%40googlegroups.com.

Re: A look at D templates

[gmhwxi]

I took a quick look.

Templates in D are similar to templates in C++. Such templates are macros 
of some kind 
primarily for the purpose of syntactic manipulation.

Templates in ATS are more than macros. To some extent, they are like 
methods in OOP:
one method in a class can be given different implementations in the 
subclasses of the class.
Also, the way template resolution is done in ATS at compile-time is similar 
to the way method
dispatching is done in OOP at run-time. In this regard, templates in ATS 
are quite similar to type
classes in Haskell.

On Friday, July 31, 2020 at 12:13:19 PM UTC-4, Artyom Shalkhakov wrote:
>
> Hello all,
>
> I have come across this article:
>
> https://dlang.org/blog/2020/07/31/the-abcs-of-templates-in-d/
>
> This makes me wonder how D templates can be compared to ATS templates?
>

-- 
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/1edf41ec-1b5e-4240-a449-9a51345e5f58o%40googlegroups.com.

Re: ATS Linux - A Feedback

[gmhwxi]

Hi Matthias,

Today I took a glance at your ats-linux project. Here are a few thoughts
that I would like to share.

1. Please do not use the current library of ATS2. Instead, you should build
a library of your own specifically for this project. Of course, you could 
use ATS2
library at the beginning and then gradually replace the ATS library code 
with your
own.

2. Please try to avoid using dependent types at the beginning. I would not 
until
after I have got a running system. Think of dependent types as a way for 
you to
do (static) debugging later.

3. Try to use abstract types a lot! Here is some code I wrote to show off 
the idea:

https://github.com/xanadu-lang/xinterp/blob/master/srcgen/TEST/xatslib_githwxi/test-2020-07-26.dats

For instance, argv is just an array of strings. But you can make it 
abstract. If you really need to make use
of the fact that argv is an array of strings, you could just do a cast. 
Yes, this is unsafe but can be fixed later
without much effort at all.

4. Try to use templates a lot! Probably you could study the code in 
ATS-Temptory (but don't use ATS-Temptory
for your project as it is a quick experiment done and over at this point).

Good luck!

--Hongwei

PS: Don't feel that I have time to contribute to your project at this 
moment. But I will be happy to make suggestions
on translating C code into ATS. 


On Wednesday, July 1, 2020 at 9:29:58 PM UTC-4, matthias wrote:
>
> Hi,
>
> After half a year of experiencing ats (as a c++ developer) I changed my 
> point of view in how  to go forward in using ats. Comparing ats with other 
> "modern" languages is not very satisfying. Always having a position in the 
> middle - for the logical prove oriented people we have linear logic 
> (finally get control over resources, while the garbage collector solved 
> before such problems), for the machine programming oriented people linear 
> logic is like c-programming (nothing new, while garbage collection or 
> intelligent resource management may also solve serious problems) - is 
> difficult. Personally I Iike to have both - I can compare - cool. To come 
> to a point. I learned very much from this list and from the very good 
> documentation of the ats language. I started to change the linux kernel as 
> a private self teaching project. Looking from the viewpoint of a 
> c-programmer in direction to ats or alternatively to c++ is for me of 
> interest, For that, a minimal linux system of about 630 objects consists 
> now on 595 ats-dats files, may help to understand more. Sure, I haven't 
> migrated 595 c-files to real ats code. The integration is a first step 
> using the %{...%} pattern. The real migration must be done, one after the 
> other, by hand. It's a kind of training. If someone else has a personal 
> interest on linux kernel coding take my approach from git.bejocama.org. 
> It's totally open. Finally Thanks.
>
> Regards Matthias
>
>

-- 
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/23923286-cf2a-4a8f-96b5-be5396840b13o%40googlegroups.com.

Re: datavtypes

[gmhwxi]

>>Do you mean that you are working on such stuff? Or do you mean, that the 
progress of recvfrom() implementation is following a route to implement a 
custom allocator? :) In this case, I will delay it a bit, as my current 
project has time boundaries.

It is just a general comment :)

I did use the Arduino platform for experimenting linear functional 
programming
in an embedded setting. It was just a proof-of-concept as I did not have 
enough
time to pursue this idea further.

If you look at a typical embedded program, functions do not perform dynamic
allocations. Most likely, the memory needed during the execution of such a 
program
is all statically allocated (e.g., by declaring some top-level arrays). 
This simply means
that we can implement a memory allocator (e.g., one based on the buddy 
algorithm)
to manage the statically allocated memory and use it for linear functional 
programming.

In short, with a memory allocator for managing a chunk of statically 
allocated memory,
we should be able to effectively apply linear functional programing to the 
construction of
embedded programs.

On Sunday, July 12, 2020 at 2:20:48 PM UTC-4, Dambaev Alexander wrote:
>
> вс, 12 июл. 2020 г. в 15:50, gmhwxi <...>:
>
>> Am really pleased that you figured it out :)
>>
>
> It was pleasure for me as well :D
>
> The first time, when I started to think about it, was when I saw that 
> array_v_split has no parameters and I asked myself "how does it know on 
> which parts it should be splitted". Then I saw an article 
> https://bluishcoder.co.nz/2010/06/02/safer-c-code-using-ats.html when I 
> was searching more info about #[] syntax of return type and I was like 
> "wow".
>
>
>> This is pure C-style of systems programming. While it can be done in ATS,
>> it is often quite involved. The recvfrom function you implemented 
>> actually shows
>> that it does not make use of more resources that what is given.
>>
>
> yes, usually C-functions should not allocate memory themselves. Otherwise, 
> where all those custom allocators will be used? :)
> And to be serious: during the time, that I had spent with haskell and 
> ocaml, I came to conclusion, that one of big issues in haskell, is 
> interfacing with C/C++
> to have recvfrom (as an example), you will have those options:
> 1. define it yourself with something like
> ```
> foreign import "socket.h" c_recvfrom :: CInt-> Ptr a-> CLong-> CInt-> Ptr 
> b-> Ptr c-> IO CInt
> recvfrom:: Fd-> IO (SockAddr, ByteString)
> recvfrom fd =
>   alloca $ \src_sz ->  do
> pending_bytes <- ioctl fd FIONREAD
> buf <- mallocBytes pending_bytes
> src_addr <- malloc
> poke src_sz (sizeOf (undefined::SockAddr))
> ret <- c_recvfrom fd buf pending_bytes src_addr src_sz
> if ret >= 0
> then (peek src_addr, packCStringLen buf pending_bytes)
> else throwIO $ userError "recvfrom failed"
> ```
> seems not difficult, unless you need to define an instance of Storable for 
> SockAddr, for which you should know memory layout of SockAddr, including 
> size, alignment and so on. Fast way, but mastering your own wrapper for GTK 
> or QT is not a good idea.
> 2. use third-party library, which has all the dirty stuff, but it will add 
> dependencies, which will affect build times, binary size, can grow occupied 
> space due to cross dependencies and it will be pain when you need to cross 
> compile, but, hopefully, it will contain everything you ever need
> 3. master things like c2hs
>
> I was thinking, that I am struggling with haskell's FFI, until I had to 
> use OCaml's FFI like this:
>
> ```
> external recvfrom: int-> (sockaddr_t, bytes) = "c_recvfrom"
>
> //caml_stub.c
>
> value c_recvfrom(value _fd){
>   CAMLparams1(_fd);
>   CAMLlocal2(buf, tuple. sa);
>   int ret = 0;
>   int fd = 0;
>   int buf_sz = 0;
>   sockaddr_in src_addr;
>   size_t sa_sz = sizeof( src_addr);
>   fd = Int_val( _fd);
>   ioctl(fd, FIONREAD, _sz);
>   buf = malloc( buf_sz);
>   ret = recvfrom( Int_val(fd), buf, buf_sz, 0, _addr, _sz);
>   buf = caml_copy_string( buf, buf_sz);
>   sa = caml_alloc_custom( _pointers, sizeof(void*), 0, 1);
>   tuple = caml_alloc(1, 0);
>Store_field( tuple, 0, sa);
>   Store_field( tuple, 1, buf);
>   CAMLreturn(tuple);
> }
> ```
>
> so OCaml's FFI is basically untyped C, in which you have to operate with 
> variables of type 'value' and bunch of macroses and hope that you haven't 
> messed up anything.
> In this regard, ATS's way of interfacing is like a breath of fresh air for 
> me :)
>  
>
>>
>> One possibility is to introduce a linear functional API for recvfrom:
&g

Re: datavtypes

[gmhwxi]

Am really pleased that you figured it out :)

This is pure C-style of systems programming. While it can be done in ATS,
it is often quite involved. The recvfrom function you implemented actually 
shows
that it does not make use of more resources that what is given.

One possibility is to introduce a linear functional API for recvfrom:

absvtype sockaddr

datavtype
recvfrom_vt =
|
recvfrom_fail of ()
|
recvfrom_succ of
{m:nat} (arrpsz(char, m), sockaddr)

fun
ATS_recvfrom
{n:pos}
(sz: size_t(n), flags: int): recvfrom_vt

ATS_recvfrom calls malloc to obtain memory. However, we can differentiate
various malloc calls. For embedded programming, we can implement a malloc
that only allocates from statically allocated memory.

Basically, what I am saying here is that low-level systems programming can 
be
done in a linear functional style with customized implementations of 
malloc/free.
I feel that we are getting very close to this vision :)

On Sunday, July 12, 2020 at 3:07:16 AM UTC-4, Dambaev Alexander wrote:
>
> And at the end, it turned out, that I am not required to manually write 
> those proofs:
>
> ```
> extern
> fn recvfrom
>   {l: agz} {n: pos}{addr_sz:pos}
>   ( buf_pf: !array_v(char?, l, n) >> recvfrom_v(l,n,m)
>   | socket_fd: int
>   , buf: ptr l
>   , sz: size_t n
>   , flags: int
>   , src_addr: _struct(addr_sz)? >> opt(sockaddr_struct(addr_sz), 
> m > 0 && m <= n) (* technically, recvfrom expects sockaddr, not sockaddr_in 
> here *)
>   , addr_sz: &(socklen_t addr_sz)
>   ): #[m:int | m <= n] ssize_t(m)
> implement recvfrom{l}{n}(buf_pf | socket_fd, buf, sz, flags, src_addr, 
> addr_sz) = c_recvfrom( buf_pf| socket_fd, buf, sz, flags, src_addr, 
> addr_sz) where {
>   (* have to define another wrapper here, as only inside this call 
> src_addr has type sockaddr_struct, not 'incompatible' sockaddr_in like in 
> caller and produces compiler warning *)
>   extern
>   fn c_recvfrom
> {l: agz} {n: pos}{addr_sz:pos}{sa_l:addr}
> ( buf_pf: !array_v(char?, l, n) >> recvfrom_v(l,n,m)
> | socket_fd: int
> , buf: ptr l
> , sz: size_t n
> , flags: int
> , src_addr: _struct(addr_sz)? >> 
> opt(sockaddr_struct(addr_sz), m > 0 && m <= n)
> , addr_sz: &(socklen_t addr_sz)
> ): #[m:int | m <= n] ssize_t(m) = "mac#recvfrom"
> }
> ```
> and the usage:
>
> ```
> var sin: sockaddr_in_struct?
> var sin_sz: socklen_t(socklen_in) = socklen_in
> extern castfn socklen2int{n:int}(i: socklen_t(n)): 
> int(n)
> val () = assert_errmsg(socklen2int(sin_sz) > 0, 
> "sin_sz <= 0") (* should be {n:pos} socklen_t(n), to not to prove, that 
> sockaddr size > 0 *)
> extern praxi sockaddr_in_trans_nil( pf: 
> !sockaddr_in_struct? @ sin >> sockaddr_struct(socklen_in)? @ sin): void
> extern praxi sockaddr_trans_in_nil( pf: 
> !sockaddr_struct(socklen_in)? @ sin >> sockaddr_in_struct? @ sin): void
> prval () = sockaddr_in_trans_nil( view@sin)
> val readed = $C.recvfrom( recv_buf_pf |  x.fd, 
> recv_buf, recv_sz, 0, sin, sin_sz)
>   in
> if readed <= 0
> then let
> val _ = $extfcall( int, "sprintf", str_buf, 
> "unable to read from socket")
> val () = $Log.log_error( addr@str_buf)
> prval $C.recvfrom_v_fail( recv_buf_pf1) = 
> recv_buf_pf
> prval () = recv_buf_pf := recv_buf_pf1
> prval () = opt_unnone( sin)
> prval () = sockaddr_trans_in_nil( view@sin)
>   in () end
> else let
> val ureaded = g1int2uint(readed)
> prval $C.recvfrom_v_succ( request_pf, rest_buf_pf) 
> = recv_buf_pf
> prval () = opt_unsome(sin) (* sin had been 
> initialized *)
> 
> (* do useful stuff here *)
> val _ = $extfcall( int, "sprintf", str_buf, 
> "readed %li bytes", ureaded)
> val () = $Log.log_info( addr@str_buf)
> val () = handle_client_packet( request_pf | x.fd, 
> recv_buf, ureaded, sin, sin_sz)
> 
> (* now cleanup buffers and proofs*)
> extern prfun array_v_nil_nz{a:viewt0ype}{n:pos}( 
> p: array_v(a,l,n)): array_v(a?,l,n) (* there is no std way to mark 
> initialized array as uninitialized *)
> prval request_nil_pf = array_v_nil_nz( request_pf)
> prval () = recv_buf_pf := array_v_unsplit( 
> request_nil_pf, rest_buf_pf)
> prval () = sockaddr_trans_in(view@sin)
>   in () end
> ```
>
>

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" 

Re: datavtypes

[gmhwxi]

Your idea is correct. Here is what I would do:


dataview
recvfrom_v(addr, int, int) =
|
{l:addr}
{n:int}
{m:int | m < 0}
recvfrom_v_fail(l, n, m) of array_v(char?, l, n)
|
{l:addr}
{n:int}
{m:nat|m <= n}
recvfrom_v_succ(l, n, m) of
(array_v(char, l, m), array_v(char?, l+m*sizeof(char), n-m))


fn
recvfrom
{l: addr} {n: pos}
( buf_pf
: array_v(char?, l, n) >> recvfrom_v(l, n, m)
| socket_fd: int
, buf: ptr l
, sz: size_t n
, flags: int
, src_addr: _in_struct? >> opt(sockaddr_in_struct, m >= 0)
, addr_sz: _t
) : #[m:int] ssize_t(m)

Please note the symbol '#' in front of the quantifer [m:int].


On Friday, July 10, 2020 at 9:08:21 AM UTC-4, Dambaev Alexander wrote:
>
> My current, not so successful try is to define result_vt:
>
> datavtype result_vt (av: view, a:t@ype+, bv: view, b:t@ype+) =
>   | Success_vt(av,a, bv, b) of (av | a)
>   | Failure_vt(av,a, bv, b) of (bv | b)
>
> and function's ftype:
> fn
>   recvfrom
>   {l: addr} {n: pos}
>   ( buf_pf: array_v(char?, l, n)
>   | socket_fd: int
>   , buf: ptr l
>   , sz: size_t n
>   , flags: int
>   , src_addr: _in_struct?
>   , addr_sz: _t
>   ): [m:pos | m <= n] result_vt( (array_v(char,l,m), array_v(char?,l+m, 
> n-m)), (sockaddr_in_struct, size_t m), array_v(char?,l,n), void) =
>   let
> val ret = g1ofg0( $extfcall(ssize_t, "recvfrom", socket_fd, buf, sz, 
> flags, addr@src_addr, addr@addr_sz))
>   in
>   if ret < 1
>   then Failure_vt( buf_pf | ())
>   else Success_vt( (answer_pf, rest_buf_pf) | (src_addr, ret) (*complains 
> on this line *) ) where {
> extern praxi unnil{v:viewt0ype} ( p: ? >> v): void
> prval () = unnil(src_addr)
> val (answer_pf, rest_buf_pf) = array_v_split( buf_pf)
>   }
>   end
>
> but compiler is not happy with it, giving me errors:
> error(3): the dynamic expression cannot be assigned the type 
> [S2EVar(5259)].
> error(3): mismatch of sorts in unification:
> The sort of variable is: S2RTbas(S2RTBASimp(9; t@ype+))
> The sort of solution is: S2RTbas(S2RTBASimp(3; viewt0ype))
> error(3): mismatch of static terms (tyleq):
> The actual term is: S2Etyrec(flt0; npf=-1; 0=S2EVar(5253), 
> 1=S2Eapp(S2Ecst(g1int_int_t0ype); S2Eextkind(atstype_ssize), 
> S2Evar(i$8638$8639(14396
> The needed term is: S2EVar(5259)
>
>
> пт, 10 июл. 2020 г. в 12:47, ice.r...@gmail.com <...>:
>
>>
>> Hi again :)
>>
>> I have function
>>
>> fn
>>   recvfrom
>>   {l: addr} {n: pos}
>>   ( buf_pf: array_v(char?, l, n)
>>   | socket_fd: int
>>   , buf: ptr l
>>   , sz: size_t n
>>   , flags: int
>>   , src_addr: _in_struct?
>>   , addr_sz: _t
>>   ): [m:int] ssize_t int
>>
>> I want to change it's return type, such that in case of success, it 
>> should split buf_pf on 2 arrays: initialized and unintialized one and 
>> src_addr to became initialized.
>> In case of failure, I want to return buf_pf and src_addr of the same view 
>> (uninitialized)
>>
>> How can I do it properly?
>>
>> -- 
>> 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/O-KlWtJqq1I/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/e013b1ec-d89b-49f9-b79a-46803b480bcen%40googlegroups.com
>>  
>> 
>> .
>>
>

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/d8feb7fb-74a2-4a7c-83f6-5bb7c1667054o%40googlegroups.com.

Re: ATS2: need help with arrays

[gmhwxi]

  >> (* how should I initialize array here so fds_pf will switch it's type 
from array_v(pollfd_t?, l, nfds) into array_v(pollfd_t, l, nfds)? *)

You have an array of size 1 in your code.

prval (pf1, pf2) = array_v_uncons(fds_pf)
val () = !fds_addr.fd = ...
val () = !fds_addr.events = ...
val () = !fds_addr.revents = ...
prval pf2 = array_v_unnil_nil(pf2)
prval () = fds_pf := array_v_uncons(pf1, pf2)

This can be quite involved. In general, writing C-style code in ATS2 is 
labor intensive :(


On Tuesday, July 7, 2020 at 10:32:04 AM UTC-4, Dambaev Alexander wrote:
>
> ah. my bad: I had actually used 
> ```
> fun poll
>   {n: nat | n > 0}{l: addr}
>   ( fds_pf: !array_v( pollfd_t, l, n) >> _ (* proof, that we have 
> access to address range (l,n), which contains initialized array of elements 
> of type pollfd_t *)
>   | fds: ptr l (* address *)
>   , nfds: size_t n (* range size *)
>   , timeout: int
>  ): int = "ext#"
> ```
>
> But misplaced refinement spec, while was writing email.
>

-- 
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/b19f5fdb-04d2-4e48-b962-92ce589c6143o%40googlegroups.com.

Re: ATS templates vs. C++ templates

[gmhwxi]

Here is an example of template metaprogramming in ATS3:

(* ** ** *)
abstype Z
abstype S(type)
(* ** ** *)
#extern
fun



dotprodN
( xs: array(a, n)
, ys: array(a, n)): a
(* ** ** *)
impltmp
{a:t0}
dotprodN
<0>(_, _) = g_0()
(* ** ** *)
impltmp
{a:t0}
{N:t0}
{n1:i0}
dotprodN

{n1 > 0}(xs, ys) =
head(xs)*head(ys)+dotprodN(tail(xs),tail(ys))
(* ** ** *)

The above ATS code roughly corresponds to the following C++ code:

template

struct DotProductT {

static inline T result(T* a, T* b) {

return *a * *b + DotProduct::result(a+1,b+1);

}

};

*// partial specialization as end criteria*

template

struct DotProductT {

static inline T result(T*, T*) {

return T{};

}

};



On Sunday, July 5, 2020 at 6:53:44 PM UTC-4, gmhwxi wrote:
>
>
> When I see a programming feature, I tend to ask myself immediately how 
> such a feature
> can be implemented. Not trying to get the fine details. Just the big 
> picture.
>
> The template system in C++ is first and foremost a macro system. Of 
> course, in order to
> better understand C++, we need to start with C.
>
> In programming language implementation, we face the issue of binding of 
> names early on.
> Basically, if a function foo is used in some code, we need to figure out 
> where the 'foo' is declared.
>
> For instance, static binding in ATS3 is handled in the module trans12 (for 
> translating from level-1 
> o level-2).
>
> C originates from assembly, which explains very well the way in which 
> binding is handled in C.
> Every function in C is given a unique global name. If there are two 
> functions of the same name,
> a link-time error is to be reported (by the command, say, ld). By the way, 
> if I ever want to make sure
> that a chosen name is globally unique, I often just map the name to a 
> dummy C function (assuming
> I am compiling to C); a link-time error is to occur if the name turns out 
> to be not unique.
>
> The C++ template system handles binding like C but with a twist, that is, 
> overloading resolution. In short,
> if there are two or more declarations for a name, say. foo, then there 
> needs to be a way to determine
> which of these declarations should be selected. C++ makes heavy use of the 
> types of the arguments of
> foo when determine the selection. Once a template/macro declaration is 
> selection, it is used to perform
> macro expansion; and the expanded code goes through type-checking.
>
> ATS does binding based on the model of lambda-calculus, which is the gold 
> standard for static binding.
> Actually, Alonzo Church invented lambda-calculus for studying binding and 
> substitution. After each template
> function is declared, it can be implemented in a legal scope as many times 
> as is needed. Note that a legal
> scope refers to one where the declared template function is accessible. 
> Let me use an example to clarify a bit.
> The following template function g_equal is for testing whether two given 
> values are equal:
>
> #extern
> fun
> 
> g_equal(x: a, y: a): bool
>
> impltmp
> g_equal(x, y) = (x = y) // integer equality
>
> impltmp
> 
> g_equal(xs, ys) =  // equality on lists
>
> The first implementation of g_equal is given the type:
>
> (int, int) -> bool
>
> The second implementation of g_equal is given the type:
>
> {a:type} (list(a), list(a)) -> bool
>
> Note that both implementations have types that are special
> instances of the general type for g_equal: 
>
> {a:type} (a, a) -> bool
>
> Say g_equal is used in some code. ATS uses the type of this instance of 
> g_equal
> to select (based the static scoping principle) the "closest" 
> implementation of g_equal
> that has a matching type. There is no macro expansion involved. At least 
> not in the
> traditional sense.
>
> Where is the need for traits in ATS3?
>
> The search used for template resolution ATS3 is like finding a matching 
> ancestor in a tree
> (of implementations of a template functions).
>
> Say that an ancestor is found. Is it the right one? If some form of 
> backtracking is allowed,
> then we can determine whether it is the right one later. But if no 
> backtracking is allowed,
> then one often applies a quick test to tell if the found ancestor should 
> be returned or skipped.
> And traits can be used to construct this quick test.
>
> In summary, I envision introducing traits in ATS3 to affect the way in 
> which template resolution
> is performed.
>
> 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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/0d199a8d-e203-457a-b77b-10223c634dd8o%40googlegroups.com.

ATS templates vs. C++ templates

[gmhwxi]

When I see a programming feature, I tend to ask myself immediately how such 
a feature
can be implemented. Not trying to get the fine details. Just the big 
picture.

The template system in C++ is first and foremost a macro system. Of course, 
in order to
better understand C++, we need to start with C.

In programming language implementation, we face the issue of binding of 
names early on.
Basically, if a function foo is used in some code, we need to figure out 
where the 'foo' is declared.

For instance, static binding in ATS3 is handled in the module trans12 (for 
translating from level-1 
o level-2).

C originates from assembly, which explains very well the way in which 
binding is handled in C.
Every function in C is given a unique global name. If there are two 
functions of the same name,
a link-time error is to be reported (by the command, say, ld). By the way, 
if I ever want to make sure
that a chosen name is globally unique, I often just map the name to a dummy 
C function (assuming
I am compiling to C); a link-time error is to occur if the name turns out 
to be not unique.

The C++ template system handles binding like C but with a twist, that is, 
overloading resolution. In short,
if there are two or more declarations for a name, say. foo, then there 
needs to be a way to determine
which of these declarations should be selected. C++ makes heavy use of the 
types of the arguments of
foo when determine the selection. Once a template/macro declaration is 
selection, it is used to perform
macro expansion; and the expanded code goes through type-checking.

ATS does binding based on the model of lambda-calculus, which is the gold 
standard for static binding.
Actually, Alonzo Church invented lambda-calculus for studying binding and 
substitution. After each template
function is declared, it can be implemented in a legal scope as many times 
as is needed. Note that a legal
scope refers to one where the declared template function is accessible. Let 
me use an example to clarify a bit.
The following template function g_equal is for testing whether two given 
values are equal:

#extern
fun

g_equal(x: a, y: a): bool

impltmp
g_equal(x, y) = (x = y) // integer equality

impltmp

g_equal(xs, ys) =  // equality on lists

The first implementation of g_equal is given the type:

(int, int) -> bool

The second implementation of g_equal is given the type:

{a:type} (list(a), list(a)) -> bool

Note that both implementations have types that are special
instances of the general type for g_equal: 

{a:type} (a, a) -> bool

Say g_equal is used in some code. ATS uses the type of this instance of 
g_equal
to select (based the static scoping principle) the "closest" implementation 
of g_equal
that has a matching type. There is no macro expansion involved. At least 
not in the
traditional sense.

Where is the need for traits in ATS3?

The search used for template resolution ATS3 is like finding a matching 
ancestor in a tree
(of implementations of a template functions).

Say that an ancestor is found. Is it the right one? If some form of 
backtracking is allowed,
then we can determine whether it is the right one later. But if no 
backtracking is allowed,
then one often applies a quick test to tell if the found ancestor should be 
returned or skipped.
And traits can be used to construct this quick test.

In summary, I envision introducing traits in ATS3 to affect the way in 
which template resolution
is performed.

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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/7c4f6715-72bb-4fc1-b843-a763637f7f7co%40googlegroups.com.

Witnessing the effectiveness of types in detecting bugs

[gmhwxi]

I did this sort of practice before. And I paid a closer attention this time.

I implemented an interpreter for ATS3 that could handle programs containing
type-errors. I tried it to test some of the ATS3 library code (consisting 
of about 15K
lines for now). After I got the non-dependent type-checker for ATS3 
working, I tried
type-checking the library code (that had already passed unit tests). Did I 
find bugs?
A large number of them. And I have been writing this kind of code for more 
than 20
years!

Once I get the dependent and linear type-checker ready, I am certain that 
many more
bugs will be flushed out. In particular, I am certain that a lot of memory 
leak bugs will
be detected.  If I extrapolate a bit, I am pretty certain that the bug 
ratio in C and C++
code is quite significant.

Regarding the COVID-19 cases out there, I suppose we can find many more of 
them if
our detection method becomes more effective. The same can be said about the 
bugs in
our code.

--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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/97b1c18a-ae9b-4f17-9322-2122edd1a004o%40googlegroups.com.

Re: Will Traits and Concepts be supported in ATS3?

[gmhwxi]

>>I would say traits are type properties

I like your description :)

##

Let me use some pseudo code to illustrate a kind of support for traits
that can be quickly implemented for ATS3.

Say we have a template:

#extern
fun

foo(x: a): void

And we have two different implementations for foo:

impltmp
{a}
foo(x) = (* first *)

impltmp

foo(x) = (* second *)

Now we have two instances of foo in our code:

val () = foo(100)
val () = foo("100")

Say that the first instance should use the first implementation of foo
and the second instance should use the second implementation of foo.
To achieve this, we could introduce a trait called FOO2 for the second
implementation:


impltmp

FOO2(a) => foo(x) = (* second *) // the pseudo syntax means that this 
implementation is guarded by FOO2(a)

Let FOO2 be given the following implementations:

impltmp
{a:type}
FOO2 = true
impltmp
FOO2 = false

To compile the instance foo, the second implementation is first 
picked; but the guard FOO2 is false;
so this implementation is skipped and the first implementation is picked 
next.

##

Using traits for constructing guards is a low-hanging fruit. We could 
certainly think of ways for traits to be used to
guide template resolution in a more profound manner.

--Hongwei





On Friday, July 3, 2020 at 4:29:29 PM UTC-4, Matthias Wolff wrote:
>
> C++ Term Traits:
>
> I would say traits are type properties
>
> struct oracle;
>
> struct postgres;
>
> template
> void print_database(T t /* value only for type deduction -- avoiding 
> explicit <>*/)
> {
> /*Type resolution: database is unknown at this stage, database is a 
> dependend type, but type dependend */
>
> if constexpr (is_same::value) { cout << 
> "oracle" << endl; return; }
>
> else if constexpr (is_same::value) { 
> cout << "postgres" << endl; return;}
>
> else { static_assert("Unsupported type"); }
> }
>
> struct abc
> {
> };
>
> struct def
> {
> };
>
> template
> struct db_traits;
>
> template<>
> struct db_traits
> {
> using database = oracle;
> };
>
> template<>
> struct db_traits
> {
> using database = postgres;
> };
>
> template
> struct something
> {
> using database = typename T::database;
> };
>
> int main()
> {
> something s;
>
> print_database(s);
>
> return 0;
>
> }
>
> Typetraits are lightweight information because the implementations of the 
> types/structs/classes
> are not of interest. Types are only names in this context.
>
> Remark: Generic programming is like any abstraction if only one example is 
> available.
> It makes things more complicated. But looking on universal properties it's 
> clear it needs
> a bunch of examples to get a benefit. So many developers can live without 
> it. But everyone
> will try it - the "feature" effect.
>
> C++ term concepts:
>
> It's relatively new, available since C++-20. It an improvement in the area 
> specification of
> templated constructions. Typically, in the C++ world it's forbidden to use 
> a mathematical
> vocabulary. Make better specifications seems to be the goal. I have no 
> personal experiences. 
>
> Remark2: C++ concepts is an additional feature but not a concept. The 
> world of C++ scientists
> is restricted by C++. It's more a (distinct) feeling: replace concepts by 
> ats-proofing.
>
> Be sure, other c++ developers will tell you other things.
> Am 03.07.20 um 20:10 schrieb gmhwxi:
>
>
> Traits:
>
> Based on my understanding, traits in C++ can be implemented in a more or 
> less
> straightforward manner. To me, traits are an template-based approach for 
> generating
> ifdef-guards used in C.
>
> However, I would prefer to take a deeper look at the template resolution 
> algorithm. Traits are
> a bit like band-aid used at surface. One can expect to achieve a lot more 
> if there is a logical way
> to affect the manner in which template code is replaced with non-template 
> code.
>
> Concepts:
>
> It is a feature mainly for statically debugging templates. I am looking 
> into it. Debugging templates
> statically is a big thing; I prefer something with clearer semantics. 
> Let's wait and see.
>
> -- 
> 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/337ff3b2-40ed-43cc-9e0f-d62cfa6e4a42o%40googlegroups.

Will Traits and Concepts be supported in ATS3?

[gmhwxi]

Traits:

Based on my understanding, traits in C++ can be implemented in a more or 
less
straightforward manner. To me, traits are an template-based approach for 
generating
ifdef-guards used in C.

However, I would prefer to take a deeper look at the template resolution 
algorithm. Traits are
a bit like band-aid used at surface. One can expect to achieve a lot more 
if there is a logical way
to affect the manner in which template code is replaced with non-template 
code.

Concepts:

It is a feature mainly for statically debugging templates. I am looking 
into it. Debugging templates
statically is a big thing; I prefer something with clearer semantics. Let's 
wait and see.

-- 
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/337ff3b2-40ed-43cc-9e0f-d62cfa6e4a42o%40googlegroups.com.

Re: The current status of ATS3

[gmhwxi]

I had originally assumed that the following style of ATS template 
implementation
could also be done in C++. But I realized that this is* not *the case after 
studying
C++ templates tonight.

fun

g_print(x: a): void

impltmp
{a:type}
g_print(xs) = ...

Did I miss something about C++ templates? It seems that the template 
parameters
of a template implementation in C++ must be variables.

--Hongwei

On Tuesday, June 30, 2020 at 4:04:29 PM UTC-4, gmhwxi wrote:
>
> Hi Artyom,
>
> I will try to answer other questions later.
>
> >>Why are ATS3 templates more powerful than C++ templates? Could you 
> contrast the two in some way?
>
> I have to say that I do not use C++ on a regular basis.
> C++ used to be C + classes + templates. By the way, I often jokingly tell 
> others this is what the two plusses in
> C++ stand for :)
>
> C does not support inner functions. C++ used to support no inner 
> functions. Now C++ support 'lambdas', with
> which you can implement inner functions. But can you implement inner 
> templates in C++?
>
> ATS supports embedded templates (that is, inner templates). I don't know 
> whether C++ supports inner templates.
> If it doesn't. then ATS is more powerful in this regard. This is a big 
> deal because inner templates are used ubiquitously
> in ATS library code.
>
> Also, with dependent types and linear types, you can do a great deal more 
> of static checking on templates,
> flushing out potential bugs. The introduction of features like concepts in 
> C++ tells me that template-related
> bugs can be quite nasty, cutting big into the benefits from using 
> templates.
>
> Maybe "powerful" is not the right word. There is raw power and there is 
> controlled power. Kind of like nuclear
> bombs versus nuclear power plants. I was mostly talking about the latter.
>
>
>
>
>
>
>
>
>
> On Tue, Jun 30, 2020 at 2:55 PM Artyom Shalkhakov <...> wrote:
>
>> Hi Hongwei,
>>
>> Thank you very much for this work!
>>
>> On Monday, June 29, 2020 at 9:40:33 PM UTC+3, gmhwxi wrote:
>>>
>>>
>>> For those interested in ATS3.
>>>
>>> Before I take a break, I would like to give you an update on the
>>> implementation of ATS3.
>>>
>>> To put things into some sort of perspective, let me first say a few
>>> words on the motivation behind ATS3.
>>>
>>> Advised by Prof. Frank Pfenning, I did my PhD thesis on PROGRAM
>>> VERIFICATION during my years at CMU, designing and implementing DML
>>> (Dependently Typed ML), a programming language that extends ML with a
>>> restricted form of dependent types. Note that DML is the predecessor of 
>>> ATS.
>>> These days, the dependent types in DML are often referred to as DML-style
>>> dependent types in the literature (in contrast to Martin-Lof's dependent 
>>> types
>>> that were originally invented for creating a type-theoretic foundation 
>>> for Mathematics).
>>>
>>> As you can see, there are two words in PROGRAM VERIFICATION. One must
>>> talk about program construction when talking about program
>>> verification. Originally, the kind of programs I intended to verify
>>> were supposedly written in an ML-like language. But it soon (even
>>> before 2008) became very clear to me that such a language badly lacks
>>> meta-programming support. And I immediately started to improvise. I
>>> first added some support for templates into ATS1 and then strengthened
>>> it in ATS2.  Unfortunately, the kind of support for templates in ATS2
>>> was in direct conflict with the support for dependent types. The
>>> original primary motivation for ATS3 was to eliminate this (crippling)
>>> conflict.
>>>
>>> Up to ATS2, I mostly did language implementation for the purpose of
>>> experimenting with a variety of programming features. At this point, I
>>> no longer feel that I have time and/or energy to continue
>>> experimenting. Compared to ATS2, I re-designed the implementation of
>>> ATS3 to make it much more modular so as to better support future
>>> changes and additions. I intend for ATS3 to eventually become a language
>>> of production quality.
>>>
>>> ATS3 is implemented in ATS2. There are three big components planned
>>> for ATS3: program construction (Part I), program compilation (Part 2),
>>> and program verification (Part 3).
>>>
>>> ##
>>>
>>> Part 1:
>>>
>>> At this moment, I have nearly finished Part I.
>>>
>>> This part c

Re: Two much accuracy can actually be bad

[gmhwxi]

Here is another way to see the issue I mentioned in my original message.

Say we have the following interface:

fun

fmemq(xs: list(a)): (a -> bool)

The function fmemq is supposed to turn a given list into a function that 
checks if a given
element is in the given list.

Suppose that we do

val foo = fmemq(xs) where { val xs = 1::2::3::nil() }

Say we infer a dependent type list(T) for the list xs where T = [a:int | 
a=1 || a=2 || a=3] int(a).
Note that T is the type precisely for the three integers 1, 2, and 3. Then 
the function foo is of
the type (T -> bool), which make foo not a very useful function. Why? 
Because foo is actually
a constant function that maps every integer in its domain to true. This is 
just an interesting example
showing that inferring the "most accurate" types may not actually be what 
the programmer really wants.

On Thursday, July 2, 2020 at 5:52:44 PM UTC-4, Brandon Barker wrote:
>
> But isn't this example similar to the idea of literal types?; defeating 
> the need for such checks can avoid runtime costs as well as add specificity 
> and safety to function signatures. Maybe I misunderstood some subtlety.
>
> On Thu, Jul 2, 2020, 4:51 PM gmhwxi <...> wrote:
>
>>
>> Today, I encountered a very interesting issue involving dependent types.
>>
>> Say, I have a string "abcde". Then I can use the string to create a 
>> predicate P:
>>
>> val P = fmemq("abcde"): bool
>>
>> Given a char x, P(x) returns true if and only if x appears in the string 
>> "abcde".
>>
>> What is the type for P?
>>
>> In a non-dependent type system, P is usually given the type: (char) -> 
>> bool.
>>
>> Given a sequence xs containing elements of type T, fmemq(xs) returns a 
>> function
>> of type (T) -> bool. For the string "abcde", this T is precisely the type 
>> for chars
>> ranging over "abcde". In other words, fmemq("abcde") is a function that 
>> can be applied
>> to a char c only if c appears in "abcde". This defeats the very need for 
>> fmemq("abcde"):
>> If it can ever be applied, then the application always returns true.
>>
>> Have fun!
>>
>> --Hongwei
>>
>>
>>
>> But in a dependent type system, 
>>
>> -- 
>> 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/61afb765-afe1-48be-a3fe-12e33b28b924o%40googlegroups.com
>>  
>> <https://groups.google.com/d/msgid/ats-lang-users/61afb765-afe1-48be-a3fe-12e33b28b924o%40googlegroups.com?utm_medium=email_source=footer>
>> .
>>
>

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/aff4fdba-4139-4fc9-9968-41f9087eba24o%40googlegroups.com.

Two much accuracy can actually be bad

[gmhwxi]

Today, I encountered a very interesting issue involving dependent types.

Say, I have a string "abcde". Then I can use the string to create a 
predicate P:

val P = fmemq("abcde"): bool

Given a char x, P(x) returns true if and only if x appears in the string 
"abcde".

What is the type for P?

In a non-dependent type system, P is usually given the type: (char) -> bool.

Given a sequence xs containing elements of type T, fmemq(xs) returns a 
function
of type (T) -> bool. For the string "abcde", this T is precisely the type 
for chars
ranging over "abcde". In other words, fmemq("abcde") is a function that can 
be applied
to a char c only if c appears in "abcde". This defeats the very need for 
fmemq("abcde"):
If it can ever be applied, then the application always returns true.

Have fun!

--Hongwei



But in a dependent type system, 

-- 
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/61afb765-afe1-48be-a3fe-12e33b28b924o%40googlegroups.com.

The current status of ATS3

[gmhwxi]

For those interested in ATS3.

Before I take a break, I would like to give you an update on the
implementation of ATS3.

To put things into some sort of perspective, let me first say a few
words on the motivation behind ATS3.

Advised by Prof. Frank Pfenning, I did my PhD thesis on PROGRAM
VERIFICATION during my years at CMU, designing and implementing DML
(Dependently Typed ML), a programming language that extends ML with a
restricted form of dependent types. Note that DML is the predecessor of ATS.
These days, the dependent types in DML are often referred to as DML-style
dependent types in the literature (in contrast to Martin-Lof's dependent 
types
that were originally invented for creating a type-theoretic foundation for 
Mathematics).

As you can see, there are two words in PROGRAM VERIFICATION. One must
talk about program construction when talking about program
verification. Originally, the kind of programs I intended to verify
were supposedly written in an ML-like language. But it soon (even
before 2008) became very clear to me that such a language badly lacks
meta-programming support. And I immediately started to improvise. I
first added some support for templates into ATS1 and then strengthened
it in ATS2.  Unfortunately, the kind of support for templates in ATS2
was in direct conflict with the support for dependent types. The
original primary motivation for ATS3 was to eliminate this (crippling)
conflict.

Up to ATS2, I mostly did language implementation for the purpose of
experimenting with a variety of programming features. At this point, I
no longer feel that I have time and/or energy to continue
experimenting. Compared to ATS2, I re-designed the implementation of
ATS3 to make it much more modular so as to better support future
changes and additions. I intend for ATS3 to eventually become a language
of production quality.

ATS3 is implemented in ATS2. There are three big components planned
for ATS3: program construction (Part I), program compilation (Part 2),
and program verification (Part 3).

##

Part 1:

At this moment, I have nearly finished Part I.

This part covers type inference (involving only ML-style algebraic
types) and template resolution (this is, replacing template instances
with proper template-free code).  There is currently a rudimentary
interpreter available for interpreting programs constructed in ATS3. I
have also being implementing a template-based prelude library for
ATS3.

Part 2:

I will soon be starting to work on Part 2 after taking a break, hoping
to finish something that can be tested at the end of the Summer.

Part 3:

This part essentially does type-checking involving linear types and
dependent types. Hopefully, I will be able to get a running implementation
by the Spring next year.

##

Based on what I have experimented so far, I find the current support
for templates in ATS3 to be a game-changing programming feature that
can greatly increase one's programming productivity. I am a bit amazed
by it :) If you think that the templates in C++ are powerful, then you
will find that the templates in ATS3 are even more powerful in many
aspects. Actually, not only just more powerful but also a great deal
safer. Keep tuned.

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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/43a7cde4-bc45-4c89-a3e1-0af2ab164927o%40googlegroups.com.

Re: At-views and isomorphisms

[gmhwxi]

Yes, we should support:

If T1 <= T2 then T1@l <= T2@L

There is a subtyping relation <= on types.
T1 <= T2 means that T1 is a subtype of T2, which
means a value of T1 can be treated as a value of T2.

The safe cast function can be declared as:

castfn cast_safe (pf: T1 <= T2 | x: T1): T2

For each type constructor, there should be a corresponding
subtyping rule.

However, constructing subtyping proofs is very tedious and should
be automated. In ATS2, casting is unsafe as no proof is required.

By the way, the various g0ofg1/g1ofg0 functions are just hacks. I have
removed these functions in ATS3. Such functions are needed in ATS2
primarily for the sake of selecting template implementations based on
(dependent) types. In ATS3. template selection is based on the erasures
of dependent types, which are algebraic (that is, no quantifiers are 
involved).

More later.

Cheers!

--Hongwei


On Friday, April 24, 2020 at 3:52:39 PM UTC-4, August Alm wrote:
>
> Hi!
>
> Jumping straight to it, consider the following types
> (here [a: t0ype+], say):
>
> node0_t(a) = @{entry = a, next = ptr}
>
> and
>
> node1_t(a) = [l: addr] @{entry = a, next = ptr(l)}
>
> Using the pure cast-functions [g1ofg0_ptr] and
> [g0ofg1_ptr] I can write down corresponding pure
> functions [g1ofg0_node] and [g0ofg1_node] to pass
> back and forth between the two types. However, say
> I'd like to define something like singly linked lists
> (or segments) using views and introduce the view
>
> node_v(a, l, l_next) =
>   @{entry = a, next = ptr(l_next)} @ l
>
> In light of the equivalence of [node0_t(a)] and
> [node1_t(a)], there should be a corresponding way
> to pass between the view
>
> node0_t(a) @ l
>
> and
>
> [l_next: addr] node_v(a, l, l_next) 
>
> My concrete question is: Is there a way to do so
> without brute-forcing it with an "extern prfun" (left
> without implementation)?
>
> More generally, if [a1] and [a2] are "equal", then the
> views [a1 @ l] and [a2 @ l] should be "equal". I know
> equality of types is very tricky business but at least
> in the case above it should somehow be enforced, I
> think. There are many such cases is ATS, where we
> have a non-dependent incarnation and a dependently
> typed incarnation of the "same" type.
>
> ptr vs [l: addr] ptr(l)
> int  vs [n: int] int(n),
> list(a)  vs [n: nat] list(a, n),
> and so on.
>
> [g0ofg1] and [g1ofg0] are overloaded to cover most
> of these. But for translating between the corresponding
> at-views?
>
>
> 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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/df3f8546-8a0a-4c67-9545-79876465b47a%40googlegroups.com.

Re: Declarations of external values & functions from separate file showing up as "undeclared"

[gmhwxi]

I took a quick look.

You used '#include' in many places.

When a SATS file is included, each of the following kind of code blocks
is discarded.

%{#
...
%}

In general, a SATS file should not be included in another file;
it should be staloaded. Say you have:

foo1.sats
foo2.sats
foo3.sats

You can then create foo_all.hats of the following content:

#staload "foo1.sats"
#staload "foo2.sats"
#staload "foo3.sats"

This foo_all.hats can be included in another file.

How to fix the problem you have now?

First, keep including SATS files as you did.
I suggest that you put all the code blocks of the
following form into a single SATS file called, say,
SDL2_headers.sats:

%{#
...
%}

Then just make sure that this file is staloaded in a file like
g_audio.dats.

By the way, you don't need to compile SATS files. You only
need to compile DATS files. Only when you introduce an exception
constructor in a SATS file, you need to compiler that SATS file.

Hope this helps.

On Sunday, April 19, 2020 at 3:34:15 PM UTC-4, d4v3y_5c0n3s wrote:
>
>  For roughly a week now, I've been having this issue where PATSCC 
> successfully typechecks my file, but when it tries to compile it to C an 
> error is produced due to GCC not seeing the values/functions that I am 
> using.  These values and functions are declared in a separate file, which 
> is staload-ed in properly.  After some testing, I was able to determine 
> that when my code was inserted into the ATS-contrib SDL library code, no 
> such errors were produced.  This most likely means that *the issue is 
> with my Makefile, and not the code itself.*  If you'd like to see my code 
> and/or the Makefile, it is available in my Github repository with is linked 
> below.
>
> For anyone who takes the time to try and answer my question, thank you so, 
> so much.  And if you have any questions, just let me know.
>
> *The link to my Github repo with full source code is available here: *
> https://github.com/d4v3y5c0n3s/Goldelish-Engine 
> 
>
> *###  Here's the error message:  ###*
>
> In file included from g_audio_dats.c:15:
> g_audio_dats.c: In function 'audio_init':
> g_audio_dats.c:351:34: error: 'AUDIO_S16' undeclared (first use in this 
> function)
>  ATSINSmove(tmpref3, ATSPMVextval(AUDIO_S16)) ;
>   ^
> /home/d4v3y/ATS2-Postiats-0.4.0/ccomp/runtime/pats_ccomp_instrset.h:276:37: 
> note: in definition of macro 'ATSINSmove'
>  #define ATSINSmove(tmp, val) (tmp = val)
>  ^~~
> g_audio_dats.c:351:21: note: in expansion of macro 'ATSPMVextval'
>  ATSINSmove(tmpref3, ATSPMVextval(AUDIO_S16)) ;
>  ^~~~
> g_audio_dats.c:351:34: note: each undeclared identifier is reported only 
> once for each function it appears in
>  ATSINSmove(tmpref3, ATSPMVextval(AUDIO_S16)) ;
>   ^
> /home/d4v3y/ATS2-Postiats-0.4.0/ccomp/runtime/pats_ccomp_instrset.h:276:37: 
> note: in definition of macro 'ATSINSmove'
>  #define ATSINSmove(tmp, val) (tmp = val)
>  ^~~
> g_audio_dats.c:351:21: note: in expansion of macro 'ATSPMVextval'
>  ATSINSmove(tmpref3, ATSPMVextval(AUDIO_S16)) ;
>  ^~~~
> g_audio_dats.c:369:19: warning: implicit declaration of function 
> 'SDL_InitSubSystem' [-Wimplicit-function-declaration]
>  ATSINSmove(tmp10, SDL_InitSubSystem(ATSPMVextval(SDL_INIT_AUDIO))) ;
>^
> /home/d4v3y/ATS2-Postiats-0.4.0/ccomp/runtime/pats_ccomp_instrset.h:276:37: 
> note: in definition of macro 'ATSINSmove'
>  #define ATSINSmove(tmp, val) (tmp = val)
>  ^~~
> g_audio_dats.c:369:50: error: 'SDL_INIT_AUDIO' undeclared (first use in 
> this function)
>  ATSINSmove(tmp10, SDL_InitSubSystem(ATSPMVextval(SDL_INIT_AUDIO))) ;
>   ^~
> /home/d4v3y/ATS2-Postiats-0.4.0/ccomp/runtime/pats_ccomp_instrset.h:276:37: 
> note: in definition of macro 'ATSINSmove'
>  #define ATSINSmove(tmp, val) (tmp = val)
>  ^~~
> g_audio_dats.c:369:37: note: in expansion of macro 'ATSPMVextval'
>  ATSINSmove(tmp10, SDL_InitSubSystem(ATSPMVextval(SDL_INIT_AUDIO))) ;
>  ^~~~
> g_audio_dats.c:401:19: warning: implicit declaration of function 
> 'Mix_OpenAudio' [-Wimplicit-function-declaration]
>  ATSINSmove(tmp16, Mix_OpenAudio(ATSPMVi0nt(22050), 
> ATSPMVextval(AUDIO_S16), ATSPMVi0nt(2), ATSPMVi0nt(4096))) ;
>^
> /home/d4v3y/ATS2-Postiats-0.4.0/ccomp/runtime/pats_ccomp_instrset.h:276:37: 
> note: in definition of macro 'ATSINSmove'
>  #define ATSINSmove(tmp, val) (tmp = val)
>  ^~~
> g_audio_dats.c:433:19: warning: implicit declaration of 

Re: simulating typeclasses in ATS

[gmhwxi]

There is no need to simulate typeclasses in ATS.

To some extent, the templates in ATS are like typeclasses on steroids :)

If you'd like to have a feel for the power of templates, please take a look 
at
ATS-Temptory:

https://sparverius.github.io/tmplats-doc/

Or you can wait for ATS3 to become ready.

On Wednesday, March 18, 2020 at 8:35:29 AM UTC-4, whyu wrote:
>
> Are there any sensible ways of simulating typeclasses in ATS? I could 
> define typeclass dictionaries explicitly and manually passing it around, 
> but that would defeat the whole purpose of using typeclasses which is to 
> let the compiler choose the dictionary for me. I could also use function 
> templates but I don't know how to make them explicit in type 
> signatures(unlike typeclass constraints).
>

-- 
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/8740ee66-0e63-4a45-8b69-d7bfd1f8c475%40googlegroups.com.

Re: Should runtime's license be GPL3+RLE3.1 instead of pure GPL3?

[gmhwxi]

I am totally fine with using GPLv3 + RLE3.1. Currently, the following 
clause is mentioned on the homepage for ATS2:

As a special exception, any C code generated by the Compiler based on the 
Libraries source is not considered by default to be licensed under 
GPLv3/LGPLv3. If you use such C code together with other code to create an 
executable, then the C code by itself does not cause the executable to be 
covered by GPLv3/LGPLv3. However, there may be reasons unrelated to using 
ATS that can result in the executable being covered by GPLv3/LGPLv3.

Once ATS3 is released, my plan is to release ATS2 under the so-called MIT 
license (or 2-clause or 3-clause BSD license).

However, my perceived way of programming in ATS3 cannot be easily covered 
with GPLv3 + RLE3.1. For instance, if you write
a program in ATS3, then your program essentially directs the ATS3 compiler 
to use various templates in some libraries to assemble
a final program in a language like C. There is really some kind of paradigm 
shift as for as code generation is of the concern, which
cannot be easily addresses using GPL plus exception clauses (or any other 
licenses I am aware of). Maybe a whole new kind of license
needs to be drafted for ATS3.

On Thursday, February 20, 2020 at 7:42:23 AM UTC-5, Andreas ZUERCHER wrote:
>
> Given that RLE3.1 is (speaking very broadbrushly) a stronger LGPL but with 
> protections against utilizing a tampered compilation toolchain (see 
> Eligible Compilation Process in RLE3.1)
> https://www.gnu.org/licenses/gcc-exception-3.1.html
> and given that the runtime of most GCC languages are licensed nowadays via 
> GPL3+RLE3.1 instead of pure GPL3 (as opposed to the prior era:  GMGPL 
> pioneering the topic of runtime/template-generation additional permission 
> grants in the GPL within the Ada community first during the GPL2 era)
> and given that the compiler itself of all GCC languages are licensed 
> nowadays via pure GPL3 (as opposed to languages that dropped out of GCC 
> such as CHILL that never made it to the GPL3 era),
> I have been wondering if licensing the runtime of each variant of ATS as 
> pure GPL (i.e., without the RLE) limits the utilization of each variant of 
> ATS to only app-domain software that itself is to be licensed as pure GPL3.
>
> By licensing each ATS runtime as GPL3+RLE3.1, then each ATS compiler could 
> be utilized worry-free by certain app-domains to publicly release 
> binary-only closed-source software, which might be important to facilitate 
> ATS's usage in the enterprise, in app-store apps, and wherever closed 
> source of the resulting executable or DLL is important to the user.
>
> By licensing each ATS runtime as pure GPL3 as it is today, then each ATS 
> compiler would be limited to the pure-GPL LIBRE/FLOSS fraction of the 
> software industry that eschews even the open-source permissive licenses 
> (e.g., MIT, Apache), leaving out the permissive-licensed open-source 
> community.
>
> To relicense each ATS runtime source file, mentioning of the Runtime 
> Library Exception 3.1 would need to be added to each such runtime source 
> file—•not• at the top-level directory where the COPYING file appears.
>
> Just food for thought to ponder what the ATS community and Hongwei Xi 
> overtly intend.
>

-- 
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/cb9345a1-c9f0-49de-a029-ffa7e26448f7%40googlegroups.com.

Re: How can I best help

[gmhwxi]

Thanks for your interest and your willingness to help.

Opportunities should arise once I am able to get ATS3 to a point where
it can actually be used by others.

Cheers!


On Wednesday, February 5, 2020 at 6:43:19 AM UTC-5, rodol wrote:
>
> I really like ATS. I've been learning for quite a while now and trying to 
> spread
> awareness, and get more people to learn it.
>
> I've seen Hongwei Xi calling for concerted community efforts. I want to 
> help,
> but I still suck at ATS. I'm currently figuring out Temptory and plan to 
> start
> fiddling with Xanadu and xjsonize soon after.
>
> I don't think I am capable enough to develop anything of use in ATS yet, 
> and
> writing docs for something I'm unfamiliar with seems like a daunting task.
>
> I think I've got dependent types, templates, and theorem proving partially
> figured out, I'm just starting out with linear views.
>
> Any advice or instruction is welcome!
>

-- 
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/ce174156-4b18-4cd7-a619-c60b1182f028%40googlegroups.com.

Re: ATS3 Temptory

[gmhwxi]

Temptory was an experiment I did last summer. I was trying
to convince myself that the Temptory approach to building libraries
should be adopted in ATS3. I guess I did convince myself :)

So programming in ATS3 should be a lot like programming in Temptory
(plus the support of type inference).

On Tuesday, February 4, 2020 at 8:34:20 PM UTC-5, rodol wrote:
>
> As I understand it, Temptory is ATS2 with a different standard 
> library/prelude essentially.
>
> Will we be able to load Temptory into ATS3, after some minor porting, or 
> is the template
> system too different for that?
>

-- 
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/0bfea904-b3d7-4489-964e-3f08c7ce5277%40googlegroups.com.

Re: A brief update on ATS3 implementation

[gmhwxi]

Yes. Not just at the top level. At all inner levels as well.
Sent from my T-Mobile 4G LTE device



-- Original message--From: Raoul DukeDate: Sat, Jan 11, 2020 03:45To: 
ats-lang-users@googlegroups.com;Subject:Re: A brief update on ATS3 
implementation
my usual usability rant: any language with inference must have a mode that 
inserts the ascii of what it inferred. 
On Fri, Jan 10, 2020 at 11:39 Brandon Barker  wrote:
Great to hear about improved type inference! This quite wild to see in 
comparison to ATS2 code. 
I just hope that everyone remembers to annotate with types at least at the 
top-level; sometimes Haskellers don't do this and it makes the code more 
difficult to read, IMO (luckily that is a rarity) ;-)


On Sunday, December 15, 2019 at 10:34:46 PM UTC-5, Richard wrote:Well done! 
Looking forward to the future progress.

On Sunday, December 15, 2019 at 9:08:21 PM UTC-5, gmhwxi wrote: Hi, there,
I would like to make a brief announcement, telling those in this groupabout 
some recent progress made in the implementation of ATS3. Theproject itself is 
publicly accessible at the following site:

https://github.com/githwxi/ATS-Xanadu
Note that you need to have ATS2 installed in order to compile ATS3.

So far I have essentially finished the following parts, though changes and 
fixesare definitely needed for a long time to come:

Part 1: Concrete syntax design + ParsingPart 2: Binding resolution based on 
static scopingPart 3: Type-inference + supporting for symbol overloadingPart 4: 
Type-based template code selection
I have also implemented a basic interpreter for testing.
Compiling ATS3 to C is scheduled in the next phase. After that. advanced 
type-checking(for dependent types and linear types) needs to be supported.
Before starting the next phase, I plan to write some documentation and hope to 
get morepeople on board. More on that later.
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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/cf089bb4-7a5e-4d46-a1c7-589c966ff246%40googlegroups.com.
-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/CAJ7XQb7z%3D8Y6566rFrADEhQdENxF_pDsBNkbSaNBSV8HYkCe0A%40mail.gmail.com.


-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/000f424a.2a419e2b4fadf55f%40gmail.com.

Re: Primitives, lists, and memory

[gmhwxi]

I have to say that compiling ATS3 to LLVM is just a preliminary plan.
The primary plan as of now is still to target C. I hope that there will be a
community effort at some point. The implementation of ATS3 is already
structured in a way to facilitate such a effort (on building an ecosystem).

Cheers!

On Monday, February 3, 2020 at 3:26:24 PM UTC-5, Andreas ZUERCHER wrote:
>
> The answer(s) to this question will be fascinating & instructive to those 
> of us studying the internals of ATS.  There will likely be 2 different 
> avenues of answers:  the ATS2/Postiats (transliteration to C) answer and 
> the ATS3 (interpreter for now, then compilation to LLVM IR forthcoming) 
> answer, because the internals might differ due to the intended destination 
> of C versus LLVM IR.  Everything about ATS2 and ATS3 is intriguing.  What a 
> time to be alive!
>
> On Sunday, February 2, 2020 at 7:04:32 PM UTC-6, rodol wrote:
>>
>> I am trying to understand exactly how ATS internals work.
>>
>> I don't understand how the datatypes work. Are they like named unboxed 
>> tuples,
>> essentially? Or are they boxed? I assume they are unboxed, but then I 
>> have trouble
>> understanding how lists work, since they would be like a bunch of nested 
>> unboxed
>> tuples. Which would be problematic since they'd be passed by value, and 
>> large lists
>> would have bad performance. On the other hand, if datatypes are boxed, 
>> then lists
>> would be like linked lists, and wouldn't be linear in memory so...
>>
>> Are arrays the preferred way to get performance?
>>
>> Is there something I can read that explain this part of 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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/b3e01acc-4bf8-4842-b95c-e9cf119b4b08%40googlegroups.com.

Re: Primitives, lists, and memory

[gmhwxi]

Values of a datatype is boxed. In compiler terminology, such values are
referred to as boxed tagged union. Here is an example that may shed some 
light:

http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x2223.html

Yes, lists in ATS are the same as singly-linked lists in C.

>>Are arrays the preferred way to get performance?

Compared to lists, arrays certainly can give you more performance.
The rule of thumb for performance is that you get more performance if
you have more "flatness" in your data.

By the way, real-time systems are primarily concerned with responsiveness
(not performance).

Sorry for lack of documentation. I can only be focusing on implementing ATS3
right now :)


On Sunday, February 2, 2020 at 8:04:32 PM UTC-5, rodol wrote:
>
> I am trying to understand exactly how ATS internals work.
>
> I don't understand how the datatypes work. Are they like named unboxed 
> tuples,
> essentially? Or are they boxed? I assume they are unboxed, but then I have 
> trouble
> understanding how lists work, since they would be like a bunch of nested 
> unboxed
> tuples. Which would be problematic since they'd be passed by value, and 
> large lists
> would have bad performance. On the other hand, if datatypes are boxed, 
> then lists
> would be like linked lists, and wouldn't be linear in memory so...
>
> Are arrays the preferred way to get performance?
>
> Is there something I can read that explain this part of 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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/05d81e79-a577-432e-9260-3fa67bcd8b51%40googlegroups.com.

Documenting Xanadu

[gmhwxi]

I have started the process of documenting the concrete syntax of Xanadu:

https://github.com/githwxi/ATS-Xanadu/blob/master/docgen/SYNTAX/XanaduConcreteSyntax.md

Essentially, I am hereby putting up a collection of notes that I myself use 
in the implementation of
Xanadu. It is not meant to be "formal"; it is mostly used as some sort of 
reminder.

-- 
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/70bddd17-5b29-4e59-b2a7-fe1e7da87f43%40googlegroups.com.

Re: Are you interested in building tools for ATS3?

[gmhwxi]

> This progression might be related to something that I have been pondering: 
>  Is the shift away from ATS2's more C-family syntax to ATS3's different 
> ground syntax a direct facilitator of any or all of {A, B0, C, B} or is it 
> an orthogonal choice?
>

To some extent, the answer is yes. With type-inference, ATS3 could readily
support programming of familiar styles to programmers working in industry.

On Tuesday, December 24, 2019 at 7:12:37 PM UTC-5, Dan'l Miller wrote:
>
> Where ≺ is precedes, A ≺ B0 ≺ C ≺ B → ATS/Xanadu is lucid & compact 
> well-presented deep insight.  I had noticed clues & pieces to this effect 
> in past postings but this puts is it together directly.
>
> This progression might be related to something that I have been pondering: 
>  Is the shift away from ATS2's more C-family syntax to ATS3's different 
> ground syntax a direct facilitator of any or all of {A, B0, C, B} or is it 
> an orthogonal choice?
>
> On Tuesday, December 24, 2019 at 6:59:14 AM UTC-6, gmhwxi wrote:
>>
>>
>> What I have learned from the ATS2 experiment is a set of programming 
>> features
>> that I want to have in ATS3 and how these features should be implemented.
>>
>> Say that we have three features A, B, and C. In ATS2, they are 
>> implemented in the
>> order of A + B + C. What I learned from ATS2 is that the order should 
>> really be A + C + B,
>> that is, C should be implemented before B. Specifically, B is 
>> type-checking and C is template
>> selection. In order to implement C before B, I need to implement another 
>> feature B0:
>> A + B0 + C + B, where B0 is type-inference. This change in implementation 
>> order is fundamental.
>> To appreciate the significant of this change, one could compare Haskell 
>> without type classes (ATS2)
>> with Haskell (ATS3).
>>
>> The C-source generation issue is relatively minor. It will be properly 
>> taken care of in ATS3.
>>
>> In short, continuing to work on ATS2 is not a good choice because some 
>> fundamental changes
>> in implementation are needed to greatly improve it. Thus, ATS3!
>>
>> On Monday, December 23, 2019 at 2:20:31 PM UTC-5, Dan'l Miller wrote:
>>>
>>> Hongwei, other than the long list of fine-grained differences between 
>>> ATS/Postiats and the emerging ATS/Xanadu, what do you think stops 
>>> ATS/Postiats itself from being “a programming language suitable for use in 
>>> production”?  For example, the C-source generation could fairly easily have 
>>> begat an PostiatsAST-to-ClangAST tree-transduction to get an LLVM backend 
>>> with relatively little effort (or PostiatsAST-to-gimpleAST 
>>> tree-transduction à la GNAT to get a gcc backend).  I ask this from the 
>>> perspective of what extensions to ATS/Xanadu would most likely be steps 
>>> forward versus repeating an impediment-to-production-suitability that 
>>> AST/Postiats already might have pursued.
>>>
>>> On Monday, December 16, 2019 at 10:05:41 PM UTC-6, gmhwxi wrote:
>>>>
>>>>
>>>> The full name for ATS3 is ATS/Xanadu.
>>>>
>>>> From this point on, I would use the name 'Xanadu' for ATS3 as this 
>>>> should make it easier
>>>> for people to locate information on ATS/Xanadu.
>>>>
>>>> I have so far implemented ATS0 (ATS/Proto),  ATS1 (ATS/Geizella and 
>>>> ATS/Anairiats),
>>>> and ATS2 (ATS/Postiats). ATS/Proto and ATS/Geizella were done in OCaml 
>>>> and the others
>>>> in ATS1. I now see all of these implementations as parts of a lengthy 
>>>> programming language
>>>> experiment spanning a period of about 15 years.
>>>>
>>>> But ATS3 is designed and implemented very differently. First and 
>>>> foremost, I hope that ATS3
>>>> can become a programming language suitable for use in production. For 
>>>> that to have a chance to
>>>> ever happen, we need to build an ecosystem for ATS3. ATS3 is structured 
>>>> in a way that can
>>>> greatly facilitate collaboration of contributors.
>>>>
>>>> While it is still a bit too early for a release of ATS3, I feel that 
>>>> some people may be interested in
>>>> playing with the syntax of ATS3 and learning a few tricks about 
>>>> programming language implementation.
>>>> With that thought on my mind, I have just implemented a (naive) 
>>>> interpreter for ATS3. Please find the code
>>>> for this interpreter in the following reposit

Re: ats3 extension - jsonize abstract syntax trees

[gmhwxi]

Yes. And also to other languages such as Python, JS, etc. for, say,
web development.

On Friday, December 27, 2019 at 1:54:36 AM UTC-5, rodol wrote:
>
> Awesome! Will definitely be reading and trying it out :)
>
> Are there plans to support the reverse operation? To transform json to 
> ATS3 ASTs?
>
> On Sunday, December 22, 2019 at 6:36:46 PM UTC-8, Richard wrote:
>>
>> Hello all,
>>
>> Here is an ats3 compiler extension that I have been working on called 
>> "xjsonize", see https://github.com/sparverius/xjsonize
>>
>> Brief overview, 
>>
>>- written in ats2 
>>- similar to xinterp, links the ats3 compiler library (libxatsopt)
>>- exports the AST at any level of compilation as json
>>- provides a library libxjsonize 
>>   - link other extensions with -lxjsonize
>>   - for example, https://github.com/sparverius/xatscc,
>>  -  this example links both libxatsopt and libxjsonize to 
>>  xinterp for jsonizing the the tree of the interpreter
>>   
>> Later versions can suite specific needs however, for now the jsonized 
>> output is currently meant to be as verbose as possible with the exception 
>> of location information (coming soon!). Also, the labify branch 
>>  provides a flatter 
>> representation than the master branch. 
>>
>>
>> Some examples of the exported json can be found HERE 
>> .
>>
>>
>> Possible use cases:
>>
>>- Learn about each translation phase of the ats3 compiler
>>- Export AST to write extensions in any programming language you 
>>wish. (some examples soon!)
>>- Something else you think ofentirely??
>>
>> Personally, reading through the AST in json form has helped me 
>> tremendously with understanding the compilation phases of ats3. I hope you 
>> find it useful as well!
>>
>>
>> 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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/a0bb29cf-a818-4574-aa7a-85a488169045%40googlegroups.com.

Re: Are you interested in building tools for ATS3?

[gmhwxi]

What I have learned from the ATS2 experiment is a set of programming 
features
that I want to have in ATS3 and how these features should be implemented.

Say that we have three features A, B, and C. In ATS2, they are implemented 
in the
order of A + B + C. What I learned from ATS2 is that the order should 
really be A + C + B,
that is, C should be implemented before B. Specifically, B is type-checking 
and C is template
selection. In order to implement C before B, I need to implement another 
feature B0:
A + B0 + C + B, where B0 is type-inference. This change in implementation 
order is fundamental.
To appreciate the significant of this change, one could compare Haskell 
without type classes (ATS2)
with Haskell (ATS3).

The C-source generation issue is relatively minor. It will be properly 
taken care of in ATS3.

In short, continuing to work on ATS2 is not a good choice because some 
fundamental changes
in implementation are needed to greatly improve it. Thus, ATS3!

On Monday, December 23, 2019 at 2:20:31 PM UTC-5, Dan'l Miller wrote:
>
> Hongwei, other than the long list of fine-grained differences between 
> ATS/Postiats and the emerging ATS/Xanadu, what do you think stops 
> ATS/Postiats itself from being “a programming language suitable for use in 
> production”?  For example, the C-source generation could fairly easily have 
> begat an PostiatsAST-to-ClangAST tree-transduction to get an LLVM backend 
> with relatively little effort (or PostiatsAST-to-gimpleAST 
> tree-transduction à la GNAT to get a gcc backend).  I ask this from the 
> perspective of what extensions to ATS/Xanadu would most likely be steps 
> forward versus repeating an impediment-to-production-suitability that 
> AST/Postiats already might have pursued.
>
> On Monday, December 16, 2019 at 10:05:41 PM UTC-6, gmhwxi wrote:
>>
>>
>> The full name for ATS3 is ATS/Xanadu.
>>
>> From this point on, I would use the name 'Xanadu' for ATS3 as this should 
>> make it easier
>> for people to locate information on ATS/Xanadu.
>>
>> I have so far implemented ATS0 (ATS/Proto),  ATS1 (ATS/Geizella and 
>> ATS/Anairiats),
>> and ATS2 (ATS/Postiats). ATS/Proto and ATS/Geizella were done in OCaml 
>> and the others
>> in ATS1. I now see all of these implementations as parts of a lengthy 
>> programming language
>> experiment spanning a period of about 15 years.
>>
>> But ATS3 is designed and implemented very differently. First and 
>> foremost, I hope that ATS3
>> can become a programming language suitable for use in production. For 
>> that to have a chance to
>> ever happen, we need to build an ecosystem for ATS3. ATS3 is structured 
>> in a way that can
>> greatly facilitate collaboration of contributors.
>>
>> While it is still a bit too early for a release of ATS3, I feel that some 
>> people may be interested in
>> playing with the syntax of ATS3 and learning a few tricks about 
>> programming language implementation.
>> With that thought on my mind, I have just implemented a (naive) 
>> interpreter for ATS3. Please find the code
>> for this interpreter in the following repository:
>>
>> https://github.com/xanadu-lang/xinterp
>>
>> The basic idea is to structure xinterp as a project external to 
>> ATS/Xanadu.
>>
>> After git-cloing xinterp, please also git-clone the following repo inside 
>> the xinterp repo:
>>
>> https://github.com/xanadu-lang/xanadu
>>
>> Please do not modify the code in the xanadu repo; the code in this repo 
>> is copied from elsewhere.
>> You may ask me to do the modification, though.
>>
>> By studying xinterp (and possibly raising questions here), you can 
>> implement all kinds of tools
>> for processing the syntax of ATS3: syntax-highlighting, pretty-printing, 
>> error-messgage-reporting, etc.
>>
>> Have fun!
>>
>> --Hongwei
>>
>> --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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/9a56547b-82cf-4131-9aa9-2d42b0f72873%40googlegroups.com.

Re: Are you interested in building tools for ATS3?

[gmhwxi]

Yes.

Sometimes, I see it as a subway train: One can get on and get off
at various points.

On Sunday, December 22, 2019 at 8:23:30 AM UTC-5, rodol wrote:
>
> This is amazing, thank you for all the work you are doing!
>
> If I'm understanding this right, it is going to be possible to make all 
> sorts of language extensions
> that hook into various point of the compilation process, allowing for a 
> large variety of functionality.
> I can already see the possibility of high level optimization 
> transformations, inline cuda kernel generation,
> actual metaprogramming code generation, and so much more. This is 
> powerful...
>
> I am excited. There is much to learn...
> I'm still figuring out ATS2, I don't think I can be much help on ATS3 yet 
> :)
>
>
> On Monday, December 16, 2019 at 8:05:41 PM UTC-8, gmhwxi wrote:
>>
>>
>> The full name for ATS3 is ATS/Xanadu.
>>
>> From this point on, I would use the name 'Xanadu' for ATS3 as this should 
>> make it easier
>> for people to locate information on ATS/Xanadu.
>>
>> I have so far implemented ATS0 (ATS/Proto),  ATS1 (ATS/Geizella and 
>> ATS/Anairiats),
>> and ATS2 (ATS/Postiats). ATS/Proto and ATS/Geizella were done in OCaml 
>> and the others
>> in ATS1. I now see all of these implementations as parts of a lengthy 
>> programming language
>> experiment spanning a period of about 15 years.
>>
>> But ATS3 is designed and implemented very differently. First and 
>> foremost, I hope that ATS3
>> can become a programming language suitable for use in production. For 
>> that to have a chance to
>> ever happen, we need to build an ecosystem for ATS3. ATS3 is structured 
>> in a way that can
>> greatly facilitate collaboration of contributors.
>>
>> While it is still a bit too early for a release of ATS3, I feel that some 
>> people may be interested in
>> playing with the syntax of ATS3 and learning a few tricks about 
>> programming language implementation.
>> With that thought on my mind, I have just implemented a (naive) 
>> interpreter for ATS3. Please find the code
>> for this interpreter in the following repository:
>>
>> https://github.com/xanadu-lang/xinterp
>>
>> The basic idea is to structure xinterp as a project external to 
>> ATS/Xanadu.
>>
>> After git-cloing xinterp, please also git-clone the following repo inside 
>> the xinterp repo:
>>
>> https://github.com/xanadu-lang/xanadu
>>
>> Please do not modify the code in the xanadu repo; the code in this repo 
>> is copied from elsewhere.
>> You may ask me to do the modification, though.
>>
>> By studying xinterp (and possibly raising questions here), you can 
>> implement all kinds of tools
>> for processing the syntax of ATS3: syntax-highlighting, pretty-printing, 
>> error-messgage-reporting, etc.
>>
>> Have fun!
>>
>> --Hongwei
>>
>> --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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/13b1461c-c696-4a3e-8c54-a2378addad3b%40googlegroups.com.

Re: Are you interested in building tools for ATS3?

[gmhwxi]

Thanks for your compliment. It is really difficult to live up to it :)

>>Is it intended that all extensions of Xanadu be placed at the same 
software-architectural design points as this extension?

What xinterp and xjonsonize show is a typical way to implement a tool for 
processing or analyzing various syntax trees used
in the implementation of ATS3. For instance, pretty printing can be 
implemented in this way; error-message reporting of all sorts
can also be implemented in this way. With xjsonize, such tools can actually 
be written in other languages than ATS2.

However, what gets me really excited is to implement so-called 
meta-programming extensions. ATS3 is designed to be both a
source language and a target language. And a meta-programming extension of 
ATS3 is supposed to compile to ATS3, enabling
higher-level programming than what is supported in ATS3. Speaking of 
programming, I think we must automate and we will automate
(Hilbert's original words are: Wir müssen wissen — wir werden wissen!).

Cheers!

--Hongwei

On Saturday, December 21, 2019 at 10:21:48 AM UTC-5, Dan'l Miller wrote:
>
> Thank you for providing this extension, Richard.  (And thank you, Hongwei, 
> for being the prime-mover genius of all this; this is like watching Mozart 
> write his symphonies.)
>
> Is it intended that all extensions of Xanadu be placed at the same 
> software-architectural design points as this extension?  Or are there 
> intended to be quite different categories of extensions that are placed in 
> Xanadu's compiler at quite different software-architectural put-stuff-here 
> design points—i.e., “horses for courses” as the British say: different 
> horses are bred for different events/venues?  (I am aware of Hongwei's 
> posting in recent days regarding AST-to-AST-to-…-to-AST transforms as a key 
> microkernel-esque breakthrough design of Xanadu.  Those transforms/ASTs 
> might be part of the answer, but are their more intended put-stuff-here 
> design points?)
>
> On Saturday, December 21, 2019 at 3:09:53 AM UTC-6, Richard wrote:
>>
>> Here is an other extension example https://github.com/sparverius/xjsonize. 
>> (see the readme for building instructions)
>> Outputs the AST at each transition level in json. This can be helpful for 
>> writing other extensions or even just to learn ast.
>>
>

-- 
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/fc5cd22d-12c6-463e-b2c9-f587a50da1ff%40googlegroups.com.

How is ATS3 implementation structured?

[gmhwxi]

FYI.

The following code outlines the implementation of ATS3 so far:

val source = source_get()

val ABStree0 = source_parse(source) // parsing 
   
val (  ) = synread_abstree(ABStree0) // AST-checking   
   

val ABStree1 = trans01_abstree(ABStree0) // fixity resolution   
  
val (  ) = tread01_abstree(ABStree1) // AST-checking for trans01   
   

val ABStree2 = trans12_abstree(ABStree1) // binding resolution 
   
val (  ) = tread12_abstree(ABStree2) // AST-checking for trans12   
   
)
val ABStree30 = trans23_abstree(ABStree2) // resolving overloaded symbols   
  
val (   ) = tread23_abstree(ABStree30) // ast-checking for trans23 
   

val ABStree31 = trans33_abstree(ABStree30) // Hindley-style type-inference 
   
val (   ) = tread33_abstree(ABStree31) // ast-checking for trans33 
   

val ABStree32 = trans3t_abstree(ABStree31) // resolving template instances 
   
val (   ) = tread3t_abstree(ABStree32) // ast-checking for trans3t 
  


A functional implementation of a compiler essentially consists of a set of 
trans-functions for translating
one form of abstract syntax tree to another form.

This time I am employing a style of error-handling that internalizes errors 
inside abstract syntax trees,
relying on various checking functions (e.g., tread01, tread12) for 
inspecting abstract syntax trees to report
error-messages. My current implementation of these checking functions only 
produces error-messages that
may be difficult for others (esp. beginners) to understand. But my hope is 
that other interested parties may
re-implement these functions to give more detailed error-message reporting.

As a rough analogy, ATS3 is structured somewhat like a micro kernel (e.g., 
L4). I will focus on implementing
the "kernel" of ATS3. And other interested parties can readily add 
"services" on top of this "kernel".

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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/7fd40236-004b-4774-882c-15b350f374c8%40googlegroups.com.

Re: Are you interested in building tools for ATS3?

[gmhwxi]

I used ATS2-0.4.0.

There is only a pre-release of this version accessible at

http://www.ats-lang.org/Downloads.html#ATS_packages

Here is the direct link to it:

http://ats-lang.sourceforge.net/IMPLEMENT/Postiats/ATS2-Postiats-0.4.0.tgz

On Tuesday, December 17, 2019 at 4:15:45 PM UTC-5, Chris Double wrote:
>
> What version of ATS2 is needed to build it? Using 0.3.13 I get: 
>
> $ make libxatsopt 
> (cd ./xanadu/srcgen/xats && make libxatsopt) 
> make[1]: Entering directory 'xinterp/xanadu/srcgen/xats' 
> patsopt -o BUILD/fixity_sats.c --static SATS/fixity.sats 
> xinterp/xanadu/srcgen/xats/SATS/fixity.sats: 1776(line=62, offs=1) -- 
> 1783(line=62, offs=8): error(parsing): the token is discarded. 
> exit(ATS): uncaught exception: 
> _2home_2hwxi_2Research_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
>  
>
> make[1]: *** [Makefile:168: BUILD/fixity_sats.c] Error 1 
>
> -- 
> https://bluishcoder.co.nz 
>

-- 
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/9eba94aa-46eb-41c1-af15-e3ea8434a882%40googlegroups.com.

Are you interested in building tools for ATS3?

[gmhwxi]

The full name for ATS3 is ATS/Xanadu.

>From this point on, I would use the name 'Xanadu' for ATS3 as this should 
make it easier
for people to locate information on ATS/Xanadu.

I have so far implemented ATS0 (ATS/Proto),  ATS1 (ATS/Geizella and 
ATS/Anairiats),
and ATS2 (ATS/Postiats). ATS/Proto and ATS/Geizella were done in OCaml and 
the others
in ATS1. I now see all of these implementations as parts of a lengthy 
programming language
experiment spanning a period of about 15 years.

But ATS3 is designed and implemented very differently. First and foremost, 
I hope that ATS3
can become a programming language suitable for use in production. For that 
to have a chance to
ever happen, we need to build an ecosystem for ATS3. ATS3 is structured in 
a way that can
greatly facilitate collaboration of contributors.

While it is still a bit too early for a release of ATS3, I feel that some 
people may be interested in
playing with the syntax of ATS3 and learning a few tricks about programming 
language implementation.
With that thought on my mind, I have just implemented a (naive) interpreter 
for ATS3. Please find the code
for this interpreter in the following repository:

https://github.com/xanadu-lang/xinterp

The basic idea is to structure xinterp as a project external to ATS/Xanadu.

After git-cloing xinterp, please also git-clone the following repo inside 
the xinterp repo:

https://github.com/xanadu-lang/xanadu

Please do not modify the code in the xanadu repo; the code in this repo is 
copied from elsewhere.
You may ask me to do the modification, though.

By studying xinterp (and possibly raising questions here), you can 
implement all kinds of tools
for processing the syntax of ATS3: syntax-highlighting, pretty-printing, 
error-messgage-reporting, etc.

Have fun!

--Hongwei

--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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/c6da8c88-92b1-4579-b9d5-136df531ee9f%40googlegroups.com.

Re: A brief update on ATS3 implementation

[gmhwxi]

Here is some code implementing the Sieve of Erastosthenes.
Note that very little type annotation is needed (due to the much stronger 
support
for type-inference in ATS3 than in ATS2)

(* ** ** *)

fun
sieve
( xs
: stream(int)) =
$lazy
(
let
val xs = $eval(xs)
in
case- xs of
|
strmcon_cons(x0, xs) =>
strmcon_cons(x0, sieve(filter(xs, x0)))
end
) (* end of [sieve] *)

and
filter(xs, x0) =
$lazy
(
let
val xs = $eval(xs)
in
case- xs of
|
strmcon_cons(x1, xs) =>
(
  if
  (x1%x0=0)
  then $eval(filter(xs, x0))
  else strmcon_cons(x1, filter(xs, x0))
)
end // end of [filter] 


   

(* ** ** *)

val
xs =
sieve(from(2)) where
{
fun
from
(n:int): stream(int) =
$lazy(strmcon_cons(n, from(n+1)))
}

(* ** ** *)

val-
strmcon_cons(x0, xs) = $eval(xs)
val-
strmcon_cons(x1, xs) = $eval(xs)
val-
strmcon_cons(x2, xs) = $eval(xs)
val-
strmcon_cons(x3, xs) = $eval(xs)
val-
strmcon_cons(x4, xs) = $eval(xs)
val-
strmcon_cons(x5, xs) = $eval(xs)

(* ** ** *)

(* end of [sieve.dats] *)



On Sunday, December 15, 2019 at 9:08:21 PM UTC-5, gmhwxi wrote:
>
>  Hi, there,
>
> I would like to make a brief announcement, telling those in this group
> about some recent progress made in the implementation of ATS3. The
> project itself is publicly accessible at the following site:
>
> https://github.com/githwxi/ATS-Xanadu
>
> Note that you need to have ATS2 installed in order to compile ATS3.
>
> So far I have essentially finished the following parts, though changes and 
> fixes
> are definitely needed for a long time to come:
>
> Part 1: Concrete syntax design + Parsing
> Part 2: Binding resolution based on static scoping
> Part 3: Type-inference + supporting for symbol overloading
> Part 4: Type-based template code selection
>
> I have also implemented a basic interpreter for testing.
>
> Compiling ATS3 to C is scheduled in the next phase. After that. advanced 
> type-checking
> (for dependent types and linear types) needs to be supported.
>
> Before starting the next phase, I plan to write some documentation and 
> hope to get more
> people on board. More on that later.
>
> 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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/8af74c75-aaa4-4c88-bfad-ce0904ba5466%40googlegroups.com.