[HN Gopher] Austral: A systems language with linear types and ca...
___________________________________________________________________
Austral: A systems language with linear types and capabilities
Author : riidom
Score : 144 points
Date : 2022-12-29 01:37 UTC (2 days ago)
(HTM) web link (borretti.me)
(TXT) w3m dump (borretti.me)
| Kinrany wrote:
| > Anti-features: macros
|
| Is there a different mechanism for compile-time programming?
| zetalyrae wrote:
| Author here. Happy to answer questions.
| _dain_ wrote:
| 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?
| [deleted]
| zetalyrae wrote:
| 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
| _dain_ wrote:
| Ah great! So to summarize:
|
| - we destroy a linear value either by destructuring it
| ourselves, or by calling a cleanup function that
| transitively destructures it
|
| - we can make a type opaque to importers of our module,
| which precludes direct destructuring by the user
|
| - the compiler forces the user to eventually destroy the
| linear value
|
| - therefore the user must call our cleanup function
|
| And it's our responsibility to ensure the function
| implements the correct cleanup logic.
| zetalyrae wrote:
| Yes, that's correct
|
| >we destroy a linear value either by destructuring it
| ourselves, or by calling a cleanup function that
| transitively destructures it
|
| I think I'll borrow this for the tutorial because it's
| very succinctly put.
| all_factz wrote:
| Trying to understand: what's to prevent someone from
| calling an FFI-defined function on a free type without
| going through the whole linear types rigmarole? E.g.
| could I call `fopen` and `fclose` directly to circumvent
| the whole `File` interface?
|
| I'm sure there's a good answer. This is a really cool and
| impressive project.
|
| EDIT: Ah, just got to the section on "The FFI Boundary".
| Makes sense!
| clord wrote:
| I like that in rust one can reuse variable names, since they
| are dead anyway. Makes sense to 'update' the old name with the
| new value, sort of like a swap-and-kill. Does austral have
| this? Seems like no reason not to.
| zetalyrae wrote:
| No, in fact variable shadowing is not allowed.
| clord wrote:
| Any other mechanism for fixing the ephemeral name problem?
| I don't like having to invent meaningless names.
| jiggawatts wrote:
| This is the safe approach.
|
| Rust's name shadowing is _technically_ safe, but a massive
| footgun because humans are human and assume that in the
| same scope the same name refers to the same thing.
|
| With name shadowing, you have to read through every line to
| make sure that the otherwise immutable value hasn't been
| replaced with an impostor.
|
| IMHO, it's one of the worst Rust design decisions and
| shouldn't be copied.
|
| People will say they're too lazy to come up with temporary
| variable names, meanwhile Rust doesn't have multiple
| dispatch so every fn name has to be unique, which I
| personally find more irritating...
| array_bullock wrote:
| [dead]
| choeger wrote:
| 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!
| zozbot234 wrote:
| 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 wrote:
| > 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
|
| >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
| GuuD wrote:
| 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 wrote:
| > 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.
| jecel wrote:
| All Smalltalk history talks mention that APL was a major
| influence, and it didn't have operator precedence either. In
| addition, the Smalltalk-72 scheme of "parse as you go" would
| make implementing precedence really awkward.
|
| Smalltalk-76 introduced a fixed syntax and does have a bit of
| precedence: unary > binary > keywords. All binary messages
| have the same priority, which given that you can define new
| ones avoids a lot of complexity at the cost of a few extra
| parenthesis.
| GuuD wrote:
| 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 wrote:
| > 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
| college_physics wrote:
| 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.
| henrydark wrote:
| 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
| mdm12 wrote:
| 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
| justincormack wrote:
| 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.
| zetalyrae wrote:
| It comes from linear logic and that's as far as I know.
|
| It's not great because it can scare away programmers who hear
| "linear" and think abstract nonsense. But there's not really a
| better name. "Uniqueness type" or "Single-use type" is too
| verbose. I'd rather not bikeshed the terminology too much and
| just use what exists.
| Nevermark wrote:
| "Single-instance" type?
|
| "Single-reference"?
| masklinn wrote:
| It's not just single-use, an affine type is also single-use:
| colloquially, a single-use item is not a must-use item.
| eternalban wrote:
| Disposable Type.
| ogogmad wrote:
| Linear types <- linear logic <- linear algebra. See here: See
| here: https://www.cs.bham.ac.uk/~drg/bll/steve.pdf
|
| There's also "affine logic" which riffs on the same thing.
| college_physics wrote:
| Ahh, thats cool. Thanks for the link
| bmacho wrote:
| Nothing, it just has the name for historic reasons.
| dboreham wrote:
| I've been scratching my head over this all day since reading
| the beginning of the thread earlier. This is the one correct
| answer.
| ajjenkins wrote:
| 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.
| ummonk wrote:
| 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.
| throwaway17_17 wrote:
| 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 wrote:
| 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/Linearity...
| asplake wrote:
| Is the type/kind Region defined anywhere?
| zetalyrae wrote:
| 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
| asplake wrote:
| 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 wrote:
| Yes, it's analogous to Rust lifetimes. The term is somewhat
| older, I think I borrowed it from Cyclone: https://en.wikip
| edia.org/wiki/Cyclone_(programming_language)
| eikenberry wrote:
| > 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?
| GMoromisato wrote:
| 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 wrote:
| >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 wrote:
| > 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?
| ummonk wrote:
| "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."
|
| Even when you could verify this, it wouldn't prevent use
| after free bugs.
| masklinn wrote:
| UAF are solved by an affine type system (like Rust has),
| they don't require a linear type system.
|
| That is, an implicitly invoked destructor is not an UAF
| concern.
| GMoromisato wrote:
| Thank you--yes, that makes sense.
| zetalyrae wrote:
| >This seems orthogonal to me. If you allow pointers, then
| linear types don't help you either, right?
|
| Unsafe pointers should exist at the FFI boundary and be
| wrapped in a linear API. Every language has a "escape
| hatch" for this purpose, and you ultimately have to rely on
| practices to constrain it. You can call malloc in any
| language.
|
| >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.
|
| The problem is the compiler can't verify it. In a Turing
| complete language, it's simply impossible to do it in a
| general way _without restrictions_. Every language that has
| compile time memory safety (Austral, Rust, Cyclone, a few
| others) imposes restrictions to make the analysis
| tractable.
|
| >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.
|
| Capabilities have to be linear so that they can't be copied
| surreptitiously:
|
| https://austral-lang.org/spec/spec.html#rationale-cap
|
| >I'd like to know more about this, because it sounds cool.
|
| There's some examples in the post. The state machine is the
| state of the file handle and the linear types ensure only
| valid transitions can be used.
|
| >This also sounds cool. Do you have a code example off the
| top of your head?
|
| Not something existing I can point to. But if you have a
| function: generic [T: Type]
| function reverse(list: List[T]): List[T]
|
| If `List` is linear then this can use in place reversal
| while the interface is referentially transparent. Because
| for the type system, the list that goes in is consumed, and
| cannot be used again, and the list that comes out is a
| brand new linear type. It just happens to use the same
| storage.
| zozbot234 wrote:
| There are uses for unsafe pointers beyond FFI. In fact,
| it's only feasible to prove that unsafe pointers are used
| soundly if the unsafety is contained within a well-
| defined program module. (Proper inter-module 'FFI' with
| unsafe pointers would need something like full separation
| logic, which is very complicated!)
| GMoromisato wrote:
| Thank you--super helpful.
| masklinn wrote:
| > 1. Does that solve the close problem as well as linear types?
|
| No.
|
| > 2. Do linear types solve other problems that the above
| doesn't?
|
| Yes: destructors which can fail. This is an issue in C++ and
| Rust. For instance, in most OS closing a file may return an
| error. With an implicit closure, that is not an information you
| can retrieve, you have to know that an error can occur, figure
| out that you might be interested, and add non-standard handling
| for it (since the standard is to just drop the value).
|
| With linear types, the "close file" function you had to invoke
| will also return an error you have to handle.
|
| This is a problem with many resource types (though maybe not
| all).
| skybrian wrote:
| 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.
| quag wrote:
| 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 wrote:
| I would assume destructuring comes into play: 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.
| vlovich123 wrote:
| 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 wrote:
| Can't disagree, but still it feels _wrong_ , doesn't it?
|
| If we consider instead filesystem space exhaustion, it's easier
| to imagine a reasonable expectation that the system could enter
| a degraded service state (e.g. reads work but writes don't),
| then recover without restart.
|
| In fact I've worked on products that expected to provide
| exactly that kind of behavior, and we (tried to) test it.
| quantified wrote:
| 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 wrote:
| >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 wrote:
| 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.
| masklinn wrote:
| 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 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 wrote:
| >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).
| epage wrote:
| 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 wrote:
| > 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 wrote:
| 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.
| mamcx wrote:
| > 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...
| ummonk wrote:
| 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.
___________________________________________________________________
(page generated 2022-12-31 23:01 UTC)