13 ms·

Austral: A systems language with linear types and capabilities

211 points by riidom 4y ago

quantified 4y ago
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.
- unconed 4y ago
  >I'm looking forward to progress on this. As someone who is also bootstrapping things, I just want to point out this is not the encouraging comment you might think it is. 'How can I help?' is. The maintainer of a project puts in the work of designing it, developing it, documenting it, and publicizing it... the last thing they want to hear is "cool, just keep doing that forever until it's good enough for me to adopt wholesale without lifting a finger".
  - ummonk 4y ago
    I think this is entirely down to the mentality of the developer. Feedback that the project will achieve traction and user adoption is motivating for many of us.
    - unconed 4y ago
      Yes but "I'm looking forward to seeing more" is about as reliable an indicator of future adoption as "For sure I'll invest in your company" is, coming from friends and family. If it motivates you, you're in for disappointment.
  - catach 4y ago
    If we assume "I'm looking forward to progress on this" is true and complete for the one stating it, then the actual alternatives are: 1. "How can I help" but it's a lie. 2. Silence.
    - unconed 4y ago
      Correct. Option 2 is assigning the appropriate weight to one's own opinion in this matter.
    - quantified 4y ago
      I'd love to have the time. Family and work take it almost all up. Compilers, semantic models and type systems are of high interest for me and I've done some work related to those. But I'd be out of my depth. There are many more areas that could be contributed to. Hats off if he wrote the docs as well as the compiler, it's great technical writing, as an example of another area that usually needs assitance. Nowadays, I need to pull larger-scale integrations of libraries together, and the quality of the supply chain along with productive development practice occupy my mind. I suppose I wouldn't be out of my depth to work on the Jetbrains IDE plugin. I tend to buy licenses for tools I use (Sublime), I'd help a Patreon. If this could acquire foundation support like Rust did, it might reach a similar position.
college_physics 4y ago
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.
- ajjenkins 4y ago
  This is my first type hearing about linear types, but my guess is the name comes from the fact that you have to repeatedly “thread” a value through your code to keep using it. If you look at the example for Files, you have to pass the outputted file pointer from writeFile as an input value to the next writeFile. So you can picture that one file pointer as linearly threading through you code. And it’s specifically linear because your “thread” can’t “branch”, because that would mean you’re using the same value twice (except an if-statement is kind of a branch, but it’s ok because when the code runs the value will follow a linear path). But I agree that “linear types” is not a great name. Something like “single use types” would be clearer to me.
- henrydark 4y ago
  It comes from Linear Logic, where there's no inference A&B->A. I think the point of the name is "there's always progress". This talk explains some other origins as well as the connections between different logics to different type systems (though the focus is on stack languages) https://youtu.be/_IgqJr8jG8M https://youtu.be/_IgqJr8jG8M
- mdm12 4y ago
  My understanding is that the 'linear' terminology derives from the field of Linear Logic[1]. But, I am by no means an expert on theoretical computer science etymology! [1] https://en.wikipedia.org/wiki/Linear_logic https://en.wikipedia.org/wiki/Linear_logic
- justincormack 4y ago
  Linear in the sense you can draw a line, not a tree, through the usage - in terms of memory allocation, the linear item cannot be copied (ie create an allocation), or destroyed during its lifetime. The naming comes from linear logic.
choeger 4y ago
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!
GuuD 4y ago
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.
- riffraff 4y ago
  > I never figured out the brilliant insight about redundancy of operator precedence As many things go, the Smalltalk designers had this insight a few decades ago, all "binary messages" have the same precedence. I still think it's weird, but it makes sense.
  - GuuD 4y ago
    Fuck, I mean… yeah. Thanks for one more insight, by showing me that sending message/calling a method is a binary operation, seems so obvious but I never made that connection. This day started by shelling by Russian rockets, but reading the post and your comment somehow made it… good? I always get caught off-guard by how much baby we’ve thrown with the water with modern languages compared to some brilliancy we had in Lisp and Smalltalk. Both are extremely out of my cup of tea region, but I learn so much when I interact with them. The only thing JS and something like Java taught me is to stay away:)
    - masklinn 4y ago
      > Thanks for one more insight, by showing me that sending message/calling a method is a binary operation The other way around. A "binary message" is specifically the message of binary operators. Smalltalk also has unary messages (named messages with no parameters), and keyword messages (non-binary messages with parameters). Its precedence rules are unary > binary > keyword, and left to right. So foo bar - baz / qux quux: corge binds as (((foo bar) - baz) / qux) qux: quux You can still get into sticky situations, mostly thanks to the cascading operator ";": a b; c sends the message following ";" to the receiver of the message preceding ";". So here it's equivalent to a b. a c now consider: foo + bar qux; quux This is equivalent to foo + bar qux. foo quux Because the message which precedes the ";" is actually "+", whose receiver is "foo": foo + (bar qux); quux
epage 4y ago
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.
- alcover 4y ago
  > having everything be explicit causes complexity to be foisted on the user I agree. I think once you understand and trust a language-provided abstraction or automation, you can use it happily. It's a machine you don't need to see the entrails of. > I'd rather my systems language scale between contexts. What do you mean ?
  - epage 4y ago
    I appreciate when they work well as a general purpose language. I might need more control in a kernel. Userspace support code benefits from being in the same language and needs some systems programming features but doesn't need as much control. I also find writing tools in Rust to be a joy.
- ummonk 4y ago
  I feel like this is more of a tooling thing? E.g. I want IDE tooling that can infer type adjustments when I'm doing a refactoring.
- mamcx 4y ago
  > be explicit causes complexity to be foisted on the user Depending on the user, this is a plus. For a system language is important to be pedantic and explicit at each corner. HOW MUCH is the question! but the point of experiments like this is see how much you can go and still keep the pain low! P.D: "Complexity" can be good, but "Complicated" is what is to be avoided. I prefer to eat the complexity of Rust rules than the complications of debug a thread code...
zetalyrae 4y ago
Author here. Happy to answer questions.
- _dain_ 4y ago
  Can you give some examples of what it looks like to destroy a linear value? Elsewhere in the thread you said the compiler doesn't privilege destructor functions over anything else. I'm a bit confused how it works. The function to close a database connection has to take in a linear value for a database handle, but it returns nil. How do you actually get rid of the handle? And how does the compiler stop you from doing it incorrectly (or does it?)? --- Oh and, if open file handles are a linear resource, how do we do print-debugging? Do we need to thread a stdout/stderr linear value through the whole program?
  - zetalyrae 4y ago
    The idea is: linear interface, free core. Free types are the opposite of linear: they're unrestricted and can be used any number of types. For example: you can define a record type that contains only free values, but tell the compiler you want it to be linear. record Foo: Linear is x: Int32; -- machine-sized ints are free y: Int32; -- but `Foo` is declared to be linear end; Then instances of `Foo` behave like any other linear type. To destroy it, you'd destructure its contents: let foo: Foo := Foo(x => 10, y => 20); let { x: Int32, y: Int32 } := foo; So, how does this relate to safety? Because you can have something like: record File: Linear is ptr: Pointer[Nat8]; end; Where `File` is a linear record that contains a free (unsafe) file pointer. You can hide this behind an API, as an opaque type: module Filesystem is type File: Linear; -- `File` is opaque -- etc. end module. Opaque types can be imported from the outside, but clients don't know what they contain. So they can't construct them directly or destructure them or access record fields. Instead, you have to expose constructors and destructors in the API: module Filesystem is type File: Linear; function openFile(path: String): File; function closeFile(file: File): Unit; end module. The implementation of `closeFile` would simply be: function closeFile(file: File): Unit is let { ptr: Pointer[Nat8] } := file; fclose(ptr); -- FFI-defined function return nil; end; >Oh and, if open file handles are a linear resource, how do we do print-debugging? Do we need to thread a stdout/stderr linear value through the whole program? Borrowing allows you to relax the linearity constraints for some time: https://austral-lang.org/tutorial/borrowing https://austral-lang.org/tutorial/borrowing
zozbot234 4y ago
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.
- zetalyrae 4y ago
  > I think Rust will also get true linear types at some point This somewhat exists as `must_use`: https://doc.rust-lang.org/std/hint/fn.must_use.html https://doc.rust-lang.org/std/hint/fn.must_use.html >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. Yes, there's a fundamental incompatibility between linear types and traditional exception handling. This was a big question I had to think about and answer in the design. Basically: Rust has "affine" types (a weakening of linear types) where values can be silently discarded. The compiler inserts destructor calls (whose behaviour is customized in the `Drop` trait). The compiler also emits the exception-handling code so that when a panic is thrown the stack unwound and the destructors are called. This approach is incompatible with linear types (linear types don't privilege any one function as the destructor). So linear types are incompatible with traditional exception handling. The choice, then, is: keep linear types or keep traditional exception handling. I decided to keep linear types, because they're simpler. The full rationale is elaborated at length here: https://austral-lang.org/spec/spec.html#rationale-errors https://austral-lang.org/spec/spec.html#rationale-errors
  - JonChesterfield 4y ago
    > So linear types are incompatible with traditional exception handling. Nice to see this spelled out. If the instance can be summarily dropped without error you can throw past it, and ideally call it affine instead of linear. If the instance needs that close() call, you either can't throw past it, or you need to move the live instances into the exception instance as it passes by and deal with them at the catch site. I found a paper discussing that somewhere but didn't keep a reference to it. A possibly interesting compromise is to allow linear types, but their live range cannot contain an unknown function call, or a function call coloured with throws. That models holding on to some handle and not doing anything too hazardous until you can put it away safely.
asplake 4y ago
Is the type/kind Region defined anywhere?
- zetalyrae 4y ago
  The post was already fairly long for an explanation and I didn't want to weigh it down further. The type system is described in more detail here: https://austral-lang.org/spec/spec.html#type-universes https://austral-lang.org/spec/spec.html#type-universes
  - asplake 4y ago
    Thanks. Actually I read that one too. Several mentions of Region but not really a definition that i could find. Not that it’s a big deal, just curious. I infer some similarity with Rust’a lifetimes but I’m a bit hazy on those
    - zetalyrae 4y ago
      Yes, it's analogous to Rust lifetimes. The term is somewhat older, I think I borrowed it from Cyclone: https://en.wikipedia.org/wiki/Cyclone_(programming_language) https://en.wikipedia.org/wiki/Cyclone_(programming_language)
throwaway17_17 4y ago
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. 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. 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.
- zetalyrae 4y ago
  Thank you for the kind words! >So, I’m just going to read the compiler source and then get a hold of you later. Luckily, the entire linear type checker is just 600 lines of code: https://github.com/austral/austral/blob/master/lib/LinearityCheck.ml https://github.com/austral/austral/blob/master/lib/Linearity...
  - still_grokking 4y ago
    > Luckily, the entire linear type checker is just 600 lines of code 600 lines of code in an extremely high level and very powerful language. Curious to see it implemented in Austral.
GMoromisato 4y ago
Instead of linear types, would it be possible to just enforce some kind of "must call close" policy? 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). 1. Does that solve the close problem as well as linear types? 2. Do linear types solve other problems that the above doesn't?
- zetalyrae 4y ago
  >1. Does that solve the close problem as well as linear types? No, because if pointers are copyable, multiple places can point to the same memory address, and all destructor guarantees are gone. You then have use-after-free vulnerabilities, that is, a CVE. C++ has had RAII for 30 years. It is demonstrably, empirically not good enough. >2. Do linear types solve other problems that the above doesn't? Linear types give you: 1. Capability-based security. 2. The ability to enforce high-level, state machine-like protocols (see the database access example) at the type level. 3. Code that performs fast in-place mutation while maintaining a purely functional interface.
  - GMoromisato 4y ago
    > No, because if pointers are copyable, multiple places can point to the same memory address, and all destructor guarantees are gone. This seems orthogonal to me. If you allow pointers, then linear types don't help you either, right? But if the compiler can verify that a value is used exactly once, then why can't it verify that a value is destructed? We mark a function as a destructor and the compiler verifies that the value is passed to a destructor exactly once. > 1. Capability-based security. I'm probably missing this, but this also seems orthogonal. It seems like Capabilities are implemented with different types. The Filesystem type is different from the Path type, and you get different capabilities depending on which type you get. This has nothing to do with linear types. > 2. The ability to enforce high-level, state machine-like protocols (see the database access example) at the type level. I'd like to know more about this, because it sounds cool. > 3. Code that performs fast in-place mutation while maintaining a purely functional interface. This also sounds cool. Do you have a code example off the top of your head?
skybrian 4y ago
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? For example, real filesystems are complicated and quirky. 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.
- sparkie 4y ago
  You probably don't want all the platform-specific stuff in a capability based language, because the filesystems in mainstream OSs are not capability based, and you can't sugar-coat a non-capability system with capabilities. The capabilities need to be built in, and one of the main principles behind them is that you should not separate designation and authority. Access-control-lists (MAC, DAC, RBAC, etc) violate this principle - the authority is held separately from the designator, and this is why these systems are always vulnerable to confused deputies. In a capability based system, you should present a set of directory capabilities to a process on launch, and the process should be able to access files/subdirs, or create new files/subdirs within it, and potentially pass capabilities to those files to other processes. The app should not, however, be able to escape the directories it has capabilities to. There should be no way to go "up". The only way a process should gain access to another directory is if another process explicitly passes it the capability. This should really be enforced at the OS level, but it is not (usually). If a capability based language can enforce it in its runtime/stl, then you can at least not have to worry about programs written in those languages escaping their directories (assuming no unsafe/FFI).
  - skybrian 4y ago
    Yes. It seems like running a capability-based system on top of a non-capability-based filesystem is a form of sandboxing. It's not impossible - for example, it's how filesystem API's work in a browser. But it's tricky to prevent sandbox escapes.
vlovich123 4y ago
Interesting observation that contradicts my experience: > 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: > Memory overcommit on Linux can be turned off. > Linux is not the only platform. > 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. 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: * Memory allocation failures happen infrequently in practice. * No one writes tests that simulate behavior of code under allocation failures. * 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. Crashing on a memory allocation failure: * there’s no untested error recovery code to worry about * 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) There are times when you allocate memory and could 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. 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. 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
- dboreham 4y ago
ummonk 4y ago
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.
quag 4y ago
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? Does every linear value ultimately have to be passed to an extern function that doesn’t follow the linear typing rules?
- masklinn 4y ago
  I would assume destructuring comes into play: https://austral-lang.org/spec/spec.html#stmt-let-destructure https://austral-lang.org/spec/spec.html#stmt-let-destructure Whatever underlying value would be moved out of the linear record by destructuring (and thus consuming) it, then released via the underlying platform's operation (e.g. close(2), CloseHandle, ...) edit: from the linked section, it looks like field access is a linear operation: > when you have a linear record type, you can’t extract the value of a linear field from it, because it consumes the record as a whole, and leaves unconsumed any other linear fields in the record so for a "newtype" (a single field wrapper type) you can just access the one field, maybe.
- JonChesterfield 4y ago
  A linear type is an annotation on another thing to opt into semantics checking. The linear file probably has an integer file handle hidden insider it. As long as there is interface/implementation separation, no interface that gives you the underlying handle and not enough reflection in the language to dig it out, you're solid. Open and close must both be on the inside of the implementation so can breach the abstraction.
eikenberry 4y ago
> 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). 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?
masklinn 4y ago
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). Shame the examples are a bit too simplistic to show the value of linearity e.g. function closeFile(file: File): Unit; that's the wrong interface, because closing a file can error. And it is an issue with destructors, which linear types can solve. 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). The only document I found was https://austral-lang.org/tutorial/errors https://austral-lang.org/tutorial/errors 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).
- trashburger 4y ago
  >that's the wrong interface, because closing a file can error Realistically, it shouldn't, and there's no way you would be able to handle it properly even if it did. Flush your FDs to ensure you get write errors before closing. And EBADF means there's a bigger problem in your program (you're incorrectly sharing FDs).
  - still_grokking 4y ago
    `closeFile` is a bad example. But here are better ones: File openFile(String path) File writeString(File file, String content) Those signatures are completely wrong! Opening or writing a file can reasonably fail in multiple ways. The language does not handle any failing effects at all.
    - zetalyrae 4y ago
      I left error handling out because it's an introductory post and the code would involve too many simultaneous concerns.
array_bullock 4y ago
why aren't linear types called acyclic types?
- l- 4y ago
  https://en.wikipedia.org/wiki/Noncommutative_logic#Cyclic_linear_logic https://en.wikipedia.org/wiki/Noncommutative_logic#Cyclic_li...
Kinrany 4y ago
> Anti-features: macros Is there a different mechanism for compile-time programming?
- zetalyrae 4y ago
  Code generation at the build system layer.
atombender 4y ago
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. 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. 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 essentially Modula/Oberon with C-style syntax and no semi colons, both of which I think improve the ergonomics.
- dureuill 4y ago
  ^ this. there's a lot i like from Austral, but I think I disagree on some fundamental level with the "simplicity" goal. I simply don't think it is necessarily conductive to less errors, and expressivity of a language matters. There is a balance to be found. For example, Rust-style iterators are "complex", yet they cause less errors than explicit indexing. Their combinators, that afford a lot of their expressivity, would cause very difficult to write types without type inference. There's a similar tale of expressivity vs simplicity in the current implementation of the borrow checker in rust that is not using lexical (tied to a syntactic scope) lifetimes. For having used rust before non lexical lifetimes were a thing I can guarantee that from a user's point of view it is worth all the complexity in the rules and the implementation. I also have a hard time to imagine a serialization framework like serde without the ability to derive traits with an annotation. Separating interface and implementation opens up to (compile time, fortunately) errors when they don't match, and brings no gain: the public interface can be generated by tools like cargo doc. Ada style syntax I find difficult to read (I prefer braces) but this is purely a product of familiarity I think The document also says the language does not feature unwinding panics. What does it has then? The capability system is interesting, but I am surprised in the hello world example that printing to the console doesn't seem to require a dedicated capability. I think an extension to this capability system would be some sort of tie-in with the OS so that a given process can start with only a subset of the root capability
docandrew 4y ago
This is very close to the language I’ve been dreaming of! Best wishes for its success.
zrkrlc 4y ago
I love this! I'm currently reading the entire spec as I'm writing this BTW, you have a typo in one of your examples. > import ( > ..., > Relase_Filesystem, > ... > )
agentultra 4y ago
Cool idea, dramatic writing. I can deal with linear types without the hand-wringing. 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.” 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. If this linear type system is great, skip to why it’s great. Again, a lot of neat ideas in here. The parser is a good idea. Langsec and a security focused language is nice to see!
still_grokking 4y ago
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]). 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. This code generates almost 3.5 kLOC of C which results in a segmentation fault when compiled and run on my machine. I'm not impressed to be honest. I would be less harsh if this wouldn't be advertised as sane and safe language. But it is. --- ¹ 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.
- docandrew 4y ago
  This is a bit harsh. It’s still early in the language’s development, and the quality of the compiler/generated code shouldn’t be conflated with the principles of the language itself.
  - still_grokking 4y ago
    It does crash "on principle" though. That's not an implementation bug! If you `recur` less often it works just fine. Like I said, the language as such can't catch such bugs, as I see it.
    - docandrew 4y ago
      That’s not a bug, it’s a limitation of your operating environment. Increase the stack size and it would work. What else would you expect to happen?
      - still_grokking 4y ago
        > That’s not a bug, […] Yes, I've mentioned this. > […] it’s a limitation of your operating environment. No, it isn't. Memory is finite. If your language doesn't handle this fact it's inherently unsafe, and a ticking time bomb. > What else would you expect to happen? Simply: No random crashes. Especially as such a crash relies on the environment where the code is run. So it may work just fine "on your machine" but than crash in production… That's imho a big no-no for anything that wants to be a "safe systems language" (especially as the post is mentioning things like nuclear power plants as target audience).
valenterry 4y ago
Looks promising! Two nitpicks from my side. From the anti-goals: > 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) 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. > no context-sensitive syntax 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.
tinyspacewizard 4y ago
I have some questions; hope the OP is still around! Will there be partial application? let appendHelloFile = appendFile("Hello"); let f = openFile("log.txt"); let f2 = appendHelloFile(f); closeFile(f2); I suppose this might complicate the linear type system? Will there be a pipeline operator? I think this fits really nicely with linear types: openFile("log.txt") |> appendFile("Hello") |> closeFile This may be at odds with the no operator precedence rule. 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.
silasdb 4y ago
Hi. Thanks for the great work and great write up! 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)?
JonChesterfield 4y ago
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. 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. 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.
renox 4y ago
A very interesting language, a few remarks: - 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. - the "Arithmetic Expression" section talk about integer division overflows but not about the other overflows? - 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. - two other comments about syntax: 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 ? 2) how about using <> for not equal insteal of /= ? The "C programmer I am" read "a /= b;" as "a = a / b;" ..

211 points by riidom 4y ago

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.

unconed 4y ago
>I'm looking forward to progress on this. As someone who is also bootstrapping things, I just want to point out this is not the encouraging comment you might think it is. 'How can I help?' is. The maintainer of a project puts in the work of designing it, developing it, documenting it, and publicizing it... the last thing they want to hear is "cool, just keep doing that forever until it's good enough for me to adopt wholesale without lifting a finger".
- ummonk 4y ago
  I think this is entirely down to the mentality of the developer. Feedback that the project will achieve traction and user adoption is motivating for many of us.
  - unconed 4y ago
    Yes but "I'm looking forward to seeing more" is about as reliable an indicator of future adoption as "For sure I'll invest in your company" is, coming from friends and family. If it motivates you, you're in for disappointment.
- catach 4y ago
  If we assume "I'm looking forward to progress on this" is true and complete for the one stating it, then the actual alternatives are: 1. "How can I help" but it's a lie. 2. Silence.
  - unconed 4y ago
    Correct. Option 2 is assigning the appropriate weight to one's own opinion in this matter.
  - quantified 4y ago
    I'd love to have the time. Family and work take it almost all up. Compilers, semantic models and type systems are of high interest for me and I've done some work related to those. But I'd be out of my depth. There are many more areas that could be contributed to. Hats off if he wrote the docs as well as the compiler, it's great technical writing, as an example of another area that usually needs assitance. Nowadays, I need to pull larger-scale integrations of libraries together, and the quality of the supply chain along with productive development practice occupy my mind. I suppose I wouldn't be out of my depth to work on the Jetbrains IDE plugin. I tend to buy licenses for tools I use (Sublime), I'd help a Patreon. If this could acquire foundation support like Rust did, it might reach a similar position.

college_physics 4y ago

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.

ajjenkins 4y ago
This is my first type hearing about linear types, but my guess is the name comes from the fact that you have to repeatedly “thread” a value through your code to keep using it. If you look at the example for Files, you have to pass the outputted file pointer from writeFile as an input value to the next writeFile. So you can picture that one file pointer as linearly threading through you code. And it’s specifically linear because your “thread” can’t “branch”, because that would mean you’re using the same value twice (except an if-statement is kind of a branch, but it’s ok because when the code runs the value will follow a linear path). But I agree that “linear types” is not a great name. Something like “single use types” would be clearer to me.
henrydark 4y ago
It comes from Linear Logic, where there's no inference A&B->A. I think the point of the name is "there's always progress". This talk explains some other origins as well as the connections between different logics to different type systems (though the focus is on stack languages) https://youtu.be/_IgqJr8jG8M https://youtu.be/_IgqJr8jG8M
mdm12 4y ago
My understanding is that the 'linear' terminology derives from the field of Linear Logic[1]. But, I am by no means an expert on theoretical computer science etymology! [1] https://en.wikipedia.org/wiki/Linear_logic https://en.wikipedia.org/wiki/Linear_logic
justincormack 4y ago
Linear in the sense you can draw a line, not a tree, through the usage - in terms of memory allocation, the linear item cannot be copied (ie create an allocation), or destroyed during its lifetime. The naming comes from linear logic.

choeger 4y ago

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!

GuuD 4y ago

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.

riffraff 4y ago
> I never figured out the brilliant insight about redundancy of operator precedence As many things go, the Smalltalk designers had this insight a few decades ago, all "binary messages" have the same precedence. I still think it's weird, but it makes sense.
- GuuD 4y ago
  Fuck, I mean… yeah. Thanks for one more insight, by showing me that sending message/calling a method is a binary operation, seems so obvious but I never made that connection. This day started by shelling by Russian rockets, but reading the post and your comment somehow made it… good? I always get caught off-guard by how much baby we’ve thrown with the water with modern languages compared to some brilliancy we had in Lisp and Smalltalk. Both are extremely out of my cup of tea region, but I learn so much when I interact with them. The only thing JS and something like Java taught me is to stay away:)
  - masklinn 4y ago
    > Thanks for one more insight, by showing me that sending message/calling a method is a binary operation The other way around. A "binary message" is specifically the message of binary operators. Smalltalk also has unary messages (named messages with no parameters), and keyword messages (non-binary messages with parameters). Its precedence rules are unary > binary > keyword, and left to right. So foo bar - baz / qux quux: corge binds as (((foo bar) - baz) / qux) qux: quux You can still get into sticky situations, mostly thanks to the cascading operator ";": a b; c sends the message following ";" to the receiver of the message preceding ";". So here it's equivalent to a b. a c now consider: foo + bar qux; quux This is equivalent to foo + bar qux. foo quux Because the message which precedes the ";" is actually "+", whose receiver is "foo": foo + (bar qux); quux

epage 4y ago

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.

alcover 4y ago
> having everything be explicit causes complexity to be foisted on the user I agree. I think once you understand and trust a language-provided abstraction or automation, you can use it happily. It's a machine you don't need to see the entrails of. > I'd rather my systems language scale between contexts. What do you mean ?
- epage 4y ago
  I appreciate when they work well as a general purpose language. I might need more control in a kernel. Userspace support code benefits from being in the same language and needs some systems programming features but doesn't need as much control. I also find writing tools in Rust to be a joy.
ummonk 4y ago
I feel like this is more of a tooling thing? E.g. I want IDE tooling that can infer type adjustments when I'm doing a refactoring.
mamcx 4y ago
> be explicit causes complexity to be foisted on the user Depending on the user, this is a plus. For a system language is important to be pedantic and explicit at each corner. HOW MUCH is the question! but the point of experiments like this is see how much you can go and still keep the pain low! P.D: "Complexity" can be good, but "Complicated" is what is to be avoided. I prefer to eat the complexity of Rust rules than the complications of debug a thread code...

zetalyrae 4y ago

Author here. Happy to answer questions.

_dain_ 4y ago
Can you give some examples of what it looks like to destroy a linear value? Elsewhere in the thread you said the compiler doesn't privilege destructor functions over anything else. I'm a bit confused how it works. The function to close a database connection has to take in a linear value for a database handle, but it returns nil. How do you actually get rid of the handle? And how does the compiler stop you from doing it incorrectly (or does it?)? --- Oh and, if open file handles are a linear resource, how do we do print-debugging? Do we need to thread a stdout/stderr linear value through the whole program?
- zetalyrae 4y ago
  The idea is: linear interface, free core. Free types are the opposite of linear: they're unrestricted and can be used any number of types. For example: you can define a record type that contains only free values, but tell the compiler you want it to be linear. record Foo: Linear is x: Int32; -- machine-sized ints are free y: Int32; -- but `Foo` is declared to be linear end; Then instances of `Foo` behave like any other linear type. To destroy it, you'd destructure its contents: let foo: Foo := Foo(x => 10, y => 20); let { x: Int32, y: Int32 } := foo; So, how does this relate to safety? Because you can have something like: record File: Linear is ptr: Pointer[Nat8]; end; Where `File` is a linear record that contains a free (unsafe) file pointer. You can hide this behind an API, as an opaque type: module Filesystem is type File: Linear; -- `File` is opaque -- etc. end module. Opaque types can be imported from the outside, but clients don't know what they contain. So they can't construct them directly or destructure them or access record fields. Instead, you have to expose constructors and destructors in the API: module Filesystem is type File: Linear; function openFile(path: String): File; function closeFile(file: File): Unit; end module. The implementation of `closeFile` would simply be: function closeFile(file: File): Unit is let { ptr: Pointer[Nat8] } := file; fclose(ptr); -- FFI-defined function return nil; end; >Oh and, if open file handles are a linear resource, how do we do print-debugging? Do we need to thread a stdout/stderr linear value through the whole program? Borrowing allows you to relax the linearity constraints for some time: https://austral-lang.org/tutorial/borrowing https://austral-lang.org/tutorial/borrowing

zozbot234 4y ago

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.

zetalyrae 4y ago
> I think Rust will also get true linear types at some point This somewhat exists as `must_use`: https://doc.rust-lang.org/std/hint/fn.must_use.html https://doc.rust-lang.org/std/hint/fn.must_use.html >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. Yes, there's a fundamental incompatibility between linear types and traditional exception handling. This was a big question I had to think about and answer in the design. Basically: Rust has "affine" types (a weakening of linear types) where values can be silently discarded. The compiler inserts destructor calls (whose behaviour is customized in the `Drop` trait). The compiler also emits the exception-handling code so that when a panic is thrown the stack unwound and the destructors are called. This approach is incompatible with linear types (linear types don't privilege any one function as the destructor). So linear types are incompatible with traditional exception handling. The choice, then, is: keep linear types or keep traditional exception handling. I decided to keep linear types, because they're simpler. The full rationale is elaborated at length here: https://austral-lang.org/spec/spec.html#rationale-errors https://austral-lang.org/spec/spec.html#rationale-errors
- JonChesterfield 4y ago
  > So linear types are incompatible with traditional exception handling. Nice to see this spelled out. If the instance can be summarily dropped without error you can throw past it, and ideally call it affine instead of linear. If the instance needs that close() call, you either can't throw past it, or you need to move the live instances into the exception instance as it passes by and deal with them at the catch site. I found a paper discussing that somewhere but didn't keep a reference to it. A possibly interesting compromise is to allow linear types, but their live range cannot contain an unknown function call, or a function call coloured with throws. That models holding on to some handle and not doing anything too hazardous until you can put it away safely.

asplake 4y ago

Is the type/kind Region defined anywhere?

zetalyrae 4y ago
The post was already fairly long for an explanation and I didn't want to weigh it down further. The type system is described in more detail here: https://austral-lang.org/spec/spec.html#type-universes https://austral-lang.org/spec/spec.html#type-universes
- asplake 4y ago
  Thanks. Actually I read that one too. Several mentions of Region but not really a definition that i could find. Not that it’s a big deal, just curious. I infer some similarity with Rust’a lifetimes but I’m a bit hazy on those
  - zetalyrae 4y ago
    Yes, it's analogous to Rust lifetimes. The term is somewhat older, I think I borrowed it from Cyclone: https://en.wikipedia.org/wiki/Cyclone_(programming_language) https://en.wikipedia.org/wiki/Cyclone_(programming_language)

throwaway17_17 4y ago

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. 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. 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.

zetalyrae 4y ago
Thank you for the kind words! >So, I’m just going to read the compiler source and then get a hold of you later. Luckily, the entire linear type checker is just 600 lines of code: https://github.com/austral/austral/blob/master/lib/LinearityCheck.ml https://github.com/austral/austral/blob/master/lib/Linearity...
- still_grokking 4y ago
  > Luckily, the entire linear type checker is just 600 lines of code 600 lines of code in an extremely high level and very powerful language. Curious to see it implemented in Austral.

GMoromisato 4y ago

Instead of linear types, would it be possible to just enforce some kind of "must call close" policy? 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). 1. Does that solve the close problem as well as linear types? 2. Do linear types solve other problems that the above doesn't?

zetalyrae 4y ago
>1. Does that solve the close problem as well as linear types? No, because if pointers are copyable, multiple places can point to the same memory address, and all destructor guarantees are gone. You then have use-after-free vulnerabilities, that is, a CVE. C++ has had RAII for 30 years. It is demonstrably, empirically not good enough. >2. Do linear types solve other problems that the above doesn't? Linear types give you: 1. Capability-based security. 2. The ability to enforce high-level, state machine-like protocols (see the database access example) at the type level. 3. Code that performs fast in-place mutation while maintaining a purely functional interface.
- GMoromisato 4y ago
  > No, because if pointers are copyable, multiple places can point to the same memory address, and all destructor guarantees are gone. This seems orthogonal to me. If you allow pointers, then linear types don't help you either, right? But if the compiler can verify that a value is used exactly once, then why can't it verify that a value is destructed? We mark a function as a destructor and the compiler verifies that the value is passed to a destructor exactly once. > 1. Capability-based security. I'm probably missing this, but this also seems orthogonal. It seems like Capabilities are implemented with different types. The Filesystem type is different from the Path type, and you get different capabilities depending on which type you get. This has nothing to do with linear types. > 2. The ability to enforce high-level, state machine-like protocols (see the database access example) at the type level. I'd like to know more about this, because it sounds cool. > 3. Code that performs fast in-place mutation while maintaining a purely functional interface. This also sounds cool. Do you have a code example off the top of your head?

skybrian 4y ago

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? For example, real filesystems are complicated and quirky. 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.

sparkie 4y ago
You probably don't want all the platform-specific stuff in a capability based language, because the filesystems in mainstream OSs are not capability based, and you can't sugar-coat a non-capability system with capabilities. The capabilities need to be built in, and one of the main principles behind them is that you should not separate designation and authority. Access-control-lists (MAC, DAC, RBAC, etc) violate this principle - the authority is held separately from the designator, and this is why these systems are always vulnerable to confused deputies. In a capability based system, you should present a set of directory capabilities to a process on launch, and the process should be able to access files/subdirs, or create new files/subdirs within it, and potentially pass capabilities to those files to other processes. The app should not, however, be able to escape the directories it has capabilities to. There should be no way to go "up". The only way a process should gain access to another directory is if another process explicitly passes it the capability. This should really be enforced at the OS level, but it is not (usually). If a capability based language can enforce it in its runtime/stl, then you can at least not have to worry about programs written in those languages escaping their directories (assuming no unsafe/FFI).
- skybrian 4y ago
  Yes. It seems like running a capability-based system on top of a non-capability-based filesystem is a form of sandboxing. It's not impossible - for example, it's how filesystem API's work in a browser. But it's tricky to prevent sandbox escapes.

vlovich123 4y ago

Interesting observation that contradicts my experience: > 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: > Memory overcommit on Linux can be turned off. > Linux is not the only platform. > 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. 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: * Memory allocation failures happen infrequently in practice. * No one writes tests that simulate behavior of code under allocation failures. * 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. Crashing on a memory allocation failure: * there’s no untested error recovery code to worry about * 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) There are times when you allocate memory and could 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. 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. 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

dboreham 4y ago

ummonk 4y ago

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.

quag 4y ago

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? Does every linear value ultimately have to be passed to an extern function that doesn’t follow the linear typing rules?

masklinn 4y ago
I would assume destructuring comes into play: https://austral-lang.org/spec/spec.html#stmt-let-destructure https://austral-lang.org/spec/spec.html#stmt-let-destructure Whatever underlying value would be moved out of the linear record by destructuring (and thus consuming) it, then released via the underlying platform's operation (e.g. close(2), CloseHandle, ...) edit: from the linked section, it looks like field access is a linear operation: > when you have a linear record type, you can’t extract the value of a linear field from it, because it consumes the record as a whole, and leaves unconsumed any other linear fields in the record so for a "newtype" (a single field wrapper type) you can just access the one field, maybe.
JonChesterfield 4y ago
A linear type is an annotation on another thing to opt into semantics checking. The linear file probably has an integer file handle hidden insider it. As long as there is interface/implementation separation, no interface that gives you the underlying handle and not enough reflection in the language to dig it out, you're solid. Open and close must both be on the inside of the implementation so can breach the abstraction.

eikenberry 4y ago

> 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). 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?

masklinn 4y ago

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). Shame the examples are a bit too simplistic to show the value of linearity e.g. function closeFile(file: File): Unit; that's the wrong interface, because closing a file can error. And it is an issue with destructors, which linear types can solve. 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). The only document I found was https://austral-lang.org/tutorial/errors https://austral-lang.org/tutorial/errors 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).

trashburger 4y ago
>that's the wrong interface, because closing a file can error Realistically, it shouldn't, and there's no way you would be able to handle it properly even if it did. Flush your FDs to ensure you get write errors before closing. And EBADF means there's a bigger problem in your program (you're incorrectly sharing FDs).
- still_grokking 4y ago
  `closeFile` is a bad example. But here are better ones: File openFile(String path) File writeString(File file, String content) Those signatures are completely wrong! Opening or writing a file can reasonably fail in multiple ways. The language does not handle any failing effects at all.
  - zetalyrae 4y ago
    I left error handling out because it's an introductory post and the code would involve too many simultaneous concerns.

array_bullock 4y ago

why aren't linear types called acyclic types?

l- 4y ago
https://en.wikipedia.org/wiki/Noncommutative_logic#Cyclic_linear_logic https://en.wikipedia.org/wiki/Noncommutative_logic#Cyclic_li...

Kinrany 4y ago

> Anti-features: macros Is there a different mechanism for compile-time programming?

zetalyrae 4y ago
Code generation at the build system layer.

atombender 4y ago

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. 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. 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 essentially Modula/Oberon with C-style syntax and no semi colons, both of which I think improve the ergonomics.

dureuill 4y ago
^ this. there's a lot i like from Austral, but I think I disagree on some fundamental level with the "simplicity" goal. I simply don't think it is necessarily conductive to less errors, and expressivity of a language matters. There is a balance to be found. For example, Rust-style iterators are "complex", yet they cause less errors than explicit indexing. Their combinators, that afford a lot of their expressivity, would cause very difficult to write types without type inference. There's a similar tale of expressivity vs simplicity in the current implementation of the borrow checker in rust that is not using lexical (tied to a syntactic scope) lifetimes. For having used rust before non lexical lifetimes were a thing I can guarantee that from a user's point of view it is worth all the complexity in the rules and the implementation. I also have a hard time to imagine a serialization framework like serde without the ability to derive traits with an annotation. Separating interface and implementation opens up to (compile time, fortunately) errors when they don't match, and brings no gain: the public interface can be generated by tools like cargo doc. Ada style syntax I find difficult to read (I prefer braces) but this is purely a product of familiarity I think The document also says the language does not feature unwinding panics. What does it has then? The capability system is interesting, but I am surprised in the hello world example that printing to the console doesn't seem to require a dedicated capability. I think an extension to this capability system would be some sort of tie-in with the OS so that a given process can start with only a subset of the root capability

docandrew 4y ago

This is very close to the language I’ve been dreaming of! Best wishes for its success.

zrkrlc 4y ago

I love this! I'm currently reading the entire spec as I'm writing this BTW, you have a typo in one of your examples. > import ( > ..., > Relase_Filesystem, > ... > )

agentultra 4y ago

Cool idea, dramatic writing. I can deal with linear types without the hand-wringing. 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.” 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. If this linear type system is great, skip to why it’s great. Again, a lot of neat ideas in here. The parser is a good idea. Langsec and a security focused language is nice to see!

still_grokking 4y ago

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]). 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. This code generates almost 3.5 kLOC of C which results in a segmentation fault when compiled and run on my machine. I'm not impressed to be honest. I would be less harsh if this wouldn't be advertised as sane and safe language. But it is. --- ¹ 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.

docandrew 4y ago
This is a bit harsh. It’s still early in the language’s development, and the quality of the compiler/generated code shouldn’t be conflated with the principles of the language itself.
- still_grokking 4y ago
  It does crash "on principle" though. That's not an implementation bug! If you `recur` less often it works just fine. Like I said, the language as such can't catch such bugs, as I see it.
  - docandrew 4y ago
    That’s not a bug, it’s a limitation of your operating environment. Increase the stack size and it would work. What else would you expect to happen?
    - still_grokking 4y ago
      > That’s not a bug, […] Yes, I've mentioned this. > […] it’s a limitation of your operating environment. No, it isn't. Memory is finite. If your language doesn't handle this fact it's inherently unsafe, and a ticking time bomb. > What else would you expect to happen? Simply: No random crashes. Especially as such a crash relies on the environment where the code is run. So it may work just fine "on your machine" but than crash in production… That's imho a big no-no for anything that wants to be a "safe systems language" (especially as the post is mentioning things like nuclear power plants as target audience).

valenterry 4y ago

Looks promising! Two nitpicks from my side. From the anti-goals: > 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) 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. > no context-sensitive syntax 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.

tinyspacewizard 4y ago

I have some questions; hope the OP is still around! Will there be partial application? let appendHelloFile = appendFile("Hello"); let f = openFile("log.txt"); let f2 = appendHelloFile(f); closeFile(f2); I suppose this might complicate the linear type system? Will there be a pipeline operator? I think this fits really nicely with linear types: openFile("log.txt") |> appendFile("Hello") |> closeFile This may be at odds with the no operator precedence rule. 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.

silasdb 4y ago

Hi. Thanks for the great work and great write up! 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)?

JonChesterfield 4y ago

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. 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. 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.

renox 4y ago

A very interesting language, a few remarks: - 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. - the "Arithmetic Expression" section talk about integer division overflows but not about the other overflows? - 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. - two other comments about syntax: 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 ? 2) how about using <> for not equal insteal of /= ? The "C programmer I am" read "a /= b;" as "a = a / b;" ..