Re: Read IO and Write IO

[Dambaev Alexander]

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
>> ```
>> 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
> 
> .
>

-- 
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/CAHjn2KwAwsdm-G_mEp5_bZHZH3t5EhaX6KkaduGqt8bAqgp3Rw%40mail.gmail.com.

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. 
>> 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: 
>>
>

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: Current Status of ATS3 (2020-11-22)

[Elijah Stone]

On Sun, 22 Nov 2020, gmhwxi wrote:

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 :)


Great to hear!


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.


What is the final vision for XATSCL0?  Will it be compiled into c?  Or 
directly into native code (via custom backend, or llvm/similar)?


What is the effect on compilation speed of having (at least) two full 
intermediate languages?



Xats2js is a functioning compiler implemented in ATS2 for translating 
XATSCML into JavaScript


JS doesn't have integers.  So how will code that uses integers be 
compiled?  Is code compiled to js is limited to 32-bit integers, since 
they can fit into the range of a double?


 -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/4594bea9-3b47-574d-d68b-2073a6f52ba7%40elronnd.net.

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

[d4v3y_5c0n3s]

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. 
> 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/c2bbf

Re: Read IO and Write IO

[Dambaev Alexander]

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/CAHjn2Kywq%3DAXmrrmjvO-T3EoJF1Yo6vuGAGo8%2BJ1VtFEoQ57mQ%40mail.gmail.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.

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

[Andreas ZUERCHER]

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 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 Go

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

[Hongwei Xi]

>>Can I guess that XATSCL0 is basically the same as the C-file that we have
now during compilation with patscc? Otherwise, what is the purpose of it?

Patscc generates code that contains goto statements. This time I would
exclude goto's in XATSCL0. In this way, compilers for ATS3 targeting other
languages can also benefit from using XATSCL0.

>>Does this mean that currently ATS3 just ignores code related to
linear/dependent types?

Yes, it ignores completely.

-- 

On Sun, Nov 22, 2020 at 11:47 PM Dambaev Alexander 
wrote:

> Glad to hear news about ATS3 implementation!
>
>
> 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.
>>
> Can I guess that XATSCL0 is basically the same as the C-file that we have
> now during compilation with patscc? Otherwise, what is the purpose of it?
>
>
>>
>> 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.
>>
> The more documentation - the better :)
>
>
>> 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.
>>
>
> Does this mean that currently ATS3 just ignores code related to
> linear/dependent types?
>
> --
> 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/CAHjn2Kxekq4Phu1%3DEFWxTVgjRm2pczK5ZsLeAy7DN%2BGzuuyA8A%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/CAPPSPLqmUjH7eLeO8iaAp0DE_Hp6RHadu%2BuKyTcLu2TPc_rq7Q%40mail.gmail.com.