Re: implement template based function on dependent type

2017-10-02 Thread Artyom Shalkhakov
On Monday, October 2, 2017 at 7:41:46 PM UTC+6, gmhwxi wrote: > > >>Could you please implement this feature? > > I don't really know how. > > Embeddable templates were added to ATS2 in an add hoc manner. > Unlike dependent types or linear types, I had no time studying this > feature carefully and

Re: Deech's talk and slides from StrangeLoop 2017

2017-10-02 Thread Steinway Wu
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

2017-10-02 Thread gmhwxi
Not stream_vt over list_vt or array_vt. Stream_vt (linear) is very different from stream (non-linear). Stream_vt presents an illusion of (possibly infinite) sequence of data but you can get only one data item at any given time. So we can talk about a linear stream of states; each state is

Re: Deech's talk and slides from StrangeLoop 2017

2017-10-02 Thread gmhwxi
Hanwen and I watched it together. It was a great talk! And very accurate, too. What you presented is what I now call "classic ATS". Very complicated stuff :) But what is really complicated is the way code is written in C. Find a C programmer and ask him/her to explain how his/her code works.

Re: Deech's talk and slides from StrangeLoop 2017

2017-10-02 Thread Steinway Wu
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

Re: Deech's talk and slides from StrangeLoop 2017

2017-10-02 Thread aditya siram
No problem. ATS is a great language! Feedback welcome. On Monday, October 2, 2017 at 8:42:57 AM UTC-5, gmhwxi wrote: > > > This is really good publicity for ATS :) > > Thanks!!! > > 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

2017-10-02 Thread gmhwxi
This is really good publicity for ATS :) Thanks!!! On Monday, October 2, 2017 at 3:02:03 AM UTC-4, Artyom Shalkhakov wrote: > > Seen on reddit: > > > https://www.reddit.com/r/programming/comments/73lhj0/a_not_so_gentle_introduction_to_systems/ > > Also see the discussion on r/rust: > > >

Re: implement template based function on dependent type

2017-10-02 Thread Artyom Shalkhakov
On Sunday, October 1, 2017 at 7:11:19 PM UTC+6, gmhwxi wrote: > > I wrote something like this: > > extern > fun > {a:t@ype} > minus(x: a, y: a): a > extern > fun > {a:t@ype} > list_minus > {n:int} > (xs : list(a,n), ys : list(a,n)): list(a,n) > > implement > (a,n) > minus(xs, ys) =