Re: ATS-CodeBook

Oops.. Well, this is my first time running patscc in a couple of years but I don't remember it being this slow (has been churning away for 5 minutes; this is version 0.3.7 of ATS2): $ which patscc /home/brandon/.nix-profile/bin/patscc

Re: ATS-CodeBook

Should be bash ./NDX100.dats On Thu, Mar 8, 2018 at 10:21 PM, Brandon Barker wrote: > Thanks for the example, > > When following the directions, I seem to run into a catastrophic error (of > course, maybe I didn't follow the directions): here was my output: > > >

Re: ATS-CodeBook

Thanks for the example, When following the directions, I seem to run into a catastrophic error (of course, maybe I didn't follow the directions): here was my output: brandon@brandon-750-170se-DevContainer:~/workspace/ATS-CodeBook/RECIPE/CSV-parsing $ bash ./myread.dats ./myread.dats: line 1:

Re: proofs vs statics?

Proofs are automatically eliminated after type-checking. Proof construction offers an approach to internalizing constraint-solving. For instance, with proofs, constraints involving multiplication can be simplified to only involve addition. On Thu, Mar 8, 2018 at 9:59 PM, Brandon Barker

atsboot: a tiny starter "kernel" in ATS

I came across this tiny kernel on the Idris discussion group, written in ATS, by Brian McKenna (who seems to be rather multilingual and I know of him from having done some nice Scala stuff as well). I'm not sure it qualifies as news at this point, since

Re: proofs vs statics?

>> Aren't proofs a static construct ... No. This is a common misconception. Proofs are dynamic but the evaluation of proofs cause no effect on the evaluation of a program (containing proofs) and can thus be omitted. Often this is referred to as proof irrelevance. You can think about it like