The Pain of Real Linear Types in Rust | Hacker News Reader

The Pain of Real Linear Types in Rust

gankro.github.io

167 pointsGankro81 comments

A lot of the awkwardness that the author describes comes from destructors, which Rust has taken from C++. In fact, Rust has even inherited the incoherence between destructors and exceptions from C++, due to the lack of a solution to the double-throw problem and the need to write unsafe code that is correct in the face of unwinding.

The 'dropck' pass is one of the corners of the language that has no precedent in a type system that has been proven sound (at least as far as I am aware, someone please correct me if i'm wrong), and it has had a lot of soundness issues in the past.

The fact that destructors have magical powers that the language refuses to bestow on ordinary functions is a bad sign. And destructors are terrible for predictable code: the order in which destructors run for temporary results in a single expression is not even specified by the language, and there are some surprises (https://aochagavia.github.io/blog/exploring-rusts-unspecifie...) that make it harder to write correct unsafe code.

If you were to design a language from the ground up with linear types and no destructors, it would be dramatically simpler than Rust.

Yeah dropck is a fun little gem, which has received several post-1.0 revisions due to soundness problems.

I agree the system you propose would be simpler in terms of spec and effort, but I don't know about simpler to use. Much like removing mutable references in favour of `foo(X) -> X` would be a simpler type system, but awful to use compared to `foo(&mut X)`.

The simplest system to use is unrestricted references with some form of automatic garbage collection. If you decide that you want a type system that statically tracks resource utilization, why stop halfway at something that only partially solves the problem? I guess you could one-up linear types here and ask for a type system that makes all creation and destruction of information explicit, e.g. https://www.cs.indiana.edu/~sabry/papers/reversible-logic.pd..., but this is probably a more useful route to explore for a hardware design language than a software programming language.

> If you decide that you want a type system that statically tracks resource utilization, why stop halfway at something that only partially solves the problem?

Because there's a tradeoff between ergonomics and static guarantees. A hybrid system (in this case, static tracking of ownership combined with automatic resource destruction) is a valid choice to balance the upsides and downsides of each extreme.

The "point of Rust" is to be the simplest zero-runtime-overhead system to use.

I'm not particularly educated in this issue, but if you're going to use a garbage collector, why not just use a language with a GC that abstracts away memory management completely? Like, what would be the advantages over Java?

I agree that dropck is scary and needs more verification before we can have reasonable assurance of its soundness. But you're being unnecessarily reductive here: the tradeoff between control and ergonomics offered by destructors is well-known. If you think Rust is verbose today, imagine a Rust where every value had to be explicitly disposed of in every scope (including temporaries). Graydon was well aware of strictly-linear type systems, and chose to go with destructors for (heh) sound reasons.

It's not like destructors actually remove the complexity. The extra function call you need to add to replace the destructor is already present in your program; it's merely hidden from view. If you are trying to verify the code you have written (either informally or formally) and want to consider all paths through the program, then you need to include the invisible control-flow created by the compiler for destructors. I don't see how it gets any simpler by not being written in your program.

Nobody's talking about semantic simplicity; we're talking about developer ergonomics.

And more specifically developer writing ergonomics.

In terms of understanding how the code will execute or testing your app, the implicit, confusing rules are less "ergonomic".

Is GC less ergonomic than C-style malloc/free? I don't think so, and not only when writing code. It makes things easier all around.

(Yes, GCs require tuning and so forth, and that can be a pain, but so does malloc and free, so that's a wash. In most applications you never need to manually tune a GC.)

If you take the view that code is read more times than it is written (which is lightly amusing given the topic of this thread), then shouldn't you optimize for the ergonomics of reading and understanding code that is already written rather than writing it? I don't see how Rust's choice is defensible from that viewpoint. If I quizzed actual Rust users (rather than the language developers that are posting here) about the invisible control-flow created by the compiler, I doubt very many of them would get it right.

Usually programmers don't care about the exact order that things are freed in. That's the whole reason why GC's have been so successful in programming languages (not to mention things like ARC, which are still deterministic but obscure).

I get that occasionally it's important to know the exact order, and this is where tighter rules and tooling can help. Rust wasn't designed to be an "everything is as explicit as possible" language. (Neither is C, for that matter, ever since compilers stopped paying attention to the "register" keyword…)

GC lets you write functions that return heap allocated values without worrying about who's responsible for freeing the result. That in turn leads to functional code over procedural, which in turn leads to simpler and easier understood code.

That is, it's less about order and more about bookkeeping. The ergonomics directly affect code quality.

Code only gets read if it gets written in the first place, which it won't if your fresh new language makes it too hard to bootstrap an ecosystem and a community. One of the foundational premises of this year's ergonomics initiative is that Rust code is still too hard to write; a Rust-like language with linear types instead of destructors would be yet harder to write, and would only improve the ability to reason about code in a small minority of cases. I've been writing Rust code since before it was cool to claim you were doing things "before it was cool", and while I appreciate the cases where people have longed for linear types, I have never needed anything more than what destructors provide (which subverts the very premise of your comment, because, for my uses, enforcing linear types would be harder to both read and write). Nobody on the Rust team is pretending that there aren't tradeoffs.

Perhaps this is obvious to everyone else, but it isn't to me. Are you advocating explicitly dropping every variable I create? Like `init; use; drop;` explicitly where right now I essentially do `init; use;` and then there's an implicit drop when we exit scope?

I guess it is only for ones with nontrivial destructors.

That makes the "trivialness" of a destructor part of the interface, which is a price. But then from my experience in C++, we pay that price anyway, because to have any sort of assurance about what you are doing, you need some clue about what the destructor does.

You would be required to drop values that aren't moved elsewhere. Currently Rust has a one-bit reference count which dynamically tracks which values need to be dropped. Linear types would transform this into a static property that the compiler checks.

Part of the pain would come from conditionals:

    if something { 
        func(val1);
    } else {
        func(val2);
    }

This would be disallowed because the liveness of val1 and val2 can't be statically known after the conditional.

If "val1" and "val2" are really things that have to be used exactly once, then the above code is already in error (unless they are provably the same object), and a compiler with linear types will correctly complain about it.

This is indeed "pain", but of a good kind (at least it if the error message is decent).

I admit there are harder cases:

    if(foo)
      func(val1)
    else
      func(val2)

    ... do something that doesn't change foo or use val1, val2 
    ...  

    if(!foo)
      func(val1)
    else
      func(val2)

Is correct, if strange, code which I assume is hard for a compiler to understand. But then it is hard for humans too.

Its hard for me to imagine that requiring every value to be explicitly dropped would produce code which is easier to read and understand.

Keep in mind today Rust is intended to be a better C++. (For loose values of 'intended'.)

Destructors are a common resource management idiom there (although I guess most C++ programmers couldn't describe the behavior correctly), and there are no other really common idioms for that.

Better the devil you kind of know?

This is a really interesting thought. In the presence of must-use types, you'd imagine that types with side effecting Drop impls (like files), would want to migrate to eventually being used/consumed by a "close" method. But doing that safely in the presence of panics would require... exception handlers?...

You could use something like Go's 'defer' statement to ensure 'close' is called before the current function returns.

Which already exists in Rust in the form of... wait for it... the Drop trait. It's the same thing.

The difference is that Go's `defer` is explicitly written out in the relevant scope, while Rust's `Drop` is implicit and defined elsewhere.

There's a "scopeguard" crate that uses Drop to make it explicit.

Destructors seem to be a pain point for functional programming people. They're inherently imperative; they don't return anything because they have no one to return it to.

The "unsafe code" problem comes mostly from backpointers. If you have a data structure with a doubly linked list, and the forward pointer and backpointer are both pure references and can't be null, no order of destruction is strictly valid. You can't create, destroy, or manipulate a doubly linked list or a tree with backpointers in safe Rust. That's a problem.

Maybe forward pointer/backpointer pairs need to be a language level concept. The compiler needs to know that the forward pointer and the backpointer are in a relationship. The pair needs to be manipulated as a unit. You have to have mutable ownership of both references to manipulate either. The borrow checker and destructor ordering need to understand this.

> Maybe forward pointer/backpointer pairs need to be a language level concept. The compiler needs to know that the forward pointer and the backpointer are in a relationship. The pair needs to be manipulated as a unit. You have to have mutable ownership of both references to manipulate either. The borrow checker and destructor ordering need to understand this.

There are many more patterns where that came from, and you don't want to teach the compiler about all of them. I don't think there's anything wrong with having a lower-level "unsafe" mechanism to let you use the language itself to build new types of structures that then provide a safe interface.

As a random example, consider the rust "intrusive-collections" crate (https://crates.io/crates/intrusive-collections), which provides the kind of "no extra pointer" linked list where you can embed a list head (or multiple list heads) directly in your structure. I don't think every such crate should have its functionality native in the compiler.

rust "intrusive-collections" crate

People used to code like that, mostly in assembler and sometimes in C. It's not necessary for functionality. It's just an optimization. One that needs to be justified with benchmarks. Also, it's not at all clear that use of that module is safe.

I'm beginning to think there's a cult of l33t unsafe Rust programming, where people who write unsafe code think they're cool. I used to say that the way to cure new programmers of that is to put them on crash dump analysis for a few months. After they've found pointer bugs in other people's code, they'll have a better sense of why pointer safety is important.

> It's not necessary for functionality. It's just an optimization. One that needs to be justified with benchmarks.

I've worked with people who have the benchmarks to back it up; pointer traversals are expensive.

> people who write unsafe code think they're cool

I've tended to find the opposite: most of the Rust programmers I run into treat unsafe code as an occasionally necessary evil, and every time they write it they think about how the landscape could be improved so they wouldn't have had to, or how to encapsulate it in a separate crate with a small surface area.

   Destructors seem to be a 
   pain point

The problem is not so much typing as such (things that don't return anything but terminate -- as destructors do -- can be typed as Unit) but rather to find a good trade-off between expressivity of the language and simplicity of the typing system.

Basically explicit destructors mean the typing system needs to track lifetimes and ownership in some form or shape. There seem to be two main options.

- Simple lifetime/ownership scheme, but then you need a garbage collector anyway, and that it's mostly pointless to have explicit destructors. Just let every variable be cleaned up by the GC makes for a simpler language (under the hood clever escape analysis might be used for stack allocation of variables that don't escape their activation context).

- Avoid a GC, but then you need a complex typing system with unique owners to have any chance at expressivity (and you still need unsafe blocks and reference counting). This is Rust's choice.

Another issue is how consistently to combine destructors with other effects, in particular exceptions.

   Pointer/backpointer pairs 
   need to be a language level 
   concept.

As "JoshTriplett" also suggests, this is certainly an interesting idea, but I don't think a compelling choice has been found yet.

Think of backpointers as a combination of Rust optional pointers and weak pointers, mostly checked at compile time. The basic rule for backpointers is this: If an type instance A contains a backpointer P1, it must either be a None, or a reference to a type instance B which has exactly one reference P2 to A.

Checks required:

- P2 cannot be changed when P1 is not None. (Run-time check; the compiler has to recognize when it is necessary.)

- P1 can only be set to None or B. (Compile-time check)

- P1 must be set to None before B is destroyed. This avoids a dangling pointer. (Compile-time check when possible, otherwise run-time check.)

- Borrow checking must treat a borrow using P1 as a borrow of B.

These simple rules would maintain the invariant for the backpointer. This allows doubly-linked lists without unsafe code. The backpointer is "weak" and doesn't count as ownership. It's basically weak pointers with a count of either 0 or 1.

I'm not saying this can't be done, au contraire! Indeed cost coherent programming idioms can be converted into typed language primitives. But there is a price to pay in terms of typing system complexity.

It's a slippery slope argument: if you add this, why stop there? Especially if you require run-time checks.

If there was a compelling set of operation that preserved the invariants without run-time checks, and it was expressive, i.e. it covered a large number of cases that you'd otherwise had to put into "unsafe" and it didn't ruin type inference ...

> They're inherently imperative; they don't return anything because they have no one to return it to.

If your think of your whole program as being a wrapped in an implicit State monad, holding a POSIXProcessState (e.g. exit code, registered signal handlers, file descriptors, etc.), then destructors are (POSIXProcessState -> POSIXProcessState) functions.

> You can't create, destroy, or manipulate a doubly linked list or a tree with backpointers in safe Rust. ... Maybe forward pointer/backpointer pairs need to be a language level concept.

You can define abstractions like this using unsafe code just fine. It doesn't need to be part of the language. (Think about how C++ "smart pointers" work: it's just a library.)

Double-exception handling during stack unwinding in C++ is the thing I disagree most with.

And Í talk from experience.

Back in the early 2000, I modified both MS VS runtime and gcc to be able to safely throw from destructors. Note to doubters that Java allows such double-exception cases and gcc already had code back then to deal with the Java case.

The way to do it is to implicitly assume that every destructor ran during stack unwinding has a try/catch surrounding it. This way, a first exception can be thrown from a destructor, but all exceptions that ultimately escape a destructor invoked during unwinding gets eaten. (Note: you can still provide your own explicit try catch in a destructor if you care about it.)

My experience with this tweak was that the horror story people come up with to reject this approach is unfounded. Here are the reasons:

1. The actual case of double-exceptions are very, very rare.

2. In the case that do arise, the second exception is often either a consequence of the first (for example, trying to access a DB were teh first exception was a failure in some DB code) or the exact same (for example running out of memory).

3. In my experience (although, since the 2nd exception is lost, I cannot actively prove this), the first exceptionis the relevant one. This is especially true due to point #2.

4. In my experience, code that care about the exact type of exception is most often either wrong or misguided. This is because such code assumes complete prescient power over what exceptions can be thrown.

5. In my experience, catching exceptions is 99% done in the top-level message or task dispatching, which doesn't care about the type of exceptions or how many occured: you just abort the operation and do some logging.

6. The fact that double exceptions are handled gracefully informs your design, which builds up and reinforce all previous points.

I once had discussion on this in the 90s in comp.lang.std.c++ and comp.lang.c++. People would not listen.

Note: to do it with STL, you do have to add try/catch within destroy() calls within containers to be able to destroy all items.

I agree. The sad thing is that an effect system to ensure that destructors and other unwinding code can't throw new exceptions is quite simple to add to a language. Depending on the language/libraries it might cause a need to expose some new library functions that don't throw exceptions, but it's already a bad sign if you're doing nontrivial failure-prone work in destructors anyways.

Because it's not entirely clear from the title and introduction, this essay is actually arguing against extending Rust's type system to include linear types, rather than critiquing the type system as it currently exists (which people often colloquially describe as having "linear types" even if it technically doesn't).

EDIT: The intro has been updated to be clearer, so now I just look like an idiot. :)

   arguing against

The argument doesn't come from a position of deep understanding of substructural types. Once you have affine types (as Rust does), linear is not really a major step. Whether it's worthwhile from a pragmatic POV is a different question.

> Whether it's worthwhile from a pragmatic POV is a different question.

Which is exactly what they're purporting to answer...

Pragmatic concerns appear to be the bulk of this argument against them.

Such questions are best answered after MLoC or GLoCs have been written.

That may be true if your goal is to advance programming language research, but if your goal is to extend a language being used in industry then you don't have the luxury of spending that sort of design and implementation effort if you suspect that the extension will be a boondoggle (especially since backwards-compatibility promises mean that you'll be forced to support those features for the rest of time).

Also known as "the Scala problem" (and I say that as someone who writes a lot of Scala).

I agree.

I wonder if Rust's compile-time meta-programming can be used to implement 'pluggable' linear-types for experiments, maybe along the lines of [1]. That might be a good compromise.

[1] S. Chang, A. Knauth, B. Greenman, Type Systems as Macros. http://www.ccs.neu.edu/home/stchang/pubs/ckg-popl2017.pdf

I can offer no proof but I'm Pretty Sure that one could hack together linear types using procedural macros, though I can't posit how nice they would be to use nor how well they would interact with the rest of the language and ecosystem.

Wouldn't that be a good path: start with initial experiments based on types-by-macros, and see how well that works. Can't be worse that C++'s template meta-programming.

Ah, but you can fake linear types today! There are ergonomic issues, but it works and it's used in practice.

https://www.reddit.com/r/rust/comments/6a3ac4/the_pain_of_re...

This is really ignoring how relevant and affine types interact with different features. For example, unwinding makes perfect sense with affine, not so with relevant. Rust has unwinding, and no effect system to track whether something can or can't unwind.

I also make it very clear that the implementation is mostly free. It's just using tools we already have with minor tweaks. Most of my issues are exactly the pragmatic matters: your standard library isn't built to handle it, nothing in the ecosystem is built to handle it, and it everyone has to opt into support for backwards compatibility reasons.

As a Scala user: the further I've got into a functional/MLey style the more linear my code has become. Options or collections are very naturally handled with "fold" (cata). Loops probably shouldn't be infinite - if you're looping it's usually because you're folding along a data structure, and those ought to be finite (one of the ideas I'm toying with is a type-level natural indexed recursion-schemes like library, to make it easy to construct recursive structures that are known-finite).

I don't know if it's where Rust wants to be, but I want a practical-oriented ML-family language that does this.

Friendly challenge (because I agree with you, but constantly run into limitations):

I loop over strings a lot. Can I fit them into a nice recursive structure without runtime overhead?

Bonus round: My loops over strings often aren't straight-forward one-byte-at-a-time iterations. Sometimes my loops look at 8 or even 16 bytes in a single iteration. How does that fit in with more sophisticated types like you're describing?

As a typing system developer I suspect there is a hard trade-off / sweetspot between complexity of the types/fold constructs and guarantees that can be enforced by types.

   How does that fit

Probably doesn't and typing systems for general purpose languages will probably have to fall back on general recursion to handle it. And there's nothing wrong with this. Language simplicity is also a virtue. If your recursion is complicated and correctness so important that testing is insufficient, then I recommend post-programming verification with a program logic.

> And there's nothing wrong with this.

Right. I am trying to brighten that line between the sophistication of type systems, the runtime performance of programs and the simplicity of code. I think they are connected in interesting ways, and some of the more rewarding learning I've ever done has consisted of using more sophisticated type system techniques without paying too much on the performance and/or simplicity side of things.

In practice, probably not.

In theory, there's no reason one couldn't compile a linked list in source to a flat array at runtime if the access pattern was right (and linear types should make that kind of optimization a lot more practical. This might even be something one could implement "in userspace" in a language with linear types - like a safe version of an iterator. Certainly I'd be excited to try - I'm not claiming this is immediately production-quality). Or one could ask where the string is coming from in the first place, and trust some kind of fusion-style optimization to remove the intermediate datastructure entirely at runtime.

Peeling off the front 8 or 16 elements should be no harder than peeling off the front 1, though naively you might have to handle each partial case from 1 to 15.

GHC already does a lot of loop fusion and optimizing away of linked lists (which is good given the unfortunate overdue of cons-lists over nicer things among Haskell users) which can be extended to work with user code using rewrite rules. Libraries like text, bytestring, and vector do exactly the elision of intermediate structures that you talk about, allowing you to convert from a vector to a list, apply some function that annoyingly only works with lists, and convert back into a vector, and have that compile into a single tight for-loop in many cases.

I wonder what the upcoming linear types work will do.

> Peeling off the front 8 or 16 elements should be no harder than peeling off the front 1, though naively you might have to handle each partial case from 1 to 15.

I think I under-specified my requirement. :-) By "16 bytes at a time," I mean, "run a single CPU instruction on those 16 bytes."

But yeah, I get your drift. I can see how it might be theoretically possible. I suppose the key gains might be in how much confidence a programmer can have that their code compiles down to the right set of instructions.

Ultimately what we want is a representation that makes it easy to understand the performance characteristics of a given piece of code (and I'd agree that this is an area where the purist functional tradition has lagged behind). In the past assembly was this, but I don't know that it can be these days; I've read that on modern hardware, the biggest factor affecting performance is cache efficiency. So even seeing the sequence of machine instructions might not be enough to allow a developer to reason about performance, because two similar-looking sequences of CPU instructions can easily end up having very different performance characteristics (branch prediction can have a similar effect AIUI).

In the long term I hope for a "nice" language (in particular one in which checked correctness is easy) with explicit performance semantics along the lines of http://www.cs.cmu.edu/~rwh/papers/iolambda/short.pdf . But yeah under the current state of the art there is no ideal approach, so there's a tradeoff in practice even though I don't think there should be one in theory.

You might find Idris's totality checking very interesting, if you haven't already seen it!

http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html...

CMU has a class on Substructural Logics https://www.cs.cmu.edu/~fp/courses/15816-f16/

Up until 2012 it was just about Linear Logic IIRC.

I was actually thinking about this precise issue this morning (due to this GitHub issue[1]). I think a valuable middleground would be to include this kind of check even without the ?Leave stuff. In essence, the compiler could just give an error if it would have needed to issue a Drop call anywhere for the type.

This ability is pretty useful when dealing with destructors that need context that you don't want to always wrap with the given type (sometimes for performance reasons).

[1]: https://github.com/gfx-rs/gfx/issues/1216

The author tries too hard to avoid using the word "object".

"Must use" objects don't seem to be all that useful. More justification is needed. Is the author thinking of Javascript-like callback approaches, broken "promises", and such?

Rust's Result type is a "must use" type, which makes it impossible to skip an error check.

Can you assign it to a variable and then ignore it?

Yes, assignment counts as a use.

That will get you an "unused variable" warning though, which you can suppress by binding to _ instead.

Hardly impossible, just prefix the expression with `[` and suffix with `]` and the warning is gone. Or with `(` and `,)` (creating a tuple of arity one).

> It's poorly named, and so are most of the concepts it introduces

Hostility towards academia check

Anyway it's fine not to have proper linear types in Rust, but I don't think linear types are the enemy here.

Right or wrong, simply saying something is poorly named doesn't show that someone is hostile towards academia. By that standard, most of the academics I know would be hostile to academia, since they invariably think something in their field has a bad name.

Simply saying it is poorly named doesn't, but this sentence:

"Just so you can look this stuff up in The Literature, I'll be providing all these bad names with a Trademark of Disdain™, but otherwise I'd prefer to use Rust-centric terminology." pretty clearly does.

The TM thing is obnoxious.

I think it's it hilarious (and true that academia often chooses poor names).

Yeah, it would be better with coloring. Or better yet hyperlinking to the relevant Wikipedia pages / papers / memes.

Edit: pages such as https://en.wikipedia.org/wiki/Idempotency_of_entailment, https://en.wikipedia.org/wiki/Monotonicity_of_entailment, https://en.wikipedia.org/wiki/Structural_rule, https://en.wikipedia.org/wiki/Nice_guy, https://en.wikipedia.org/wiki/Linear_logic, https://en.wikipedia.org/wiki/Affine_logic, https://en.wikipedia.org/wiki/Relevance_logic (not sure why "Proper Support" is capitalized, that seems to have no referent)

Hyperlinks allow you to directly look up a term by clicking on it, i.e. are actually useful, whereas trademark symbols are just visual noise. Although of course it is possible to over-link as well, see e.g. the wiktionary FAQ on "wikifying": https://en.wiktionary.org/wiki/Help:FAQ#Wikifying, in practice this doesn't seem to happen; it's more the reverse problem of not putting in enough links.

Literally the only link in the article, on the first use of the Official Terminology, is a link to the wikipedia page that defines all the terms.

And that's not really sufficient; words have a life of their own and take on contextual meanings outside of whatever scope they're introduced in. Case in point, linear types come from linear logic, by Girard, whereas relevant types come from unrelated older work by Belnap and Anderson. The simple act of putting them under one umbrella term, "substructural types", erases the older work and means that the article will focus more on Girard's perspective of logic.

Then the article makes the "discovery" that "People who say they want Linear™ Types In Rust actually just want Proper Support For Relevant™ Types.", which is pretty obvious if you know this historical context, and coins yet another term, must-use types, which unsurprisingly has no ™ after it.

I think I get what you're trying to do, I myself used ™ for a little bit back 6-7 years ago, a little bit before I wrote http://insearchoftheultimateprogramming.blogspot.com/2011/04.... But ™ just isn't effective; even if you think you know what a term means, you can't explain it except by its relationship to other terms. And once you forget what that ™ symbol referred to you're just as clueless as everyone else. Whereas URLs are "resource locators" and actually clarify what you intended.

The bit about erasing seems like a bit of stretch. Belnap taught at least one of his proof theory classes using Restall's "An Introduction to Substructural Logics" as a textbook. (Belnap did make it clear that he didn't think linear logic was relevant to his own philosophical concerns, but that's not the same as saying he bears it some kind of ill-will).

Well, if relevance logic is part of linear logic, and it's a true subsumption relationship, then you're saying Belnap doesn't think relevance logic is relevant anymore. So in other words he's pretty much rejected logic altogether.

I guess it makes sense, his most recent papers are about indeterminism (http://www.pitt.edu/~belnap/futurecontingents.pdf), which logic doesn't handle well, but I'm not quite sure how you'd represent the branching-universe model he uses in a type system. I guess you'd need the history operator he uses, m/h = moment m on history h.

I was referring to the subsumption under substructural logic, not a subsumption under linear logic. Belnap seemed to view linear logic as rather different from his own interests in relevance logic.

I'm just miffed that they're complaining about names that are actual words. How would you like if they were all named after their discoverers, and therefore an a priori undistinguished mishmash of proper names? (cf. separation axioms[1])

[1]: https://en.wikipedia.org/wiki/Separation_axiom

That's pretty funny. I'm sure memorizing the differences between the Hausdorff, the completely Hausdorff, the regular Hausdorff, the normal Hausdorff, the completely normal Hausdorff, and the perfectly normal Hausdorff must be fun.

There are only two hard things in Computer Science: cache invalidation and naming things. —Phil Karlton

oh, and:

The first step towards wisdom is calling things by their right names. —Anonymous Chinese Proverb

There are only two hard things in Computer Science: cache invalidation, naming things, and off-by-1 errors.

It doesn't help to use "actual words" when those words have no discernible relationship to their usage. And I don't just mean "common" usage, but the usage by others in related fields. "affine" and "linear" are commonplace concepts in mathematics, but it is in no way clear how they relate to type systems, let alone what properties a type system has when described as such.

The only other fields I know of where things are as badly named are are abstract algebra (ideal, ring, module) and grammar (infinitive, perfect, accusative). It seems to be no coincidence that type theory straddles the two.

Gankro has a... distinctive writing style. :) He also has a master's in computer science, so if he actually has any enmity for academia it might very well be justified. :P

What I find asinine is that the writer says substructural type systems (the concept which the names of the types are inherited from) are badly named, yet I'm somewhat dubious that he knows anything about them? I certainly don't, and although the relationship between affine types and affine spaces is not immediately obvious to me, the relationship between linear types and linearity is very clear.

Reply on news.ycombinator.com