This article, everything else aside, is excellent. I wrote a rambling bunch of stuff in this comment and before I posted I had to cut out a lot, because HN comments aren’t really the best place for an in depth discussion about type theory implementations. So, I’m just going to read the compiler source and then get a hold of you later.<p>I am really intrigued by your explicit anti-features list. They are very close to my preferences for language design, so I was going to keep on reading just from that. The feature list is spelled out well and I certainly think you managed to make this article a nice hook for looking further.<p>Then I followed a link to the language spec. My god, but is it not only written cleanly, but the presentation is so clean too. I got a short way in (after jumping to the type system specification) and stopped to come comment. I doubt you were expecting to get compliments for layout and formatting, but I am going to shamelessly steal your spec’s presentation for my language docs.
This is fantastically written documentation. What is even more exciting for me, that this is almost exactly what I was dreaming and talking non-stop about for the last few years. I never figured out the brilliant insight about redundancy of operator precedence. On the more embarrassing note in numerous implementation not-quite-attempts I always ended up gutting loops as a feature in favor of recursion and went with effects for capabilities (among other things). Then I was usually caught off guard by either of those or my other darling — partial application interacting in unexpected way (only for me probably) with linear types, which always punched me back to square one. Extremely impressed with how sound and grounded in reality your choices are. Fantastic job.
Seems interesting though I can not say that I like the Ada inheritance (especially the interface files, but the verbosity as well, the lack of tuples and verbosity of Pair seems like it would quickly be frustrating with a linear type system, as well as the seeming lack of same-scope shadowing).<p>Shame the examples are a bit too simplistic to show the value of linearity e.g.<p><pre><code> function closeFile(file: File): Unit;
</code></pre>
that's the wrong interface, because closing a file can error. And it is an issue with destructors, which linear types can solve.<p>It would also demonstrate runtime error handling, which is completely ignored by the entire document and largely absent from the spec (error handling is discussed a lot, but never actually demonstrated).<p>The only document I found was <a href="https://austral-lang.org/tutorial/errors" rel="nofollow">https://austral-lang.org/tutorial/errors</a> which seems to indicate that not only does Austral (unfortunately imo) follows Haskell's lead through using an Either for errors (which is clear as mud), it proceeds to break Haskell's mnemonic for success/failure (not that that's great, but at least it was something).
I like this a lot! For several years I've been pondering the exact same idea of using linear types this way, combined with some kind of Rust-style borrowing. I've never really had any serious ambitions to create a programming language, though, so I'm happy to see someone finally doing this for real.<p>I love many of the choices here, like removing implicit type coercion, type inference, and operator precedence. I do worry that it could go too far. One thing we see with Go is that the simplicity of the language, while it has many virtues, also leads to some crude designs that feel regressive. For example, treating errors as values is a fine idea, but the language is too rudimentary to express sum types, so the handling of errors becomes crude and cluttered. Not bad enough to ruin the language, but bad enough to be an annoying wart. I hope that Austral can avoid falling into such traps when it needs to tackle more advanced concepts such as concurrency (I don't know how this is done today?). Not having async/await is fine, for example, provided that there is some other mechanism that doesn't lead to spaghetti code or too much repetition.<p>The part I'm the least enthusiastic about is the Algol/Ada-style syntax. I'm not sure the added verbosity of that syntax is superior to C-style syntax. The language I use the most these days, Go, is <i>essentially</i> Modula/Oberon with C-style syntax and no semi colons, both of which I think improve the ergonomics.
It's a good start. I expect that a lot will be learned by implementing the standard library, particularly if a serious attempt is made to make it work well on multiple platforms. Do you want to model a lot of platform-specific restrictions like Rust or sweep them under the rug like Go?<p>For example, real filesystems are complicated and quirky.<p>Though it's risky to build on another experimental language, it seems like building on Zig's toolchain would be a good way to get lots of cross-platform capability and experience quickly, since it accepts C and generates code for many platforms.
Simple spec? Check. Linear type memory management? Check. Ada syntax? Check. Avoiding footguns? Check. It's like you took my fantasy of the ideal low level programming language that I've never gotten around to implementing, and you actually built it.
This is rather interesting. Safe and reliable programming in the large is an important goal. Generics, sum types and typeclasses make different kinds of useful abstraction available from the get-go. I'm looking forward to progress on this.
Can somebody explain what is "linear" about linear types. There seems to be a common pattern in computer science of reusing well established mathematical terms (e.g. vectors, tensors) in confusing ways.
How does closeFile get implemented? That is, how do you consume a linear type without having to either pass it to another function or return it?<p>Does every linear value ultimately have to be passed to an extern function that doesn’t follow the linear typing rules?
Looks promising!<p>Two nitpicks from my side.<p>From the anti-goals:<p>> Async is a very specific feature, and every way of doing concurrency other than kernel threads has come and gone out of fashion (think Scala actors and Goroutines, two very admirable features)<p>Scala actors are not a language feature so are not remotely comparable to async/await or Goroutines. They are also not "out of fashion", if anything they were just overused - but it doesn't impact the language in any way at all.<p>> no context-sensitive syntax<p>There are different opinions on language design and that's fine. But "ease of use" and "complex systems" are not at adds. In fact, you can argue that Assembly is a "simpler" system than Austral. But does that make it easier to use? I don't think so. I think this part sheds light on the fact that the author needs to work on that part - not necessarily on changing the language design, but at least the language isn't great.
Interesting ideas but I'm in the camp that having everything be explicit causes complexity to be foisted on the user. There are times and places where that simplicity might offer some advantages but I'd rather my systems language scale between contexts.
What does/will Austral do on out of stack memory? Assuming it maps tail calls to branches, the call stack still grows on the non-tail calls.<p>Options I'm aware of are die (optionally gracefully), allocate more stack (segments or moving), allocate a lot of address space up front and then die on exhaustion.<p>Asking because I think there's a reasonable argument that out of heap and out of stack are the same category, and the docs discuss returning optional from allocating functions, but not tagging all functions with an optional to indicate out of stack.
Cool idea, dramatic writing. I can deal with linear types without the hand-wringing.<p>As someone famous in CS once said, “simplicity is a great virtue but it takes hard work to achieve it and education to appreciate it.”<p>Let’s face it: programming is hard and no amount of waving our hands and refusing to learn anything new is going to make anything better.<p>If this linear type system is great, skip to why it’s great.<p>Again, a lot of neat ideas in here. The parser is a good idea. Langsec and a security focused language is nice to see!
Nice writeup. I think Rust will also get true linear types at some point (i.e. types that can't be auto-dropped) because they're required for improved async support. One key obstacle to this is that Rust supports panics anywhere-- there's no provision for "panic-free" code as of yet-- and a panic might need to drop values as part of unwinding the stack. The author is surely aware of this, but it's worth making it clear.
A very interesting language, a few remarks:<p>- your blog "hides" the links behind barely visible font changes, quite funny for someone who designed a programming language with no hidden function call.. Don't do this please.<p>- the "Arithmetic Expression" section talk about integer division overflows but not about the other overflows?<p>- I couldn't understand the "Cast Expression" section, either it's me or it has to be clarified.. Also a syntax remark: I'm surprised that there is no easily greppable keyword for casting.<p>- two other comments about syntax:<p>1) the '!' symbol is used to dereference and in "read-write borrow", I don't see any obvious relationship between both usage, maybe you could use '@' for dereference ?<p>2) how about using <> for not equal insteal of /= ?
The "C programmer I am" read "a /= b;" as "a = a / b;" ..
Instead of linear types, would it be possible to just enforce some kind of "must call close" policy?<p>What if you somehow mark the close() function as--let me make up a name--a "destructor". Then enforce at compile time that a value must always have a call to a destructor (or maybe it gets called automatically when out of scope).<p>1. Does that solve the close problem as well as linear types?<p>2. Do linear types solve other problems that the above doesn't?
I have some questions; hope the OP is still around!<p>Will there be partial application?<p><pre><code> let appendHelloFile = appendFile("Hello");
let f = openFile("log.txt");
let f2 = appendHelloFile(f);
closeFile(f2);
</code></pre>
I suppose this might complicate the linear type system?<p>Will there be a pipeline operator? I think this fits really nicely with linear types:<p><pre><code> openFile("log.txt")
|> appendFile("Hello")
|> closeFile
</code></pre>
This may be at odds with the no operator precedence rule.<p>You say that async will not be baked into the langauge. I think this is the right decision. However, will there be a syntatic sugar that can be used to avoid the "pyramid of doom" when writing promise-orientated code? It is possible to make this general purpose if done right.
Interesting design. I agree 99% with the choices. My only disagreement would be about not being able to overload binary operators. I wonder how the type system handles the inherent overloading of * for floats and integers. Besides this minor point, I totally agree with the design and intent!
> every way of doing concurrency other than kernel threads has come and gone out of fashion (think Scala actors and Goroutines, two very admirable features).<p>I'd say the fact that these examples are around show that NxM, green-over-kernel threading works and works well. It made it through the crucible of fashion and is now a "good" way. Much like GC did. So I'd say your claim that kernel threads are it is misplaced... unless you just consider NxM threads to be kernel threads w/ some sugar?
I love this! I'm currently reading the entire spec as I'm writing this<p>BTW, you have a typo in one of your examples.<p>> import (<p>> ...,<p>> Relase_Filesystem,<p>> ...<p>> )
Hi. Thanks for the great work and great write up!<p>At a first glance, I only see advantages with this approach. What would be the caveats of using Austral instead of Rust (disregarding the ecosystem and toolchain factors)?
Interesting observation that contradicts my experience:<p>> A common misconception is that checking for allocation failure is pointless, since a program might be terminated by the OS if memory is exhausted, or because platforms that implement memory overcommit (such as Linux) will always return a pointer as though allocation had succeeded, and crash when writing to that pointer. This is a misconception for the following reasons:<p>> Memory overcommit on Linux can be turned off.<p>> Linux is not the only platform.<p>> Memory exhaustion is not the only situation where allocation might fail: if memory is sufficiently fragmented that a chunk of the requested size is not available, allocation will fail.<p>This is kind of the eternal vim vs eMacs debate but for malloc. In practice, I’ve not found this philosophy to be useful and actually problematic and the reasons given are the “easy” ones to convince more junior engineers. They’re true btw and the counter points provided aren’t really convincing. Regardless, the real reasons are:<p>* Memory allocation failures happen infrequently in practice.<p>* No one writes tests that simulate behavior of code under allocation failures.<p>* Memory allocation failures are basically treated as contract violations anyway in terms of triage - it’s not different from any other bug and you’d still need to fix it.<p>Crashing on a memory allocation failure:<p>* there’s no untested error recovery code to worry about<p>* the cause of the malloc failure means something else is broken / misconfigured. A crash tells you what to fix / when to fix it. A silent recovery attempt (when successful) will mask this and shift the problem (eg bug in error handling later or something)<p>There are times when you allocate memory and <i>could</i> handle failure gracefully by rejecting the request or something. However, as I mentioned. Memory allocation failures are rare and when they happen you need to fix a bug anyway. So crashing on a rare condition instead of running untested error recovery code is probably preferable in general.<p>Context: I have experience in mobile, embedded, desktop, and cloud so I’ve seen the gamut of dev environments. And everywhere the “abandon on malloc failure” turns out to be a more maintainable strategy that results in more robust code that’s simpler and shorter and faster/cheaper to develop because you’re not writing and thinking about error handling paths that never get run.<p>Regardless, it is kind of interesting to see a language adopt this philosophy. Maybe that can address some of the problems of trying to do this manually in other languages. I’m skeptical because the error paths problem remains, but I’m open to the experiment
The language was trivial to break in a few minutes. (And it likely can't do anything about it [edit to make this clear: This is not an implementation bug. Without depended types or abstract interpretation this is unfixable¹, as I see it]).<p><pre><code> module body Test is
function recur(n: Nat64): Nat64 is
if n < 2 then
return n;
else
return recur(n - 1);
end if;
end;
function main(): ExitCode is
print("recur(50000000) = ");
printLn(recur(50000000));
return ExitSuccess();
end;
end module body.
</code></pre>
This code generates almost 3.5 kLOC of C which results in a segmentation fault when compiled and run on my machine.<p>I'm not impressed to be honest.<p>I would be less harsh if this wouldn't be advertised as sane and safe language. But it is.<p>---<p>¹ Of course you could fix this with for example trampolining. But than the promise of "no hidden control flow or functions calls or allocations" would be broken instantly.