Hi,
I recently came across glot.io, an online service that lets you run and
share snippets. It is open source, so I took the opportunity to add support
for our ATS programming language. They use docker image to run ATS code,
and the image I provide contains not only ATS, but also erlang/elixir
Sure, but where can I find the source file for the logo?
On Saturday, May 7, 2016 at 5:28:38 PM UTC-4, gmhwxi wrote:
>
> Could you also make ATS logo shown in the entry for ATS?
>
> On Saturday, May 7, 2016 at 2:18:45 PM UTC-4, Steinway Wu wrote:
>>
>> Hi,
>>
>
Sure, it is merged. It will be published in the next deployment.
On Monday, May 9, 2016 at 9:57:03 AM UTC-4, gmhwxi wrote:
>
> It is here:
>
>
> https://github.com/githwxi/ATS-Postiats/blob/master/doc/PROJECT/MEDIUM/ats2langweb/theLogo/theLogo.png
>
> On Mon, May 9, 2016 at
This is cool!
On Sunday, May 22, 2016 at 12:24:21 AM UTC-4, gmhwxi wrote:
>
>
> ATS2 now supports ifcase-expressions, which are similar to
> the if-expressions in Erlang. Here is an example:
>
> //
> fun
> acker
> {m,n:nat}
> ..
> (
> m: int(m)
> , n: int(n)
> ) : intGte(0) =
> (
> ifcase
> | m
Hi, I just created a tag wiki for ATS on stackoverflow, in case anyone post
relevant questions there.
http://stackoverflow.com/tags/ats/info
--
You received this message because you are subscribed to the Google Groups
"ats-lang-users" group.
To unsubscribe from this group and stop receiving e
This is so cool!
On Wednesday, June 29, 2016 at 1:24:12 PM UTC-4, gmhwxi wrote:
>
>
> In ATS2-0.2.8, a static constant can now be declared with an external name:
>
> For instance:
>
> stacst sine_of_real : real -> real = "ext#sin"
>
> This is useful when constraints generated during typechecking a
Hi,
In a practice, I encountered a problem of memorizing functions. Given a
function `f`, a memorized version of `f`, called `memo f` should cache the
results of `f` applying on some `input`. I tried a demo here
https://glot.io/snippets/egflakau5h, which shows a generic implementation
of the
Thanks, I forgot to save it after debug. Now it works.
On Sunday, July 10, 2016 at 9:38:49 PM UTC-4, gmhwxi wrote:
>
> Please change
>
> memo1
>
> to
>
> memo1
>
> Also, please delete the line "staload .../gorder_int.dats"
>
> On Sunday, July 1
Hi,
In `stream_vt.dats`, I saw the following snippets,
fun {a:vt0p} {b:vt0p} stream_vt_map_con (xs: stream_vt (a)) : stream_vt_con
(b) = let
val xs_con = !xs
in
case+ xs_con of
| @stream_vt_cons(x, xs) => let
val y = stream_vt_map$fopr (x) // fopr is of type {a,b:vt@ype}
&a
Hi friends,
I'm thinking about moving Google Group to a self-hosted Discourse.
Discourse is an online discussion kit, http://www.discourse.org, very much
like a forum version of Stack Overflow. It's founded by the founder of
StackOverflow.
I think it is beneficial for several reasons.
1.
tion
> in ATS is to use call-by-reference when linear data is handled.
>
> 3. The 'xs' on the right-hand side is a variable (with address); its
> content needs to be taken out before free@ can be called.
>
>
>
>
> On Thu, Jul 14, 2016 at 9:20 AM, Stei
I'm a little confused. This is solved using z3, not using dReal, right? So
what's the relation with dReal/dReach here?
On Monday, June 13, 2016 at 6:08:13 PM UTC-4, gmhwxi wrote:
>
> The directory is renamed as follows:
>
>
> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/
hope is that dReal can be used to solve such constraints effectively
> in practice.
>
> On Saturday, July 16, 2016 at 11:53:42 PM UTC-4, Steinway Wu wrote:
>>
>> I'm a little confused. This is solved using z3, not using dReal, right?
>> So what's the relation
Hi, @Hongwei
I received an ad from StackOverflow, introducing their "Documentation"
feature in beta, here http://stackoverflow.com/tour/documentation. It seems
useful for us, too. You can have a look.
It needs at least five requests for the #ats tag to allow us to create
documents. Anyone int
Neat!
On Monday, July 25, 2016 at 12:58:55 PM UTC-4, gmhwxi wrote:
>
>
> I am thinking about building some on-line services for easing the
> use of the ATS programming language system. For the moment,
> I managed to finish one that supports syntax-hiliting for ATS code:
>
> http://www.ats-lang.org
Hi,
Following up on Hongwei's *ats-as-a-service*, I wrote a pandoc plugin for
automating some of the tasks of writing interactive ats tutorials, shown
here https://steinwaywhw.github.io/ats-tutorials/. If you a familiar with
pandoc, then my small script is just a pandoc filter in python, that
UTC-4, Steinway Wu wrote:
>
> Hi,
>
> Following up on Hongwei's *ats-as-a-service*, I wrote a pandoc plugin for
> automating some of the tasks of writing interactive ats tutorials, shown
> here https://steinwaywhw.github.io/ats-tutorials/. If you a familiar with
> pandoc,
Hi,
When I define an exception in SATS file `exn.sats`, I need to compile it
like `patscc *.dats *exn.sats*` to have the symbol defined. However, when I
define a normal datatype in some sats file, I usually can compile it by
indicating only those DATS files, like `patscc *.dats`. Why are they
Hi,
I'm trying to implement `gcompare_val_val` for a datatype `list`, but
encounters an error saying "some disallowed effects may be incurred: 1"
```
datatype list (a:t@ype) = ...
fun {a:t@ype} list_compare ...
implement (a) gcompare_val_val (x, y) = list_compare (x, y)
```
What is that effe
Hi,
Is it possible to do overloadings like below?
```
fun {a:t@ype} gcomapre_val_val (a, a): int
symintr compare
overload compare with gcompare_val_val
overload compare with gcompare_val_val
```
I'm asking this since this. Say, we have a dummy `mycompare`
```
fun {a:t@ype} mycompare (a, a):
$effmask_all( list_compare
> (x, y) )
>
>
>
> On Thu, Aug 11, 2016 at 2:03 PM, Steinway Wu <> wrote:
>
>> Hi,
>>
>> I'm trying to implement `gcompare_val_val` for a datatype `list`, but
>> encounters an error saying "some disallowed effec
I saw
this, https://bluishcoder.co.nz/2011/10/19/overloading-functions-in-ats.html,
which describes the same thing I would like to do. But those examples no
longer work.
On Friday, August 12, 2016 at 12:13:12 PM UTC-4, Steinway Wu wrote:
>
> Hi,
>
> Is it possible to do overl
Black magic... Why does it work?
On Friday, August 12, 2016 at 6:09:40 PM UTC-4, gmhwxi wrote:
>
> Try:
>
>
> fun{a:t@ype}
>
> mycompare(INV(a), a): int
>
>
> Sent from my T-Mobile 4G LTE device
>
>
> ------ Original message--
>
> *From: *Stein
Great job!
On Tuesday, August 16, 2016 at 3:58:28 AM UTC-4, Artyom Shalkhakov wrote:
>
> On Tuesday, August 16, 2016 at 11:15:51 AM UTC+6, gmhwxi wrote:
>>
>> This is great news!
>>
>> I really want to try it for my upcoming class.
>>
>> Could you show me how to use the Monaco editor to
>> replac
Hi,
I was reading a chapter about type inference and constraint solving in ML.
It mentioned a quick Union/Find algorithm for testing equivalent classes. I
translate the code into ATS, and pasted here at [glot.io: Union/Find](
https://glot.io/snippets/eiaoq3icf1)
Just for fun.
--
Steinway Wu
Updated, thanks!
On Friday, September 9, 2016 at 7:07:55 PM UTC-4, gmhwxi wrote:
>
>
> I suggest:
>
> fun{} addr_of{a:t@ype} (pt a): ptr
>
> Casting a pointer(64bit) to an integer(32bit) is a bit dangerous.
>
>
> On Friday, September 9, 2016 at 5:36:35 PM UTC-
Just share a link from hacker news, a lisp machine.
http://www.technoblogy.com/show?1GX1
--
Steinway Wu
Sent with Airmail
--
You received this message because you are subscribed to the Google Groups
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emai
Hi,
https://gist.github.com/steinwaywhw/27d8fbb569cf178d08d9465aa92c741e
I’m sharing my SublimeText script for building/typechecking ATS files.
After loading this plugin, and filling the blanks, press the hotkey for
Build (on mac, it is cmd+b/cmd+shift+b), it will compile/typecheck the
program.
yes... but not a big issue though. hope we could have more people
interested in ATS and ask questions there.
On Sunday, October 16, 2016 at 7:02:43 AM UTC-4, Kiwamu Okabe wrote:
>
> On Sun, Oct 16, 2016 at 3:20 AM, gmhwxi wrote:
> > http://stackoverflow.com/tags/ats/info
>
> I think the "ats"
I didn't know Join-calculus before, but this definitely looks interesting
to me. It seems that it can encode pi-calculus to some degree, but I
haven't fully investigate that paper. But just for your information, ATS
supports session types which I think is relevant here. You may want to have
a l
Since you already have some experience with JoCaml, would you mind sharing
some code examples, or slides that you have? I would like to learn more
about it.
On Wednesday, December 21, 2016 at 4:23:57 PM UTC-5, Ian MathWiz wrote:
>
> I've seen some other feature/roadmap ideas on this list, so I
I just played with it on my ats-utils package. I published it
here, https://www.npmjs.com/package/ats-utils so that others can try out.
It is under MIT license.
On Tuesday, January 3, 2017 at 2:45:09 PM UTC-5, gmhwxi wrote:
>
>
>
> ##
> #
> # For the moment, I am using ats-lang-users for at
It seems that the change breaks the build of ATS-Postiats-contrib. I can no
longer compile atscc2js/2erl/2clj etc. It can not find source files any
more and reporting errors like ".PATSRELOCROOT-$USER/SATS/json.sats is not
available".
On Tuesday, January 3, 2017 at 2:45:09 PM UTC-5, gmhwxi wro
Great note!
On Thursday, March 16, 2017 at 11:20:54 AM UTC-4, August Alm wrote:
>
> Hi all!
>
> I just wrote down some sketchy thoughts on monads and comonads in ATS. ATS
> has a very unique type system, so there are (co)monads in ATS that simply
> do not exist in other languages. I'm wondering
Hey friends,
I just came across this,
https://github.com/jgm/skylighting/blob/master/xml/ats.xml, when I was
writing a latex documents indirectly by using markdown/pandoc. I found that
Pandoc natively supports ATS syntax highlighting, which generates pretty
LaTex/PDF files. That's AMAZING! I
't tell anyone. Have it spring up from an unrelated
> source. You just made my day, thanks, Kiwamu. :)
>
>
>>
>> On Apr 18, 2017 7:45 AM, "gmhwxi" wrote:
>>
>>> author="Kiwamu Okabe (...)"
>>>
>>> On Monday, Apr
I encountered a problem.
Say I have this in the ATS code
stacst set_emp: set = "ext@smt_set_emp"
and this in the smt2 code
(define-const smt_set_emp (Set) ((as const (Set)) false))
`--constraint-export` is able to translate all static applications of
`smt_emp` to `smt_set_emp`.
*However, it
I put up a PR for your
consideration. https://github.com/githwxi/ATS-Postiats/pull/170
On Tuesday, July 4, 2017 at 2:47:15 PM UTC-4, Steinway Wu wrote:
>
> I encountered a problem.
>
> Say I have this in the ATS code
>
> stacst set_emp: set = "ext@smt_set_emp"
&
Hi Aditya,
Great talk! You did a great job presenting a difficult system in a
easy-to-understand way :)
Just wanna point out a detail. Proofs are dynamic terms (of sort "prop").
So they are not really "type-level". But I guess it is ok to say
"type-level" in the talk since they will be erased
Hi Aditya,
Your talk is also featured on *The Verge*! Congratulations!
https://www.theverge.com/2017/10/2/16404152/strange-loop-2017-programming-talks-youtube
On Monday, October 2, 2017 at 3:02:03 AM UTC-4, Artyom Shalkhakov wrote:
>
> Seen on reddit:
>
>
> https://www.reddit.com/r/programming
I guess you can define \cross and * as functions that consumes the linear
list and return a new one?
On Friday, October 20, 2017 at 10:11:00 AM UTC-4, Russoul wrote:
>
> Let's treat `list_vt(a,n)` as algebraic vector of dim 'n'. Then let's
> perform some operations on a bunch of them:
>
> (*pse
Hi,
We now have dynamic templates, parameterized by static terms. Is it
possible to have some simple form of static templates like the followings?
Or is there any other way to make static functions ad-hoc polymorphic?
datasort typelist =
| tnil of ()
| tcons of (t@ype, typelist)
#define :: t
to the domain of meta-programming.
>
> In general, it is very difficult to do meta-programming in a typeful
> manner. Often one tries to write code to generate code that may
> contain type-error and then apply typechecking to the generated code.
>
> On Friday, October 20, 2017 at 5:45:45
Hi Hongwei, just for the record, let me put down some offline discussions.
1. Programmers can decide how a literal is parsed, or even write some
plugins to parse some custom literals. For instance, 1 can be interpreted
as int, nat, and int(1) etc. Programmers should be able to either turn a
kn
Hi Brandon,
ATS, as formulated in http://www.ats-lang.org/MYDATA/ATSfoundation.pdf, is
proven sound. See Section 3. ATS with theorem-proving is proven sound by
proof erasure, in Section 4.
As far as I know, the soundness is proven directly, following the
traditional approach of Progress + Pre
Hi Artyom,
This is awesome :)
I have a question about "gradual improvement" of performance. I personally
feels it is more about gradual improvement of specification, e.g. change a
simple data type into a more refined type, to catch more bugs. So the sales
pitch is more like "write dirty code
Hi Artyom,
Yes, I think it's good :)
(Sorry for the delay. I was offline for the past week. )
On Monday, April 2, 2018 at 1:48:19 AM UTC-4, Artyom Shalkhakov wrote:
>
>
> Hi Steinway,
>
> On Sunday, April 1, 2018 at 11:39:34 PM UTC+6, Steinway Wu wrote:
>>
>> H
Did anyone mention operators definition/overloading? I think currently in
ATS2, one can only overload a symbol with a function. But I actually prefer
how OCaml and Haskell handles operators: they are just functions whose
names happen to be symbols instead of alphabets. One use parenthesis around
Great work, Lance! You helped me understand what smart contract means :)
On Friday, April 27, 2018 at 12:17:01 PM UTC-4, Lance Galletti wrote:
>
> Hey ATS users!
>
> I recently had the chance to build a blockchain and smart contract
> language in ATS - all with a nice CLI thanks to
> https://git
that ATS
uses late-binding.
On Tuesday, February 13, 2018 at 2:52:29 PM UTC-5, Steinway Wu wrote:
>
> Hi Hongwei, just for the record, let me put down some offline discussions.
>
> 1. Programmers can decide how a literal is parsed, or even write some
> plugins to parse some cu
Hi,
I just noticed that there are some Nix scripts. I never knew we have Nix
efforts. Could someone provide some insights into the experiences using Nix
for ATS? Is it working? Does someone maintain a Nix package for ATS?
--
You received this message because you are subscribed to the Google
Hi all,
I just updated the ats-redis bindings to work with the latest hiredis.
https://github.com/steinwaywhw/ats-redis
It is a binding at its bare minimum, but still useful. Pull requests are
welcomed.
Npm package is on the way. I did something wrong and need to wait 24hr
before I can publ
Hi Hongwei and August,
https://glot.io/snippets/f0nd233vde
I have this functor code working without any "name" hack. @Hongwei, did you
make any improvements on templates to make it happen? Or am I missing
something? And btw, glot.io is still running ATS 0.2.11.
On Wednesday, March 29, 2017 a
Oh I see. But anyway, here's a monad type class. Just for the record.
https://glot.io/snippets/f0nejek645
On Tuesday, May 1, 2018 at 11:27:29 PM UTC-4, gmhwxi wrote:
>
>
> This approach can only handle simple type constructors like list and maybe.
> It would not handle List defined as follows:
I actually just tried it, and it works with `[n:nat] List (a, n)`. See
https://glot.io/snippets/f0nf39m7lk.
On Tuesday, May 1, 2018 at 11:59:32 PM UTC-4, Steinway Wu wrote:
>
> Oh I see. But anyway, here's a monad type class. Just for the record.
>
> https://glot.io/snippets/f0
Cool! I just learned about Nix recently, and it looks (at first glance, at
least) promising. Do you (or Brandon) have any experiences comparing
packaging individual ATS libraries using NPM vs using Nix?
On Tuesday, May 1, 2018 at 11:29:29 PM UTC-4, Artyom Shalkhakov wrote:
>
> Hi Steinway,
>
>
Hi,
If a put a template function invocation inside a closure function, it seems
that the template is resolved at the closure definition time. I know one
way to work around this is to use templates all the way, and replace
closures with something like `foobar$fwork`. But is there another way of
Well, I sort of find a way around, that is to write a eta-expanded version
that is a template. So the template get's invoked right before it is used
to generate a closure. https://glot.io/snippets/f0pf8h25o9
On Thursday, May 3, 2018 at 8:05:28 PM UTC-4, Steinway Wu wrote:
>
> Hi,
&
I kind of hope there's some sort of `-` besides `-` and
`-` stuff. Just to mark that this is a template and should be resolved
later.
On Thursday, May 3, 2018 at 8:26:28 PM UTC-4, Steinway Wu wrote:
>
> Well, I sort of find a way around, that is to write a eta-expanded version
Hi,
Even though `stream_vt (a)` is defined on `a: vt@ype`, many library
functions for `stream_vt (a)` is only defined on `a: t@ype`. It feels like
`a: t@ype` is easier to work with since there's no need to free a single
element in some of the library functions, like `stream_vt_make_cons`. Is
Oh, there's a gfree_val and gfree_ref
On Saturday, May 5, 2018 at 11:01:16 PM UTC-4, gmhwxi wrote:
>
> Is there a template called gfree? You can put gfree(x) there.
> For non-linear x,
>
> implement(a:t@ype) gfree(x) = ().
>
> On Saturday, May 5, 2018 at 10:51:34 P
I have a follow up question. How does `~xs` as in `$ldelay(..., ~xs)`
handle a stream of linear elements, or even linear closures?
On Saturday, May 5, 2018 at 11:23:33 PM UTC-4, Steinway Wu wrote:
>
> Oh, there's a gfree_val and gfree_ref
>
> On Saturday, May 5, 2018 at
And the `free` method is defined to be the second argument of $ldelay? Is
that understanding correct?
On Sunday, May 6, 2018 at 12:19:55 AM UTC-4, gmhwxi wrote:
>
>
> A linear stream is a bit like an object with two methods:
> one for eval and the other for free; !xs calls the eval method
> and ~
I was playing with a utility library based on type classes, implemented as
templates. As you mentioned, I experienced "interface explosion". For
things like a fold, or a fmap, I have a t@ype version that is probably
garbage collected, a vt@ype version that is call-by-value, and a vt@ype
version
That’s awesome!
--
You received this message because you are subscribed to the Google Groups
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-use
Hi,
It seems the documentation at
https://github.com/githwxi/ATS-Postiats/wiki/Building-and-installing as
well as scripts at
https://github.com/ats-lang/ats-lang.github.io/blob/master/SCRIPT/C9-ATS2-install-latest.sh
are outdated. I’m trying both and encountered link errors.
Here’s what I
It is so weird, turns out that
ATSHOME=/some/path/with/../../in/it make -f Makefile_devl all
will fail, but
ATSHOME=/some/absolute/path/with/no/dot make -f Makefile_devl all
works.
Any idea what could have caused that? Is it a Make issue or is it an ATS
compiler issue?
*Steinway Wu*
*吴翰文
67 matches
Mail list logo
