Re: ATS3: ATS/Xanadu

2018-10-22 Thread Chris Double
On Mon, Oct 22, 2018 at 1:38 AM gmhwxi wrote: > > > Yes, you can already use ATS2 with Z3: > > https://github.com/githwxi/ATS-Postiats/tree/master/contrib/ATS-extsolve-z3 > I wrote a bit about using it here: https://bluishcoder.co.nz/2018/01/03/writing-basic-proofs-in-ats.html --

Re: repl?

2018-10-22 Thread Chris Double
On Mon, Oct 22, 2018 at 3:19 PM Hongwei Xi wrote: > > A few years back, I looked into to the possibility of using CINT > build an REPL for ATS2. Now Cling seems to be under active development: Can TCC compile ATS code? https://bellard.org/tcc/ It can be used as a dynamic code generator as well

Re: repl?

2018-10-22 Thread Julian Fondren
On Monday, October 22, 2018 at 2:34:29 AM UTC-5, Chris Double wrote: > > On Mon, Oct 22, 2018 at 3:19 PM Hongwei Xi > > wrote: > > > > A few years back, I looked into to the possibility of using CINT > > build an REPL for ATS2. Now Cling seems to be under active development: > > Can TCC

Re: repl?

2018-10-22 Thread Brandon Barker
Seems to be on of the big arguments for using Go. Of course ATS will (rightly) never match the simplicity criteria that they strive for. Though I imagine for more "complicated" scripts typechecking/constraint solving may become the predominant portion of time spent among compiling and running

Re: repl?

2018-10-22 Thread Raoul Duke
so just to be a pedantic defender of real UX, please everybody note that (at least according to me) scripting != repl, and repl does not guarantee good ux. an actually useful, helpful, repl bestows new super powers on those who can get their hands on such magical, enchanted, tools. it likely

Re: repl?

2018-10-22 Thread Vanessa McHale
This is an aside, but perhaps caching constraint solving and the like would be a good idea? I know Agda will not re-typecheck a module dependency unless it is touched. On 10/22/18 4:05 PM, Brandon Barker wrote: > Seems to be on of the big arguments for using Go. Of course ATS will > (rightly)

Re: repl?

2018-10-22 Thread gmhwxi
Yes. Please use v0.9.26. TCC v0.9.25 is buggy and should be avoided. I like TCC a lot. It is a pity that it does not get maintained these days. With TCC, I often use ATS for scripting. Once adequate lib support is put into place, I feel that ATS can work very well for the need of shell

Re: repl?

2018-10-22 Thread Chris Double
On Tue, Oct 23, 2018 at 10:05 AM Brandon Barker wrote: > Though I imagine for more "complicated" scripts typechecking/constraint > solving may become the predominant portion of time spent among compiling and > running code (at least in some cases). Though in this case, it probably is > less

Re: repl?

2018-10-22 Thread Hongwei Xi
>>Of course ATS will (rightly) never match the simplicity criteria that they strive for. I won't give up so quickly :) Go is a fine language. But Go lacks what I call "high mechanism" that can greatly increase one's programming productivity. With enhanced type inference and embeddable

Re: repl?

2018-10-22 Thread Hongwei Xi
>>perhaps caching constraint solving and the like would be a good idea? Definitely. Right now, patsopt typechecks the prelude files every time when it is called. On Mon, Oct 22, 2018 at 6:42 PM Vanessa McHale wrote: > This is an aside, but perhaps caching constraint solving and the like >