Programming With Datasorts

[M88]

Hello,

I've been experimenting with datasorts as a means to compose / configure 
programs in ATS2. 

To demonstrate, I put together a small example of a static S-expression 
eDSL here .

The general approach is to a) encode a small language as a datasort b) 
implement with templates.  If additional constraints are necessary, one can 
use proofs as constructors.

I've been putting this approach to more practical use with the following 
two projects:
- atsaudio : uses datasorts 
to compose a high-performance DSP callback
- atshtml   : uses datasorts 
as HTML templates, with an option to construct verified documents with 
proofs.

(These are in early stages, and have not been thoroughly tested).

 While it may seem impractical, I noticed that implementations shrink 
pretty dramatically over time.  I also felt that it cut down on a lot of 
decisions I needed to make about interface design. 

With ATS3 on the horizon, I'm interested in seeing how static evaluation / 
metaprogramming evolve.  In part, I wrote atshtml to see how static 
constraints compare to scripted macros (like in Nim).  I could accomplish 
similar ends, though I do wish there was a way to provide plain-text errors 
when constraint-checking fails.

Best,
Mark

-- 
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/56e74300-960e-420b-99b8-a731abbc528a%40googlegroups.com.

Re: Read IO and Write IO

[M88]

This seems very versatile and flexible.

I like the idea of I/O tracking being opt-in and very specific.  I often 
find that only one type of effect is of interest, and tracking the rest can 
get in the way.  

I recently used a similar technique to track drawing to the screen (using 
an absview, "DRAWING").  This helped annotate function signatures, as well 
as provide meaningful restrictions for effects.

I do wonder how this change might affect proofs. If it's no longer possible 
to mark a function as "pure", can any function be used in a proof-function 
so long as it typechecks? 


On Thursday, August 8, 2019 at 9:24:02 AM UTC-4, gmhwxi wrote:
>
>
> Because tracking effects is no longer planned in ATS3, we need to
> think about how to handle effects incurred by calling external functions.
>
> We can introduce an abstrace linear VIEW IO:
>
> absview IO
>
> Say a function foo needs to do IO. Then it has to have a proof of the view 
> IO:
>
> fun foo(!IO | ...): ...
>
> This is just a monadic style of handing effects in Haskell.
>
> IO is so-called because there is I and O in IO. So we may also introduce
>
> absview I and O
>
> and proof functions
>
> prfun IO_split : IO -> (I, O)
> prfun IO_unsplit: (I, O) -> IO
>
> If a function only does I but no O, then it only needs a proof of the I 
> view:
>
> fun foo2 (!I | ...): ...
>
> Again, this is just a note put here as a 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/58633b60-e4fe-466e-8f84-329bc6499f30%40googlegroups.com.

Re: Issue with call-by-reference and template dispatch

[M88]

I see -- thanks.

On Wednesday, June 26, 2019 at 1:34:48 PM UTC-4, gmhwxi wrote:
>
> Right now, ATS2 cannot properly support the use of function types as 
> template
> parameters. I have no plan to fix it. Though, I expect that ATS3 be 
> implemented to
> properly handle function types as template parameters.
>
> On Wed, Jun 26, 2019 at 12:16 PM M88 > 
> wrote:
>
>>
>> This is how I get around the issue:
>>
>>
>> typedef Foo = @{
>>f = () -> void
>> }
>>
>> abstflt foo = Foo
>> extern castfn reveal ( foo ) : Foo
>> extern castfn conceal ( Foo ) : foo
>>
>> impltmp 
>> do_something( x ) =
>>let
>>   val xx = reveal ( x )
>>   var z : int = 0
>> in xx.f( z )
>>end
>>
>> implfun main0 () 
>>   = println!("Hello world")
>>   where {
>>  var ff : Foo = (@{
>>  f = lam(x) => println!(x)
>>   }) : Foo
>>
>>   val _ = do_something( conceal( ff ) )
>>
>>
>>   }
>>
>>
>>
>> I did a little bit more testing, using the following definitions for 
>> "foo".
>>
>>
>> // Case 1
>> absprop FOO
>> typedef foo = @{
>> f = (FOO | int) -> void
>> }
>> // Case 2
>> absview FOO
>> typedef foo = @{
>>f = ( FOO | int ) -> void 
>> }
>> // Case 3
>> typedef foo = @{
>>f = {l:addr}( !(int @ l) | ptr l ) -> void
>> }
>>
>>
>>
>>
>> The first two cases worked as expected, but the last one failed in the 
>> same way.  Maybe the issue is with at-views and template dispatch, 
>> specifically.
>>
>>
>> On Wednesday, June 26, 2019 at 8:13:41 AM UTC-4, Richard wrote:
>>>
>>> On Tuesday, June 25, 2019 at 9:47:50 AM UTC-4, M88 wrote: 
>>> > I noticed this a while ago in ATS2 (just verified in Temptory). 
>>> > 
>>> > 
>>> > 
>>> > It seems that call-by-reference functions in record definitions cause 
>>> issues with template dispatch. 
>>> > 
>>>
>>> From what I can tell after some testing, a type defined as a function 
>>> with call-by-reference seems to cause the same issue (even outside 
>>> records). 
>>>
>>> > 
>>> > The following will fail to compile ( no match for `do_something` ) -- 
>>> changing  the signature of `foo.f` to `(int) -> void` will compile 
>>> successfully. 
>>> > 
>>> > 
>>> > 
>>> > 
>>> > 
>>> > 
>>> > #include "share/HATS/temptory_staload_bucs320.hats" 
>>> > 
>>> > typedef foo = @{ 
>>> >   f = () -> void 
>>> > } 
>>> > 
>>> > extern 
>>> > fun {a:vtflt} do_something( a ) : void 
>>> > 
>>> > impltmp 
>>> > do_something( x ) = 
>>> >   let 
>>> >  var z : int = 0 
>>> >in x.f(z) 
>>> >end 
>>> > 
>>> > implfun main0() 
>>> >= println!("Hello [test0]") 
>>> >where { 
>>> >  var ff : foo = (@{ 
>>> >   f = lam(x) => println!(x) 
>>> > }): foo 
>>> > 
>>> >  val () = do_something(ff) 
>>> >} 
>>> > 
>>> > 
>>> > 
>>> > 
>>> > I've been using abstract types / casting as a work-around. 
>>>
>>> Could you share how you use abstract type / casting in this example to 
>>> get it to work? 
>>>
>> -- 
>> 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-lan...@googlegroups.com .
>> To post to this group, send email to ats-lan...@googlegroups.com 
>> .
>> Visit this group at https://groups.google.com/group/ats-lang-users.
>> To view this discussion on the web visit 
>> https://groups.google.com/d/msgid/ats-lang-users/8d5f8598-9955-43d8-9249-a7a5b222676d%40googlegroups.com
>>  
>> <https://groups.google.com/d/msgid/ats-lang-users/8d5f8598-9955-43d8-9249-a7a5b222676d%40googlegroups.com?utm_medium=email_source=footer>
>> .
>>
>

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/66ef1dee-cd94-4d7c-8852-ab2eb5b9b320%40googlegroups.com.

Re: Issue with call-by-reference and template dispatch

[M88]

This is how I get around the issue:


typedef Foo = @{
   f = () -> void
}

abstflt foo = Foo
extern castfn reveal ( foo ) : Foo
extern castfn conceal ( Foo ) : foo

impltmp 
do_something( x ) =
   let
  val xx = reveal ( x )
  var z : int = 0
in xx.f( z )
   end

implfun main0 () 
  = println!("Hello world")
  where {
 var ff : Foo = (@{
 f = lam(x) => println!(x)
  }) : Foo

  val _ = do_something( conceal( ff ) )


  }



I did a little bit more testing, using the following definitions for "foo".


// Case 1
absprop FOO
typedef foo = @{
f = (FOO | int) -> void
}
// Case 2
absview FOO
typedef foo = @{
   f = ( FOO | int ) -> void 
}
// Case 3
typedef foo = @{
   f = {l:addr}( !(int @ l) | ptr l ) -> void
}




The first two cases worked as expected, but the last one failed in the same 
way.  Maybe the issue is with at-views and template dispatch, specifically.


On Wednesday, June 26, 2019 at 8:13:41 AM UTC-4, Richard wrote:
>
> On Tuesday, June 25, 2019 at 9:47:50 AM UTC-4, M88 wrote: 
> > I noticed this a while ago in ATS2 (just verified in Temptory). 
> > 
> > 
> > 
> > It seems that call-by-reference functions in record definitions cause 
> issues with template dispatch. 
> > 
>
> From what I can tell after some testing, a type defined as a function with 
> call-by-reference seems to cause the same issue (even outside records). 
>
> > 
> > The following will fail to compile ( no match for `do_something` ) -- 
> changing  the signature of `foo.f` to `(int) -> void` will compile 
> successfully. 
> > 
> > 
> > 
> > 
> > 
> > 
> > #include "share/HATS/temptory_staload_bucs320.hats" 
> > 
> > typedef foo = @{ 
> >   f = () -> void 
> > } 
> > 
> > extern 
> > fun {a:vtflt} do_something( a ) : void 
> > 
> > impltmp 
> > do_something( x ) = 
> >   let 
> >  var z : int = 0 
> >in x.f(z) 
> >end 
> > 
> > implfun main0() 
> >= println!("Hello [test0]") 
> >where { 
> >  var ff : foo = (@{ 
> >   f = lam(x) => println!(x) 
> > }): foo 
> > 
> >  val () = do_something(ff) 
> >} 
> > 
> > 
> > 
> > 
> > I've been using abstract types / casting as a work-around. 
>
> Could you share how you use abstract type / casting in this example to get 
> it to work? 
>

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/8d5f8598-9955-43d8-9249-a7a5b222676d%40googlegroups.com.

Issue with call-by-reference and template dispatch

[M88]

I noticed this a while ago in ATS2 (just verified in Temptory).

It seems that call-by-reference functions in record definitions cause 
issues with template dispatch.

The following will fail to compile ( no match for `do_something` ) -- 
changing  the signature of `foo.f` to `(int) -> void` will compile 
successfully.


#include "share/HATS/temptory_staload_bucs320.hats"

typedef foo = @{
  f = () -> void
}

extern
fun {a:vtflt} do_something( a ) : void

impltmp
do_something( x ) =
  let
 var z : int = 0
   in x.f(z)
   end

implfun main0() 
   = println!("Hello [test0]") 
   where {
 var ff : foo = (@{
  f = lam(x) => println!(x)
}): foo

 val () = do_something(ff)
   }




I've been using abstract types / casting as a work-around. 

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/1a050c00-e9ff-4a44-a8cd-4b227db55d35%40googlegroups.com.

Re: libatscc: packaging

[M88]

Hi Artyom,

It's in a rather primitive state and not thoroughly tested, but feel free 
to have a look:
https://github.com/mephistopheles-8/ATS-Postiats/commit/61404adc68ffb5e1b5925cbd735bfe5ac8b5cdb9

All it really does is dump stored functions into an object. There are more 
entities that should probably be exported (eg, variables). The format of 
the object depends on the specified module.
It turns out I never got around to doing UMD, but I did IIFE, CommonJS and 
ES6.



On Tuesday, May 7, 2019 at 3:40:41 AM UTC-4, artyom.s...@gmail.com wrote:
>
> On Tuesday, May 7, 2019 at 5:58:44 AM UTC+3, M88 wrote:
>>
>>
>> Somewhat related:  maybe it would be good to have some character-sequence 
>> that represents a module accessor in the host language?
>>
>>
> Yes, it makes sense to support some form of qualified identifiers in the 
> source language. As it stands now, the ATS compiler will escape all "." and 
> other symbols, so they would have to be unmangled.
>  
>
>> For example, something like "mac#Math**sqrt" could be translated to 
>> "Math.sqrt" by atscc2[x], depending on what the module system uses for 
>> namespaces.
>>
>> From an implementation standpoint, the accessor notatiion might be a 
>> rather* bad* idea ( we'd be converting functions named 
>> "Math_052__052_sqrt" to "Math.sqrt" ).  Still, maybe there
>> are ways to make it better.
>>
>> Beyond making FFI easier, we'd also be able to package the prelude as a 
>> module in the host language, which may have benefits (integration, 
>> bundling, tree-shaking, etc) over
>> methods like concatenation.  
>>
>>
> Yes, this is precisely what I was aiming at, and note that the existing 
> translators do this (except for atscc2js, which I planned to enhance with 
> some support for ES modules). Not only do we want to package the prelude, 
> but also the code that we get via the source-to-source compilers.
>  
>
>> Just a thought
>>
>> A while ago, I had attempted to add [es6, commonjs, IIFE, UMD] module 
>> support to atscc2js.  Though it worked with a single file, I decided it had 
>> little benefit over inline code blocks if there is no [easy] way to access 
>> functions from the generated modules. 
>>
>>
> Could you post this work somewhere? I'd like to have a look.
>  
>
>>
>> On Monday, April 1, 2019 at 6:46:44 AM UTC-4, Artyom Shalkhakov wrote:
>>>
>>> Hi all,
>>>
>>> I've started work on improving atscc2js yesterday and found that we have 
>>> three similar projects:
>>>
>>>1. https://github.com/steinwaywhw/ATS-Python3
>>>2. https://github.com/bakpakin/ats-lua
>>>3. https://github.com/sazl/ats-go
>>>4. and the in-progress atscc2js
>>>
>>> Every target programming language comes with its own "prelude" (e.g. 
>>> libatscc2js for JS), but such preludes essentially implement the interfaces 
>>> defined in libatscc.
>>>
>>> Now I'm thinking that we need to package up the interface and keep it as 
>>> uniform as possible across the different targets, so that programmers may 
>>> hopefully share more code between platforms with little issues (or no issue 
>>> at all).
>>>
>>> With the above in mind, I propose to:
>>>
>>>1. package up libatscc somehow, e.g. put it on NPM (I'm working on 
>>>this, it will require only minimal changes to the existing code)
>>>2. come up with some process to maintain this 'specification' (maybe 
>>>create a github organization and put this library into a repository; let 
>>>people use issues and PRs to propose changes)
>>>
>>> Is anybody interested? If not I'll just go with the first point, and the 
>>> specification will live on in the ATS-Postiats repository (for now).
>>>
>>

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/abc2e98e-67f4-4f1a-915c-0bd57f842247%40googlegroups.com.

Re: libatscc: packaging

[M88]

Somewhat related:  maybe it would be good to have some character-sequence 
that represents a module accessor in the host language?

For example, something like "mac#Math**sqrt" could be translated to 
"Math.sqrt" by atscc2[x], depending on what the module system uses for 
namespaces.

>From an implementation standpoint, the accessor notatiion might be a rather* 
bad* idea ( we'd be converting functions named "Math_052__052_sqrt" to 
"Math.sqrt" ).  Still, maybe there
are ways to make it better.

Beyond making FFI easier, we'd also be able to package the prelude as a 
module in the host language, which may have benefits (integration, 
bundling, tree-shaking, etc) over
methods like concatenation.  

Just a thought

A while ago, I had attempted to add [es6, commonjs, IIFE, UMD] module 
support to atscc2js.  Though it worked with a single file, I decided it had 
little benefit over inline code blocks if there is no [easy] way to access 
functions from the generated modules. 


On Monday, April 1, 2019 at 6:46:44 AM UTC-4, Artyom Shalkhakov wrote:
>
> Hi all,
>
> I've started work on improving atscc2js yesterday and found that we have 
> three similar projects:
>
>1. https://github.com/steinwaywhw/ATS-Python3
>2. https://github.com/bakpakin/ats-lua
>3. https://github.com/sazl/ats-go
>4. and the in-progress atscc2js
>
> Every target programming language comes with its own "prelude" (e.g. 
> libatscc2js for JS), but such preludes essentially implement the interfaces 
> defined in libatscc.
>
> Now I'm thinking that we need to package up the interface and keep it as 
> uniform as possible across the different targets, so that programmers may 
> hopefully share more code between platforms with little issues (or no issue 
> at all).
>
> With the above in mind, I propose to:
>
>1. package up libatscc somehow, e.g. put it on NPM (I'm working on 
>this, it will require only minimal changes to the existing code)
>2. come up with some process to maintain this 'specification' (maybe 
>create a github organization and put this library into a repository; let 
>people use issues and PRs to propose changes)
>
> Is anybody interested? If not I'll just go with the first point, and the 
> specification will live on in the ATS-Postiats repository (for now).
>

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

Re: Call-by-value assignment

[M88]

The following line is problematic:
>
> prval () = $effmask_all(x := env)
>
> as assignment is definitely not a proof.
>

This looked a bit off.  I suppose in theory, one could wrap any function in 
$effmask_all and use it in proofs. 

 

> I suggest that you just do
>
> val () = x := env
>
> The compiler should allocate the same memory for both x and env.
>

in my case, this caused a C compilation error, "Invalid use of void 
expression."  Perhaps it's because VT happened to be a file descriptor.

I had supposed assignment was invalid for a call-by-value argument, but it 
would make more sense if "x" was a pointer.  Would this end up being the 
equivalent of "(*x) = env" in C?
 

> Theoretically, you could separate x into two parts: data and (linear) 
> proof;
> only move the data into env; there is no need to move the data back from 
> env
> into x since the data is non-linear. Really not worth the trouble :)
>
>
I'd tend to agree :)

Another dimension is that I would need to implement templates in terms of 
the data.  My interface is currently in terms of VT, so it would likely 
require casting from within the template implementation (or, duplicating an 
interface in terms of some data type T).  Since some functions might 
reference T in an unsafe way, it's probably the equivalent of casting.

I gave it some thought, and the two best options appeared to be:

a) Since my interface is in terms of VT, the simplest thing seemed to be 
this:
 var env = $UNSAFE.castvwtp1{VT}(x)
 val _ = some_template(env)
 prval () = $UNSAFE.cast2void(env)

b) Supposing I want to keep things nice[ish], I could create an interface 
like this:
 
   absvt@ype VT0(x:id)

   castfn vt_take( !VT(x) >> VT0(x) ) ->  VT(x)

   prfn vt_put( !VT0(x) >> VT(x), VT(x) ): void

   .
   var env = vt_take(x)
   val _ = some_template(env) 
   prval () = vt_put( x, env )

Version b seems pretty good for this case.



> On Sun, Feb 24, 2019 at 2:52 AM M88 > 
> wrote:
>
>> Hello,
>>
>> I have a viewtype and I am using it in a call-by-value function.  I want 
>> to temporarily assign it to a variable for use in a template that uses 
>> call-by-reference.
>>
>> Is there a way to assert that the variable has not been consumed? 
>>
>> Right now I am doing this, which typechecks and compiles in my case:
>>
>> extern fun {env}
>> some_template( env :  >> _ ) : void
>>
>> fun f ( x: !VT) : void = 
>> let
>>  var env = x
>>  val _ = some_template(env)
>>  prval () = $effmask_all(
>> x := env
>>   )
>> in
>>end
>>
>> Is this expected behavior?  Is it possible to write a proof function that 
>> can restore "x"? 
>>
>> ( Ultimately, x does not change, and the semantics of call-by-value seem 
>> best for this function ).
>>
>>
>>
>>
>>
>> -- 
>> You received this message because you are subscribed to the Google Groups 
>> "ats-lang-users" group.
>> To unsubscribe from this group and stop receiving emails from it, send an 
>> email to ats-lang-user...@googlegroups.com .
>> To post to this group, send email to ats-lan...@googlegroups.com 
>> .
>> Visit this group at https://groups.google.com/group/ats-lang-users.
>> To view this discussion on the web visit 
>> https://groups.google.com/d/msgid/ats-lang-users/ce57d10d-cb0a-465f-b9f6-954d7d6678cb%40googlegroups.com
>>  
>> <https://groups.google.com/d/msgid/ats-lang-users/ce57d10d-cb0a-465f-b9f6-954d7d6678cb%40googlegroups.com?utm_medium=email_source=footer>
>> .
>>
>

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/7b9e6024-d973-496e-b5b9-0c76835f3d4d%40googlegroups.com.

Call-by-value assignment

[M88]

Hello,

I have a viewtype and I am using it in a call-by-value function.  I want to 
temporarily assign it to a variable for use in a template that uses 
call-by-reference.

Is there a way to assert that the variable has not been consumed? 

Right now I am doing this, which typechecks and compiles in my case:

extern fun {env}
some_template( env :  >> _ ) : void

fun f ( x: !VT) : void = 
let
 var env = x
 val _ = some_template(env)
 prval () = $effmask_all(
x := env
  )
in
   end

Is this expected behavior?  Is it possible to write a proof function that 
can restore "x"? 

( Ultimately, x does not change, and the semantics of call-by-value seem 
best for this function ).





-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/ce57d10d-cb0a-465f-b9f6-954d7d6678cb%40googlegroups.com.

Re: Linking with abstract types

[M88]

Ah -- I was referring to atscc2js / atscc2php / atscc2py3, etc, not the 
built-in *codegen2 *feature (sorry if I was ambiguous).  If one compiles to 
separate files in say, PHP, then some of the functions that are normally 
static or inlined in C (eg, __patsfun_*) may have duplicate names, causing 
the script to crash.   In JS, it may produce some strange bugs, because 
named functions overwrite one another.  

Eg: 
// JS behavior

function foo() { console.log("foo 1") }
function bar() { foo() }
function foo () {  console.log("foo 2") }

bar();
// outputs "foo 2"  

 To avoid errors like these, it's good to use `patsopt -dd` to compile to a 
single file (which creates a unique name for each function) before sending 
the C to the code generator.  

I realize that *codegen *refers to the datcon / datcontag / fprint 
generation utility.  Again, sorry for the ambiguity.


On Friday, October 19, 2018 at 8:34:11 AM UTC-4, gmhwxi wrote:
>
> Here is one way of using codegens that I perceive:
>
> Use codegens to generate code and the generated code is
> stored in a file, say, of the name xyz.hats. Then one can do
>
> local
>
> #include xyz.hats
>
> in
>
>   [Some code that needs the content of xyz.hats]
>
> end
>
> The generated code often contains a lot of templates and usually cannot
> be typechecked separately; it needs to be put into a context to pass 
> typechecking.
>
> On Fri, Oct 19, 2018 at 6:04 AM M88 > 
> wrote:
>
>> Thanks for the responses.
>>
>> Along with the gcc optimizations, code generated in a single file (with 
>> `patsopt -dd` or `mylibies_link.hats`) tends to play more nicely with 
>> codegens, which may or may not have a notion of a "static" function like in 
>> C (making namespace collisions possible with separate compilation).  I 
>> suppose if one is using codegens, it's also more convenient to have the 
>> library in a single file (eg, for JS). 
>>
>> I will experiment with reabsimpl -- I would like to keep a single .hats 
>> file for downstream users when it's time for packaging.
>>
>> On Wednesday, October 17, 2018 at 12:53:53 AM UTC-4, M88 wrote:
>>
>>> Hello,
>>>
>>> This doesn't seem to affect compilation, but I often get this warning 
>>> when attempting to link .dats files into mylibies_link.hats:
>>> "warning(3): the static constant [] is not abstract at this point"
>>>
>>> This happens when I want to link a .dats file that implements abstract 
>>> types.  
>>>
>>> // mylibies.hats
>>> staload "./SATS/foo.sats" //expose the interface  (declares abstract 
>>> types)
>>> staload _ = "./DATS/foo.dats" // expose the templates  (implements 
>>> abstract types)
>>>
>>> // mylibies_link.hats
>>> local
>>> #include "./DATS/foo.dats"  // link the file (for non-template 
>>> functions, etc)
>>> in end
>>>
>>> It seems that all three declarations are necessary for compilation to 
>>> succeed. There is no compilation error.
>>>
>>> Is this warning safe to ignore, and/or is there a preferred way of 
>>> linking in this case?  
>>>
>>>
>>> -- 
>> You received this message because you are subscribed to the Google Groups 
>> "ats-lang-users" group.
>> To unsubscribe from this group and stop receiving emails from it, send an 
>> email to ats-lang-user...@googlegroups.com .
>> To post to this group, send email to ats-lan...@googlegroups.com 
>> .
>> Visit this group at https://groups.google.com/group/ats-lang-users.
>> To view this discussion on the web visit 
>> https://groups.google.com/d/msgid/ats-lang-users/deeccf71-2719-42eb-9c89-03a2b4e326a3%40googlegroups.com
>>  
>> <https://groups.google.com/d/msgid/ats-lang-users/deeccf71-2719-42eb-9c89-03a2b4e326a3%40googlegroups.com?utm_medium=email_source=footer>
>> .
>>
>

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/8dfc1bed-bdcb-459d-9013-5c7ac708f013%40googlegroups.com.

Re: Linking with abstract types

[M88]

Thanks for the responses.

Along with the gcc optimizations, code generated in a single file (with 
`patsopt -dd` or `mylibies_link.hats`) tends to play more nicely with 
codegens, which may or may not have a notion of a "static" function like in 
C (making namespace collisions possible with separate compilation).  I 
suppose if one is using codegens, it's also more convenient to have the 
library in a single file (eg, for JS). 

I will experiment with reabsimpl -- I would like to keep a single .hats 
file for downstream users when it's time for packaging.

On Wednesday, October 17, 2018 at 12:53:53 AM UTC-4, M88 wrote:

> Hello,
>
> This doesn't seem to affect compilation, but I often get this warning when 
> attempting to link .dats files into mylibies_link.hats:
> "warning(3): the static constant [] is not abstract at this point"
>
> This happens when I want to link a .dats file that implements abstract 
> types.  
>
> // mylibies.hats
> staload "./SATS/foo.sats" //expose the interface  (declares abstract 
> types)
> staload _ = "./DATS/foo.dats" // expose the templates  (implements 
> abstract types)
>
> // mylibies_link.hats
> local
> #include "./DATS/foo.dats"  // link the file (for non-template functions, 
> etc)
> in end
>
> It seems that all three declarations are necessary for compilation to 
> succeed. There is no compilation error.
>
> Is this warning safe to ignore, and/or is there a preferred way of linking 
> in this case?  
>
>
>

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/deeccf71-2719-42eb-9c89-03a2b4e326a3%40googlegroups.com.

Linking with abstract types

[M88]

Hello,

This doesn't seem to affect compilation, but I often get this warning when 
attempting to link .dats files into mylibies_link.hats:
"warning(3): the static constant [] is not abstract at this point"

This happens when I want to link a .dats file that implements abstract 
types.  

// mylibies.hats
staload "./SATS/foo.sats" //expose the interface  (declares abstract 
types)
staload _ = "./DATS/foo.dats" // expose the templates  (implements abstract 
types)

// mylibies_link.hats
local
#include "./DATS/foo.dats"  // link the file (for non-template functions, 
etc)
in end

It seems that all three declarations are necessary for compilation to 
succeed. There is no compilation error.

Is this warning safe to ignore, and/or is there a preferred way of linking 
in this case?  


-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/9da1f4c4-136e-4885-8e24-6dcb3e5d9aa1%40googlegroups.com.

Re: ATS3: ATS/Xanadu

[M88]

Thanks Julian,

I could see this as a possible implementation of the original templates.  
Ultimately, I would see the parser parameterized over different input / 
output types, and stack allocated variables could be different sizes, 
depending on what is being parsed.  I think templates would be necessary 
for that (or at least, convenient).  

My original suggestion has caveats (eg, binary size could explode, *maybe*).  
While I'm not sure macros are the right answer ( I chose them because it's 
syntactically valid ATS2 ), I could see the ability to compose template 
instantiations on a high level being rather useful.  

More broadly, I've been toying with the observation that, in many cases, 
implicit closure arguments are actually constants. Perhaps there are ways 
to exploit this for high-level programming.  I'm getting ahead of myself 
(it's probably frivolous just to save on a few cloref allocations), but my 
idea went something like this:

In this contrived example, let's say we wanted to curry an envless cfun, 
returning an envless cfun.  We could do this in ATS2 like so:

extern
fun {a,b,c:t@ype} curry$fopr(a,b) : c

extern
fun {a:t@ype} curry$arg() : a

extern
fun {a,b,c:t@ype} curry() :  b -> c 

implement {a,b,c}
curry () =
let
fun f1 (b) : c =
curry$fopr(curry$arg(),b) 
in f1
end


This would be difficult to actually use, in practice.  

What if it could be transformed into something like this, where cst() is a 
type specifier, requiring the value to be a top-level declaration or a 
constant literal:

extern
fun {a,b,c:t@ype} curry( cst( (a,b) -> c ) ) :  cst( cst(a) -> b -> c )

implement {a,b,c}
curry ( f ) = 
   lam( x ) => lam (y) => f(x,y) // no error about this not being envless, 
because f and x are cst()

This is more limited than closures, but still useful.  For instance, all 
envless lambda literals would be cst.  Then it'd be possible to do things 
like:

val f = curry( lam ( x: int, y : int ) : int => x + y )
val y = f(5)(2)  // returns 7

I would think that any function that accepted or returned a cst(...) value 
would need to be a template for it to work. 

I suppose implementing this idea  may not be worth it, but I thought the 
ability to instantiate templates in macros might still be nice to have.



On Friday, October 5, 2018 at 3:17:55 AM UTC-4, Julian Fondren wrote:
>
> On Thursday, October 4, 2018 at 8:47:31 PM UTC-5, M88 wrote:
>>
>> Recently I was attempting to write parser combinators without 
>> heap-allocated closures (or any sort of allocation).  It was a bit 
>> difficult because stack-allocated closures are of varying size and must be 
>> affixed to a `var`.  I did find a successful approach using templates.
>>
>
> With a linear object that includes a stack (which can avoid allocation if 
> you implement that with a fixed array) you can have code like
>
> let
> val p = new_parser(argv[1])
> fun parseHello(p: !parser_vt): void = parse(p, "hello")
> fun parseQuery(p: !parser_vt): void = parse(p, "what day of the month is 
> it?")
> fun parseAcceptable(p: !parser_vt): void = (
> push(p); parseHello(p);
> if failed(p) then (
> pop(p); parseQuery(p);
> ) else commit(p)
> )
> in
> parseAcceptable(p);
> if isdone(p) then
> println!("Hi, it's the first of the month.");
> free_parser(p);
> end
>
>
> In general, think of linear objects when you're looking at some pretty 
> do-notation, from how purely functional languages with uniqueness types do 
> I/O. 
>
>
> The local-function-: transformation (turning apparently 
> closed-over variables into implicit parameters) will try to consume your 
> linear variables, so you can't easily do without those p arguments. That 
> same transformation could be used though if you kept your state in mutable 
> local variables, which might not be so bad if you #include the : 
> functions into your let-declaration from a .hats file with stuff like:
>
> fun parse(str: string): void = (
> if !reading then (
> if is_prefix(str, input, !input$at) then
> !input$at := !input$at + strlen(str)
> else
> !reading := false
> )
> )
>
>
> It went a little something like:
>>
>> implement parse_token$tok<>() = "this"
>> val THIS = parse_token<>
>> implement parse_token$tok<>() = "that"
>> val THAT = parse_token<>
>>
>> implement parse_or$p1(str,tup) = THIS(str,tup)
>> implement parse_or$p2(str,tup) = THAT(str,tup)
>> val THIS_or_THAT = parse_or
>>
>> It would be nice if something like this were possible:
>

Re: ATS3: ATS/Xanadu

[M88]

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

Recently I was attempting to write parser combinators without 
heap-allocated closures (or any sort of allocation).  It was a bit 
difficult because stack-allocated closures are of varying size and must be 
affixed to a `var`.  I did find a successful approach using templates.

It went a little something like:

implement parse_token$tok<>() = "this"
val THIS = parse_token<>
implement parse_token$tok<>() = "that"
val THAT = parse_token<>

implement parse_or$p1(str,tup) = THIS(str,tup)
implement parse_or$p2(str,tup) = THAT(str,tup)
val THIS_or_THAT = parse_or

It would be nice if something like this were possible:

macdef token(str) = let
   implement parse_token$tok<>() = ,(str)
   in parse_token<>
   end

macdef ||(p1,p2) = let
   implement parse_or$p1(str,tup) = ,(p1)(str,tup)
   implement parse_or$p2(str,tup) = ,(p2)(str,tup)
in parse_or
end

val this_or_that = token("this") || token("that")  // returns a constant 
cfun.

This probably only makes sense in the domain of embedded programming 
(otherwise closures could be used). 



On Friday, February 9, 2018 at 1:15:22 PM UTC-5, gmhwxi wrote:
>
> For the moment, I just want to open a thread for ATS3.
>
> I decided to pick ATS/Xanadu for the full project name. I like the name 
> Xanadu
> because it is poetic and brings a feel of exoticness.
>
> ATS3 is supposed to be compiled to ATS2. At least at the beginning. I will 
> try to
> write more about what I have in mind regarding ATS3.
>
> I know that a lot of people have been complaining about the syntax of 
> ATS2. So
> we can start the effort of designing some "nice" syntax for ATS3. Please 
> feel free
> to post here if you would like share your opinions and ideas.
>
> I will be happy to take the lead but we definitely need to have some form 
> of community
> effort on this project given its size and scope.
>
> Cheers!
>
> --Hongwei
>
> PS: I felt rushed every time up to now when implementing ATS. This time I 
> am hoping
> to have the luxury of thinking about implementation a bit before actually 
> doing it :)
>
>

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/7674f7d9-a788-4296-b413-ee8f58f9aed5%40googlegroups.com.

Re: Initializing statically-allocated arrays within templates

[M88]

Scoped includes and constants  areawesome.

On Tuesday, September 25, 2018 at 3:28:05 PM UTC-4, M88 wrote:
>
> Hello,
>
> I was wondering if it's possible to use a template to define the size of a 
> statically allocated array in a template.
>
> An example (that won't compile) is:
>
> extern
> fun {a:t@ype} example () : void
>
> extern
> val {} example$bufsz  : [n:pos] size_t n
>
> implement {a}
> example () =
> let
>   val sz = example$bufsz<>
>   var buf = @[a?][sz]()
> in
> end
>
> Is it possible to define example$bufsz<> as a constant with late-binding?  
> I suppose behavior like sizeof would be ideal, but that seems to be 
> internal.
>
> Thanks,
> -M
>
>
>
>

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/6450c0ad-f253-4766-9c5e-aa05232c2f8b%40googlegroups.com.

Re: Initializing statically-allocated arrays within templates

[M88]

I get an error during C compilation, ATSERRORarrdim_unknown, when I try to 
use a template function.

Thanks Julian -- that's a decent solution.


On Tuesday, September 25, 2018 at 3:28:05 PM UTC-4, M88 wrote:
>
> Hello,
>
> I was wondering if it's possible to use a template to define the size of a 
> statically allocated array in a template.
>
> An example (that won't compile) is:
>
> extern
> fun {a:t@ype} example () : void
>
> extern
> val {} example$bufsz  : [n:pos] size_t n
>
> implement {a}
> example () =
> let
>   val sz = example$bufsz<>
>   var buf = @[a?][sz]()
> in
> end
>
> Is it possible to define example$bufsz<> as a constant with late-binding?  
> I suppose behavior like sizeof would be ideal, but that seems to be 
> internal.
>
> Thanks,
> -M
>
>
>
>

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/e22b9c5c-9617-4f4b-b1dd-814642198192%40googlegroups.com.

Initializing statically-allocated arrays within templates

[M88]

Hello,

I was wondering if it's possible to use a template to define the size of a 
statically allocated array in a template.

An example (that won't compile) is:

extern
fun {a:t@ype} example () : void

extern
val {} example$bufsz  : [n:pos] size_t n

implement {a}
example () =
let
  val sz = example$bufsz<>
  var buf = @[a?][sz]()
in
end

Is it possible to define example$bufsz<> as a constant with late-binding?  
I suppose behavior like sizeof would be ideal, but that seems to be 
internal.

Thanks,
-M



-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/b5bd37d6-cfe7-4a30-a956-b8aada50a005%40googlegroups.com.

Re: ATS3: ATS/Xanadu

[M88]

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

Original:
datasort tlist = tnil
| tcons of (t0ype, tlist)

extern fun {t:tlist} foo(): void
extern fun {a:t0ype} foo$fopr(): void

implement foo() = ()
implement(a,ts) foo() = {
  val () = foo$fopr()
  val () = foo()
  val () = ignoret (1)
}

implement main0 () = let
  implement foo$fopr() = println!("int")
  implement foo$fopr() = println!("string")
  implement foo$fopr() = println!("bool")
  val () = println!("test 1: should print int, string")
  val () = foo()
  val () = println!("test 2: should print bool, int")
  val () = foo()
in


Example:


datasort tlist = tnil
| tcons of (type, tlist)

extern 
   fun {t:tlist} foo(): void
   fun {a:type} foo$fopr(): void

impl 
foo() = ()

(a,ts) foo() = {
   val 
  () = foo$fopr()
  () = foo()
  
 }

main0 () = 
  let
 impl 
foo$fopr() = println!("int")
foo$fopr() = println!("string")
foo$fopr() = println!("bool")
 val 
() = println!("test 1: should print int, string")
() = foo()
() = println!("test 2: should print bool, int")
() = foo()
 in ()

I guess the good thing here is that it's 99% ATS2.  Of course, there are 
likely plenty of issues, including whitespace-significance (I was hesitant 
to post something this concrete). 

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/7a7e5e9d-5267-4499-9ebf-9ea51aeb2212%40googlegroups.com.

Re: Defining constraints -- datasorts and stacst

[M88]

> It seems that isCA1_praxi should be declared
> as follows:
>
> praxi
> isCA1_praxi{cb:catB} (): [isCA1(sA_1(cA_1,cb))] void
>

Yes, this makes sense -- I am looking for universal quantification.

I suppose the issue here is how it would be invoked.  Would I
still need to invoke the proof as follows?

prval () = isCA1_praxi{cB_1}()
prval () = isCA1_praxi{cB_2}()
prval () = isCA1_praxi{cB_3}()



After giving this some thought, I realized I could invoke the proof
within a constructor, omitting the need to explicitly specify each "catB." 
  

fun makeCA1 {cb:catB}() : [sa:sortA | isCA1(sa) ] typeA(sa)

What tripped me up at first is that the return value of each constructor
should specify the constraint "isCA1" if I use this approach, whereas
the former let me invoke the proofs globally.


On Saturday, April 7, 2018 at 12:25:05 AM UTC-4, M88 wrote:
>>
>>
>> I was looking into the rock-paper-scissors example (here 
>> <https://groups.google.com/forum/#!topic/ats-lang-users/YcdEzhJdJzs> and 
>> here 
>> <https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST20/test25.dats>)
>>  
>> and I found it very useful for learning how to define  predicates in the 
>> statics.
>>
>> I had made an attempt something similar, but using independent datasorts 
>> as parameters. 
>>
>> For example:
>>
>> datasort catA =
>>| cA_1
>>| cA_2
>>| cA_3
>>
>> datasort catB =
>>| cB_1
>>| cB_2
>>| cB_3
>>
>> datasort sortA =
>>| sA_1 of (catA, catB)
>>| sA_2
>>| sA_3
>>
>> // only sortA is used to define types. Eg,
>> abst@ype typeA(sortA)
>>
>> I ran into a few issues.  I arrived at a solution, but I thought it could 
>> be cleaner.
>>
>> First, I discovered that I wasn't  able to define equalities with 
>> datasorts.  Eg, {sa:sortA | sa == sA_2}.  It would typecheck, but the 
>> constraints could not be solved. I suppose this makes sense, considering 
>> the definition of ==.  Does ATS supply a way to determine equalities on 
>> datasorts?  Is there another feature that would make this unnecessary?
>>
>> As an alternative, I decided to declare a static predicate, as in the 
>> rock-paper-scissors example:
>>
>> stacst isCA1 : sortA -> bool
>>
>> // This works, but becomes quite verbose.
>> praxi isCA1_praxi ():
>>[
>>   isCA1(sA_1(cA_1,cB_1)) &&
>>   isCA1(sA_1(cA_1,cB_2)) &&
>>   isCA1(sA_1(cA_1,cB_3))
>>] void
>>
>> The verbosity isn't an issue in this example, but becomes pretty 
>> unmanageable as the relationships get more complex. I would like to say, 
>> "for any catB".  I tried using universal and existential quantification, 
>> but the constraints would not solve.  I would like to avoid passing catB 
>> explicitly. 
>>
>> Is there a  way to reduce it to something like this:
>>
>> // The constraints will not solve:
>> praxi isCA1_praxi ():
>>[ cb: catB |
>>   isCA1(sA_1(cA_1,cb)) 
>>] void
>>
>> Perhaps I am abusing datasorts -- suggestions for other approaches are 
>> 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 post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/68469c62-1ab0-4d0c-936b-e8775877b5f3%40googlegroups.com.

Defining constraints -- datasorts and stacst

[M88]

I was looking into the rock-paper-scissors example (here 
 and 
here 
)
 
and I found it very useful for learning how to define  predicates in the 
statics.

I had made an attempt something similar, but using independent datasorts as 
parameters. 

For example:

datasort catA =
   | cA_1
   | cA_2
   | cA_3

datasort catB =
   | cB_1
   | cB_2
   | cB_3

datasort sortA =
   | sA_1 of (catA, catB)
   | sA_2
   | sA_3

// only sortA is used to define types. Eg,
abst@ype typeA(sortA)

I ran into a few issues.  I arrived at a solution, but I thought it could 
be cleaner.

First, I discovered that I wasn't  able to define equalities with 
datasorts.  Eg, {sa:sortA | sa == sA_2}.  It would typecheck, but the 
constraints could not be solved. I suppose this makes sense, considering 
the definition of ==.  Does ATS supply a way to determine equalities on 
datasorts?  Is there another feature that would make this unnecessary?

As an alternative, I decided to declare a static predicate, as in the 
rock-paper-scissors example:

stacst isCA1 : sortA -> bool

// This works, but becomes quite verbose.
praxi isCA1_praxi ():
   [
  isCA1(sA_1(cA_1,cB_1)) &&
  isCA1(sA_1(cA_1,cB_2)) &&
  isCA1(sA_1(cA_1,cB_3))
   ] void

The verbosity isn't an issue in this example, but becomes pretty 
unmanageable as the relationships get more complex. I would like to say, 
"for any catB".  I tried using universal and existential quantification, 
but the constraints would not solve.  I would like to avoid passing catB 
explicitly. 

Is there a  way to reduce it to something like this:

// The constraints will not solve:
praxi isCA1_praxi ():
   [ cb: catB |
  isCA1(sA_1(cA_1,cb)) 
   ] void

Perhaps I am abusing datasorts -- suggestions for other approaches are 
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 post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/2aa9d070-e9bb-461d-974e-c0bb3ecb6ce5%40googlegroups.com.

staload, paths, and infix operators

[M88]

I have two questions...

The first is that path resolution seems to have changed from ATS2 0.3.7 and 
0.3.9.
I used to be able to write 'staload "sats/foo.sats"' in "dats/foo.dats" 
and running patscc from the project root would find the file.  Now it seems 
I need to
write 'staload "./../sats/foo.sats"'.   Did this actually change, or am I 
missing something?
Strangely, -IATS with the project root doesn't seem to be working for me 
either -- at least with patscc.  
I've tried both relative and absolute paths.

The second is that infix operators consisting of non-alpha symbols (eg, 
'|>') are not imported
from .sats files during staload.  I can declare them in .dats files.  Would 
I need to
#include these if I chose to share them between files?

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/abc22b94-a2d6-4205-9647-b8c5b7ada745%40googlegroups.com.

Re: ATS3: ATS/Xanadu

[M88]

> I thought about this issue as well. One idea I had is to
> use overloading aggressively.
>

A thought I had recently -- I'm almost wondering if certain proofs (eg, 
linear proofs) could behave more like value constraints.  That is, they 
could be invoked optionally, and would only be checked when specified.  For 
example, if a variable invoked with type "b" is linear, it could be passed 
to either function  "fun foo ( linear(l) | b l )" or "fn foo ( b )"  
without error.  I suppose it would also be interesting if general proofs 
could be specified in type declarations -- again, analogously to value 
constraints.   I suppose this suggestion would almost imply a "dataprop 
table" associated with every val / var invoked, which may or may not be 
feasible 

Speaking of constraints, one thing ATS2 doesn't have are "implementation 
constraints" -- that is, something like typeclasses or traits.  I see how 
specific templates capture 85-90% of the functionality, and honestly I 
don't often miss the former.  Still, such constructs are useful for 
documenting certain dependencies within code (they tell a developer "Hey, 
for this to work for your type, go implement that template" ).  This type 
of thing introduces a structured overloading that might reduce the number 
of tokens in the code a fair bit, too.  

Right now the biggest issue with ATS2, as I see is, is that a non-expert
> user gets tripped everywhere. For such a user, programming in ATS can 
> hardly
> be an enjoyable experience. ATS3 tries to put joy back into learning 
> functional
> programming via ATS. 
>

I found the conceptual core of ATS2 pretty easy to grasp, given the 
examples and the *Introduction to ATS. *The difficult part was finding the 
meaning of certain tokens in source code, or even discovering that a 
certain feature exists in the first place.  Also, I suppose I'm about as 
efficient at ATS2 as I am with C -- it can be difficult to justify using 
ATS instead of C (especially when I have to write FFI to C anyway, though 
c2ats has proven quite useful).   I think ATS2 with relatively minor 
usability enhancements would tip my preference more strongly in its favor 
-- better error messages, some information hiding (I guess, syntactic 
sugar) and perhaps H/M inference alone could go a long way.
 

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/282bc6ea-ebe5-4e86-9b64-1f7db11c7b45%40googlegroups.com.

ATS3: ATS/Xanadu

[M88]

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

Maybe this could extend to other types that have a dual linear version (eg 
strptr / string). It seems there are commonly functions that could operate on 
either, and at the moment this is achieved by casting. Perhaps there could be a 
type level attribute for all pointer-based types, like "lin string" / "gc 
string" , which are both also just "string". 

This may also allow for specifying "linearity" in variable declarations, eg 
'let lin val x=Foo(7), y="A linear string" in... '. 

I suppose a similar syntax could make dealing with proof values more concise, 
too (eg, 'let prf val pa=my_proof_fn(), pb=another_proof_fn(pa) in... '). 

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/c5467efb-603a-4635-a3c7-d4f3840e7165%40googlegroups.com.

Re: ATS3: ATS/Xanadu

[M88]

I have accrued a bit of a wishlist while working with ATS.   Maybe some of 
it is useful or feasible.

Things I would keep the same:

   - I think dependent type / proof syntax is well done, and it feels a bit 
   more natural than Idris.  I'd keep this the same
   - The '~' to free an unfolded view type is a good choice. 
   - I'm also fond of '@' for unboxed types.
   - I like the degree to which it resembles SML. 
   - I like the various language backends.  The JS backend is especially 
   important, I think
   
I really like Idris and Haskell, though maybe SML-like syntax offers more 
flexibility (eg, defining different types of functions).  For 
resource-awareness, distinguishing between C-like lambdas and closures is 
excellent.  Then again, I don't miss the "fun" while working with Haskell 
or Idris. 

One good thing about Idris is that it's somewhat easy to target native / 
JS, and unofficially, the JVM.  A bit odd that the JS backend can be faster 
than the native at times.

Haskell is horrendous to cross-compile, and GHCJS program sizes are 
massive.  I love it for basic native compilation, though.

I think ATS could have a slight edge in the sense of portability -- the JS 
it outputs is tiny and it's dead-simple to cross-compile.   That said, I 
can't integrate the JS very easily into a standard JS toolchain, since it 
doesn't output modules.


Here are syntactic things I think ATS would benefit from:


   - Active whitespace would be a great alternative to "end", and might add 
   some elegance
   - Templates need to be better distinguished from dependent types.
   - As mentioned already, I dislike the '@' signs in types (eg, t@ype).  
   Aliasing also becomes very confusing (it took me a while to figure out what 
   t0p meant, or t0ype for that matter)
   - I found numeric suffixes similarly problematic -- clo1, for instance.  
   The number gives no indication about what the name may mean. 
   - List literals would be awesome in some capacity (eg, ["this", "is", 
   "a", "list"]).  I guess it may be hard to distinguish between types of 
   lists, but I do think $list / $list_v is a bit too verbose.
   - $FOO reads like a shell variable.  Nixing the dollar sign next to 
   modules may be a good choice.
   - I think C might be best banished to .cats files.  Or, maybe the inline 
   code blocks could be assigned a language (eg, %C{  ... %})
   - Multiline strings are useful in any language.
 
   
Technical things I think ATS could use:


   - Some lightweight concurrency primitives would be great -- nothing that 
   would require a runtime, but maybe something to schedule things like green 
   threads.
   - Clearer error messages, ideally aware of the C compilation phase.  C 
   errors can be confusing whenI'm not working in C.
   - Odds and ends -- a build / package manager might be useful. 
   - Lazy "val" might be nice -- like Haskell's "let". 
   - The JS backend is great, but it would help to output modules. ES6 
   would be a fine choice for this, I think.  Node will catch up eventually, 
   and in the meantime, there are tools like Rollup, etc.
   - Possibly, row types?
   

One thing I liked about ATS is that I could port the same library to 
multiple language targets simply by swapping out .hats and .cats files. I 
had attempted to build a web framework / HTML DSL on this principle (though 
time isn't on my side).  I felt that some of my Makefile trickery could be 
better managed by a smart build tool, that knows the library and the 
language targets (C for the server and JS for the client), for example.  I 
don't think it needs to be particularly complex, but there would need to be 
some conventions for directory structure and organization of .cats files in 
different languages.


-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/06909163-6217-437e-b92c-bdaa7c96cf64%40googlegroups.com.

Re: Controlling the allocation / deallocation rates when using datatypes

[M88]

Thank you -- the rewrite was informative, and the most efficient so far. 

I overlooked the fact that a datatype is a pointer to an unboxed tuple.  It 
should make it possible to statically allocate them, if I wanted to.

It looks like there are several options here.

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/e4a061a0-f6e6-4488-b837-0c561cdc990c%40googlegroups.com.

Re: Controlling the allocation / deallocation rates when using datatypes

[M88]

> It is unclear what you translated. Could you show?


I was just saying that I didn't expect the compiler to treat stream-fusion 
the same way in ATS as it does in Haskell. To your point, I expected 
different algorithms.

I found the tutorial useful -- implementing a custom allocation routine was 
easier than I expected it to be. I managed to get the version with 
datavtypes to run as quickly as the stack version (eg, ~12ms).   I need to 
refine it a bit more, but that's the start I was looking for.

I would be interested in seeing an implementation of a). I attached the 
original datavtype version of the code I was using to test.  This is a toy 
program that creates a stream and prints the final value.

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/644579cc-b9bf-4b03-a5f7-9736bcf024f2%40googlegroups.com.


ode_test_linear1.dats
Description: Binary data

Controlling the allocation / deallocation rates when using datatypes

[M88]

Hello,

I just started dabbling with ATS, so bear with me.

I really like using datatypes / datavtypes as a control structure, but the 
allocation / deallocation rates seem fairly high when there are a fair 
number created in sequence.   

I suppose I've gotten used to the stream-fusion motif in Haskell.  I'm 
aware of the caveats of directly translating from one language to another 
(eg, optimizations like stream-fusion may not hold, nor are they necessary, 
per se), but I like the idea of the enum-based  state machine.  For example:

datatype Step (s:t@ype, a:t@ype) =
  | Yield of (s,a)
  | Step of (s)
  | Done

When I do something like, say, generate 100 of these guys, my 
allocation / deallocation rates are pretty high, and I suspect it's 
impacting performance (eg, relative performance with -O2: a stack-only 
version with unboxed tuple "Step" runs in 11ms, a datavtype version runs in 
closer to 35ms, getting 44ms-60ms with GC and datatypes, while a naive shot 
in Haskell runs in 9ms). 

I could use something like this, but it is much less elegant (this is how I 
implemented the stack-only version):

datatype StepType =
| Yield
| Skip
| Done


typedef Step (s:t@ype, a:t@ype) = @(StepType,s,a)

I'm wondering if it's possible to do any of the following (or if ATS might 
already be doing it for me):

a.) Statically allocate a single variable of a given datatype, and/or 
create the datatype at a specific memory location
b) Define an initial heap size that stays constant throughout the lifetime 
of a program, so that transient entities like the ones above consistently 
re-use the same memory pool.

I think I could probably conjure up something like the latter using custom 
allocation functions (eg, DATS_MEMALLOC_USER), but I thought I would reach 
out first...

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/c2fc9fa1-3742-4b23-938c-081579066a89%40googlegroups.com.