Re: Building ATS2 from Github head.

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* *吴翰文

Building ATS2 from Github head.

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

Re: Temptory Docs Website

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

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

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

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

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

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

I have a follow up question. How does `~xs` as in `$ldelay(..., ~xs)` handle a stream of linear elements, or even linear closures? On Saturday, May 5, 2018 at 11:23:33 PM UTC-4, Steinway Wu wrote: > > Oh, there's a gfree_val and gfree_ref > > On Saturday, May 5, 2018 at 11:01

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

Oh, there's a gfree_val and gfree_ref On Saturday, May 5, 2018 at 11:01:16 PM UTC-4, gmhwxi wrote: > > Is there a template called gfree? You can put gfree(x) there. > For non-linear x, > > implement(a:t@ype) gfree(x) = (). > > On Saturday, May 5, 2018 at 10:51:34 PM UTC

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

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

Re: Templates and Closures

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, > &

Re: Nix

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

Re: Template-based implementation for functors

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/snippet

Re: Template-based implementation for functors

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

ATS-Redis

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

Re: ATS3: ATS/Xanadu

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

Re: Intro to ATS - How to code productively

Hi Artyom, Yes, I think it's good :) (Sorry for the delay. I was offline for the past week. ) On Monday, April 2, 2018 at 1:48:19 AM UTC-4, Artyom Shalkhakov wrote: > > > Hi Steinway, > > On Sunday, April 1, 2018 at 11:39:34 PM UTC+6, Steinway Wu wrote: >> >> Hi Art

Re: Theoretical underpinnings for ATS's type system

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 +

Re: ATS3: ATS/Xanadu

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

Re: Static Templates

ain of meta-programming. > > In general, it is very difficult to do meta-programming in a typeful > manner. Often one tries to write code to generate code that may > contain type-error and then apply typechecking to the generated code. > > On Friday, October 20, 2017 at 5:45:45 PM UTC-4,

Re: Best way to handle short-living linear objects

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

Re: Deech's talk and slides from StrangeLoop 2017

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

Re: Deech's talk and slides from StrangeLoop 2017

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

pandoc supports ATS syntax highlighting

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

Re: Adding join patterns to 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

Re: Ask/Answer ATS-related questions on StackOverflow

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 >

Sublime Text - Build/Type Check with hot key

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.

A demo of Union/Find algorithm in ATS

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

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

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

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

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