Applied Type System; does anyone use this thing?

In roscidus.com/blog/blog/2014/06/06/python-to-ocaml-retrospective/ some guy blogs about his rewrite of some Python program. Randomly, one of the languages he considers is 'ATS': ats-lang.org/Home.html
ATS seems to the be result of some guy having strong opinions about type systems, while having very weak opinions about language design. So for comments ATS literally has ML-style, C-style, C++-style options, and also some fourth novelty that the author found useful once. The author introduces tuples, then boxed tuples, then basically writes "so which should you use? well, uh, profile it I guess. Maybe there's a difference in some cases?" The whole language is like this.
And in some respects it's spectacularly ugly:#include "share/atspre_staload.hats"#include "share/atspre_staload_libats_ML.hats"// ^-- these fucking stdlib namesimplement main0 () = // "main0" ... let val f = 42.0 val i = g0float2int (f) // "gee zero" prefixes? manual name mangling in print_int (i); print_newline () endOTOH, Rust is pretty ugly too. ATS is supposed to have similar capabilities. Has anyone looked at it?
careful distributing binaries. ATS's compiler names symbols after the the full path of the compile-time location of the files involved, so it leaks your username if you compile files under your homedir.

Other urls found in this thread:

pastebin.com/D8zdEmYH
gnu.org/software/emacs/manual/html_node/emacs/Abbrevs.html
web.archive.org/web/20121218042116/http://shootout.alioth.debian.org/u64/ats.php
twitter.com/SFWRedditVideos

pastebin.com/D8zdEmYH has some code written by the ATS guy himself.
My only explanation is that, before he developed ATS, he was employed for 20 years with pay based on LOC.

Contributed on ats-lang-users:
I am foaming at the mouth.

There's no doubt that ATS looks unpleasant, and is probably unpleasant to write. It provides what is, AFAIK, a unique feature, however, which is the ability to formally specify and prove the properties of the code you're writing. So, unlike the seL4 kernel, which was written in C and then laboriously proven in Coq (over 200,000 lines of proof code for less than 10,000 lines of kernel code, IIRC), ATS is supposed to unite programming and proof. It's a neat concept, even if the language itself looks pretty rough.

But you'd use ATS in fairly restricted domains. High security kernels and operating systems, maybe networking stacks, that kind of thing. It's not what you'd use for manipulating text files or writing 2D games.

Do they not understad M-w -> C-y?

That costs you a lot of juggling when you use the kill ring for anything else. Try this:
gnu.org/software/emacs/manual/html_node/emacs/Abbrevs.html
Your code is less readable this way, though.

Very cool. Thanks.

Isn't Ada/SPARK exactly doing what you're saying?

Rust isn't ugly, it's cleaner than C or C++. It's not pretty though.
ATS on the other hand, now that's ugly.
I've looked at ATS, but the problem is there are exactly 2 people using it so it's impossible to get useful information about it and of course it has no libraries. It's really only useful to perform proofs on top of C programs. The proof system is neat but the syntax makes it unusable, and even the main author uses the gc instead of the pointer proofs.

No.
Yes.

No.

C has less syntax elements, but the same fragment of code in C is a shitload dirtier since it tends to contain a lot of hacks and tricks to achieve even basic results.

what a piece of horse shit tbqh

#include "share/atspre_staload.hats"#include "share/atspre_staload_libats_ML.hats"datatype option0 (a:t@ype) = | option0_none (a) of () | option0_some (a) of adatatype list0 (a:t@ype) = | list0_nil (a) of () | list0_cons (a) of (a, list0 a)fun {a:t@ype} list0_last (xs:list0 a): option0 a = let fun loop (x:a) (xs:list0 a) = (case+ xs of | list0_nil() => option0_some(x) | list0_cons(x, xs) => loop x xs) in (case+ xs of | list0_nil() => option0_none() | list0_cons(x, xs) => loop x xs) endimplement main0 () = let var list = list0_cons("hello", list0_cons("there", list0_cons("friend", list0_nil()))) var last = list0_last(list) in case+ last of | option0_none() => print_string("no last to list!\n") | option0_some(last) => (print_string(last); print_string("\n")) endsomehow it's growing on me. I guess ML is such genius, I can tolerate a lot of it's around. I'll at least give ATS enough of a chance to see what the point is.
... the author's own code is still a mess though.

That's just useless masturbation.
Either the output is what you want or it isn't.

t. literal inbred

How does it compare speed-wise to say, Haskell?

type systems are for fucking nerds
go read a category theory textbook fag

for speed, it beats the shit out of Haskell.

ever write an assert() or any equivalent which is just "if this isn't as expected somehow, murder the user and hope we get away with it"?
proofs are the same thing but they throw errors at compile time instead of runtime, so you get to fix your code before deploying it.
ATS's default setting, on a scale of 0 ("do whatever the fuck you want") to 11 ("I have not run this code; I have only verified that it is correct.") is about a 4, because the normal indexing operators like somestring[3] require a proof to work at all.

HAHAHAHA

All of the dependently typed languages are far slower than everything else except interpreted shit. Its not fundamental but its like saying Haskell is faster than C++ because the compiler has more guarantees. It may be true someday, its not now.

I bet you are a big fan of javascript

since ATS is hard, I've gone shopping a few times for a similar enough language. Idea: if I learn this, using its better docs or examples, I might then be able to come back to ATS and have an easier time, since it won't be so alien anymore.
language shopping result: nothing is similar enough to be worth the time.
ATS's proofs and dependent types have no runtime overhead at all.

The proofs not having runtime overhead does not mean the language is faster for the same reason Haskell is not faster than C++.

Indeed. That it beats the shit out of Haskell is just a fact, not something I've made any attempt to explain.

If the goal is to be slow

Learn Idris. Idris is the most modern dependently typed language that is intended to actually be programmed in. It is also very nice for writing proofs.

is Dons telling people to just lie outright if they don't know anything about a language? Such a nasty, mendacious little community that language has.

I looked at Idris. It wasn't similar enough to be worth my time. ATS's programming with theorm-proving isn't there, and Idris (like rust) tries to prove things for you (termination in Idris's case) instead of giving you the tools to prove them.

The termination checker is just for convenience you can turn of the checker. You can write your own termination proofs etc. The checker is just there because without proving termination of a proof your proofs can have errors in them. You must not know anything about the language.

I know very little bit about--like I said, my interest was learning ATS, so when Idris didn't look useful for that I stopped looking into it.

You should consider learning Idris instead then.

The language that its supporters in this thread agree is slower than anything except interpreted shit?
Nah. I'll use the JS target if I want some ATS code to run slower than usual.

ATS is dependently typed and fits in that "slow shit" category

Since ATS is amazing for speed, this rule you have about dependently-typed languages is just wrong. Sounds like a self-serving myth, "Idris isn't bad; you just can't expect the same kind of speed from it."

ATS is not amazing for speed. ATS is slower than almost every real language that is not interpreted.

Yeah, you're just making shit up. This is THS. Since Idris is implemented in Haskell, I guess the same kind of dishonest creeps are interested in it. That's a pity.

Only benchmarks that ATS does any good at are trivial tree operations that every functional language does well on

Yeah, OK man. You're definitely going to lie your way into the big industry jobs. Since I've got a job, I'm going to stop helping you shit up this thread.

...

web.archive.org/web/20121218042116/http://shootout.alioth.debian.org/u64/ats.php
that mandelbrot

numbers from benchmark game 2014:
ATS: 24, C++ 19

...

look, children. This is what rabid language partisanship reduces a human being to.

I'd like to learn it, but I'm really into FORTHs lately, and their simplicity and syntaxlessness makes me moist.

How big are the binaries? Is the language suitable for embedded code

hahahahaha

ATS won't let you index into an array without a proof and it has a lot of syntax, so it won't make you moist.
Small. Sure. ATS is probably slightly easier than Forth for embedded work since it can more easily exploit the popularity of C for embedded work.
I'm more interested in the other meaning of 'embedded' - injecting ATS into programs that already exist. It does this very well.

it's a page of benchmarks. The one I singled out is exceptional due to its memory usage probably because C++ is desperately trading memory for speed and still losing to ATS on speed. 2012 is not the 'before time'; I didn't pay a team of archaeologists to find these benchmarks for me. Turning your nose up at single(lol)core performance is like turning your nose up at non-VR games or non-quantum computing--it just means that you're a memelord without perspective and that your opinion is worthless--not an exercise in reason, but an exercise in recall ("which of these two things is newer and therefore better?").

A few of those microbenchmarks are good because a single Chinese autist spent a shit ton of time writing the equivalent of assembly in ATS. If you do the equivalent in any language you will get the same results. Look at the code he wrote for those benchmarks that did well jesus fucking christ. Eventually autists in other languages did the same thing and well beat out the ATS performance.

probably the author of the language, and it probably looks like complete shit because that's his normal style (c.f. the beginning of this thread) and not because he's actually doing anything that unusual.
yeah the benchmark 'game' is shit and it always will be shit so long as the people behind it are so sensitive to attacks on their honor. The important takeaway is that ATS beats the shit out of Haskell for speed :)

hahahahaha

No I think it's fast because I'm using it and can plainly detect that it's fast.
Meanwhile, writing 'the equivalent of assembly' in a dogshit language doesn't make it any faster. On the contrary, doing that in J or Python or JS will result in massive slowdowns.
What people actually do to make pigs fly is they go off and write a library in another, actually fast language, and then load that and do a benchmark that spends 99% of its lifetime in the other lang's code, and conclude that the pig is natively capable of flight.
This was really obvious when Haskell was doing it ("lol, you're using ? Wow you're dumb. You should be using GHC.Only.Extension.String."), but there's also stuff like NumPy.
The approach the benchmark should've taken was to say that these extensions hybridize the language, and deserve a separate score.
... OK that's enough milking. Say something more than "hahahahaha".

Writing the equivalent of assembly in anything makes it fast

epigrams of Holla Forums
#1. Dependently typed languages are much slower than non-dependently typed languages.
#2. Clearly-written code in a language is always slower than 'the equivalent of assembly' in a language.
go on. it's already funny.

...

...

...