HN Theater @HNTheaterMonth

Talks that might be informative for the curious:

https://www.youtube.com/watch?v=t0mhvd3-60Y

https://www.youtube.com/watch?v=uxv62QQajx8

SPJ usually makes great introductions about new things being introduced to GHC. Here's one about linear types: https://www.youtube.com/watch?v=t0mhvd3-60Y

> How do people that don't have PhDs bridge the gap in their knowledge from what's commonly taught/used (OOP and it's design patterns) to thinking in terms of monads/monoids/functors/etc.

In my own experience, you just practice, and munch new knowledge bits by bits. The crucial point here is that you don't need to know _all_ of haskell to be productive using it.

So you learn the basics, start using monads without understanding the Monad abstraction (it's really not something you need to understand to use), and after a while it just clicks. And once you're confortable with this basic knowledge, you learn new things when you need them.

As a result, I (and many other paid haskellers) have a job writing haskell without having a PhD, without learning category theory, or without a deep math bagage.

My understanding is that the current implementation is only groundwork for possible future performance benefits, since there are no changes to the runtime system or garbage collector, and that their current intended use is mostly for allowing library authors to encode safe session/resource handling in the type system. So, new libraries can make it a type error to fail to properly close a connection or release a shared resource.

Simon Peyton Jones talk: https://www.youtube.com/watch?v=t0mhvd3-60Y

⬐ whateveracct

You can write safe memory management libraries in userspace with the existing extension. That can help reduce GC pressure by moving data off-heap and allow for safer & more efficient FFI bindings.

As someone who has been exploring doing gamedev in Haskell, that all is very exciting and the use-cases are constantly obvious to me.

It is entirely up to userspace to leverage this new feature. It doesn't do anything on its own outside of the type-checker. And to use it, your library will probably have to do some unsafe coercion under the hood (just like ST uses unsafePerformIO under the hood to do pure mutability.)

⬐ dllthomas

Right, my understanding is that in a sense it doesn't "enable new performance", because operationally speaking it's all stuff you could do anyway. What it does is move a lot of potential approaches from "absurdly unsafe" to "perfectly fine", so whatever your threshold for safety it's likely to move some speed improvements over the line if you care much about speed.

Session Types, AFAIU are a specific implementation of a linear logic in some type system and I am not all too familiar with them in practice. However, I would like to think I am well versed in Linear Logic and Substructural Type Theory. I think the works by Wadler are a good place to start, in particular is a sort of review paper, based in intuitionistic logic (which he also covers in said paper), on linear logic. It’s called ‘A Taste of Linear Logic’ (I actually have the paper open in Safari on my iPhone as I type this) and it is written as a sort of primer on the area. Wadler’s bibliographies on the works contained in the pages you linked are a good source as well. If you are at all coming from a place of familiarity with Haskell, a decent overview of the current discussions on Linear Types in functional languages is at [2]. And lastly, if you like videos, Simon Peyton Jones has a great talk on YouTube [3] where he discusses practical linear types for Haskell, but the theory is not Haskell specific.

I will warn you that the latter two references make several arguments and then discuss uniqueness typing (which is related but very different) and that is a whole other rabbit hole of sources, but generally a good topic to dig into as well.

[1] https://homepages.inf.ed.ac.uk/wadler/papers/lineartaste/lin...

[2] http://edsko.net/2017/01/08/linearity-in-haskell/

[3] https://youtu.be/t0mhvd3-60Y

Simon Peyton Jones initial intuition [0] was that Rust would be full of soundness holes due to not starting with a full formalization. Derek Dryer, Ralf Jung and others in the RustBelt project [1] did amazing work in formalizing Rust's safety guarantees, showing that Peyton Jones' guess was not accurate.

There is nothing wrong about having bugs, of course, but the reaction to the bug in this thread shows that mathematical correctness is not as universally valued as I thought it would be. I agree with the sentiment that this is a bigger issue that shouldn't be discussed in a technical thread about a specific bug. However, after reading this, it is unclear to me whether mathematical correctness is regarded in the Rust project as an explicit goal, an explicit non-goal or an unessential nice-to-have. (I do not mean to insinuate anything with the word "unclear", as I believe all three options are valid and appeal to different use cases. Almost all of the popular languages don't care about this, for instance.)

[0] https://youtu.be/t0mhvd3-60Y?t=130 [1] https://plv.mpi-sws.org/rustbelt/

⬐ fluffything

Two of Rust goals are:

* Hack without fear (which can be interpreted as soundness) * Practical programming language (a language you can use to get stuff done)

A full operational semantics of Rust with soundness proofs is probably at least a decade away, blocking the language on that would mean that one can't get anything done until that happens. And that is at tension with Rust being a practical language.

So if you had a spectrum of languages, and you were to classify them along these two axes, Rust would be at the very safe and very practical end of the spectrum. But safety isn't an absolute, it's a spectrum. Rust won't protect you form, e.g., race conditions, dead locks, memory leaks, or somebody breaking into your house and hitting your computer with a baseball bat, etc. You need to have a threat model, and then deduce from it how much safety is enough. Rust aims to only give you memory and thread safety, so there is definitely room for much safer languages than Rust down the road, that protect you from these other things. The art is increasing safety, without sacrificing practicality, performance, etc.

⬐ dethinking

Not sure if you caught it, but Ralf does address this somewhat in the thread:

> Good question. We even had a sketch of a formal model for pinning, but that model was always about the three separate pointer types (PinBox<T>/PinMut<T>/Pin<T>). The switch to the generic Pin was done without formal modelling.

> Actually trying to prove things about Pin could have helped, but one of our team actually did that over the summer and he did not find this issue. The problem is that our formalization does not actually model traits. So while we do have a formal version of the contract that Deref/DerefMut need to satisfy, we cannot even state things like "for any Pin<T> where T: Deref, this impl satisfies the contract"

That does sound scary, but I think the point is that this is a known blind spot in the formal model. It also has a known solution; the trait ought to be unsafe, so that the implementor takes responsibility for upholding the contract. The issue with Pin is it’s using an existing, safe trait, on the informal assumption that it couldn’t be unsoundly aliased by users. (Of course that turns out to be false.)

So you can look at that and say “an unsound feature got into the stdlib without passing formal verification”, and that’s true, speaking to a lack of concern for formalization.

On the other hand, you could look at it and say “the unsoundness of this feature is well isolated by formal methods and leakage at this interface is not the end of the world”, which is also true, and speaks to the utility of the formal work that has been done.

It seems clear to me that the answer for Rust is “balance”. Formal verification is important not not to have, and things that can’t be verified shouldn’t be allowed. But formal verification takes up time when everything could be working 100% in production, and the alternative is likely even less sound formally, so it’s better to build an API now with some known risks than to wait for something known to be risk-free.

Whatever your personal philosophy is, it seems clear that toeing that line has been instrumental to Rust’s success.

⬐ lidHanteyk

I would say that SPJ was quite right, though. Compare and contrast with Haskell. In Haskell, there are broadly only three cases of unsoundness:

* Infinite loops

* `undefined`

* Abuse of unsafe IO behavior, including monads built on or reducible to IO

Rust's unsoundness bugs are all over [0], and come from so many different angles that they feel indistinct from any other low-level C-like language.

I looked a little into RustBelt; how would it have helped this `Pin` issue? I browsed [1] a bit and it seems like `Pin` would have to have been proven on its own in an ad-hoc way not covered by RustBelt.

[0] https://github.com/rust-lang/rust/labels/I-unsound%20%F0%9F%...

[1] https://gitlab.mpi-sws.org/iris/lambda-rust/tree/popl18

⬐ rapsey

You are being very disingenuous. Rust does not have unsound bugs all over stable. Linking to an issue tracker for bugs in development branch proves nothing.

⬐ kibwen

As a Rust user, I think it's fine for the grandparent commenter to link to the I-unsound tag; even if some of those bugs are only accessible on the unstable nightly release, there are plenty of soundness bugs to choose from on the stable releases. The important thing is Rust's philosophy that soundness issues are to be taken seriously, even going so far as to allow backwards-incompatible changes if necessary to address them (though obviously this is a situation of last resort).

There are several people working on formalizing aspects of Rust, and though it will take a long time to get there such efforts have already found and fixed bugs in Rust and its standard library. It's fair to take SPJ's critique on the chin for now; Rust deliberately chose the path of eventual soundness in order to produce a usable language in less time, and as long as we keep working towards that goal there's nothing to be ashamed about.

⬐ dranov

> I looked a little into RustBelt; how would it have helped this `Pin` issue? I browsed [1] a bit and it seems like `Pin` would have to have been proven on its own in an ad-hoc way not covered by RustBelt.

To clarify, we do have a work-in-progress formalization of pinning as part of RustBelt [0] (I worked on it over the summer). We did not discover this issue because RustBelt does not currently model traits, and the problem here is very much about the interaction between traits and pinning. Ralf touches on this in the linked discussion:

> Actually trying to prove things about Pin could have helped, but one of our team actually did that over the summer and he did not find this issue. The problem is that our formalization does not actually model traits. So while we do have a formal version of the contract that Deref/DerefMut need to satisfy, we cannot even state things like "for any Pin<T> where T: Deref, this impl satisfies the contract".

[0] - https://gitlab.mpi-sws.org/iris/lambda-rust/tree/gpirlea/pin...

⬐ steveklabnik

> However, after reading this, it is unclear to me whether mathematical correctness is regarded in the Rust project as an explicit goal, an explicit non-goal or an unessential nice-to-have. (I do not mean to insinuate anything with the word "unclear", as I believe all three options are valid and appeal to different use cases.)

It's a balance. We cannot drop everything, nor stop all development, in order to get proofs. However, we are actively working toward formalizing the language itself, because we do see value in it.

⬐ fluffything

> We cannot drop everything, nor stop all development, in order to get proofs.

That kind of contradict some of the reactions, e.g., in this thread about adding an `Ordering::Unordered` to the language: https://internals.rust-lang.org/t/unordered-as-a-solution-to...

Where it is essentially argued that "all development should be stopped until we have formal proofs".

I guess it depends on which parts of the language things touch. `Ordering::Unordered` touches fundamentals parts of the memory model, and well, `Pin` touches the fundamental kinds of values that Rust has: owned, shared, mut shared, and with pin, also pinned.

When people complain that things are stabilized too quickly, I don't think they complain about async / await taking years. The `Pin` API was unstable for like less than half a year in its final form before being stabilized, that's quite a short time for people to try to find holes in it, given how fundamental it is.

⬐ kibwen

Ralf is the one writing the soundness proofs (and bless him for doing so), but I don't believe that he's actually on the language team, so I wouldn't interpret that as an official stance.

⬐ steveklabnik

Team members can have their own opinion, of course. That is exactly what is happening in that thread, though Mazdak is the only language team member arguing that position. I personally wouldn't characterize this as "all development should be stopped until we have formal proofs," though, this argument is "if we commit to this API we will be locked out of one particular model and I'm not sure that we should be making that kind of decision yet."

Empirically it's pretty clear that the language is being developed. If that were the decision of the team, it would pretty much have to go through an RFC, and so we'd be able to point to that.

⬐ majewsky

If the formalization discovers more (or more significant) soundness holes, would that be a possible reason for a Rust 2.0 release?

⬐ steveklabnik

In theory, if there were incredibly massive holes that affected most Rust code and could not be fixed without backwards-incompatible changes, I guess so. Details matter in cases like these. It would just depend.

⬐ kibwen

This was something that kept me up at night in the run-up to Rust 1.0 and beyond (dreadful memories of the leakpocalypse), but so far we seem to have been quite lucky in that nobody has yet discovered a dramatic and fundamentally damning soundness flaw (and the progress of formal verification since 1.0 has increased confidence somewhat in the absence of such a flaw, but `Pin` represents a rather hairier increase in surface area than is usual... fingers crossed :P ).

⬐ mauricioc

Totally reasonable stance, in my opinion, since Rust moves quickly and formalizing things takes time. But what is the stance on soundness bugs? Are they sometimes acceptable as permanent parts of the language, or is it a goal to eventually fix any soundness bugs that show up?

⬐ devit

Not sure about the exact official stance, but can't imagine it's anything other than eventually fixing all soundness bugs, at least as long as someone is willing to do the work.

However, an important thing to note is that Rust strives to be safe only against unintentional bugs, and not against intentional malicious code (against which you are supposed to use OS/CPU-level sandboxing), so unsoundness issues that are very unlikely to be accidentally triggered aren't necessarily a very high priority.

This is a reasonable policy, since current Rust does not have a certified provably correct compiler and Rust programs in current practice don't come with formal proofs, so full provable soundness in type system doesn't really translate to any useful properties, since programs can intentionally fail to do what they are supposed to do in other ways (just do something safe but malicious or incorrect or exploit bugs in rustc or LLVM).

For instance, this issue is very unlikely to be triggered by non-malicious code, so emergency action to fix it is not being taken, and instead it will probably be fixed only once there is clear consensus on the best fix.

⬐ zozbot234

The line between "unintentional" bugs and "intentional/malicious" escape hatches is quite fuzzy given the extent that most Rust projects rely on outside code. Soundness bugs, at least in stable rust, are serious and should be addressed as such, or Rust developers will end up with a leftpad situation as soon as a popular third-party crate 'unintentionally' introduces some sort of soundness concern.

⬐ TheCoelacanth

Stealing credit card numbers, displaying adware and launching missiles are all safe Rust.

Rust does not offer any protection against malicious code and it does not claim to. It offers protection against malicious input to non-malicious code, but no protection against malicious code itself.

⬐ devit

Third party crates can include malicious safe code that doesn't exploit any soundness bugs, so I'm not sure how exploiting soundness bugs could make the situation worse.

It's only a problem if you try to restrict I/O APIs and use the Rust type system as a security boundary, which is something that I don't think anyone does and that should not be done since the surface area is too vast to secure without formal proofs of the whole Rust stack, which are too time-consuming to produce with current technologies.

⬐ __s

https://www.tockos.org does what you think nobody does

⬐ dethinking

TIL, and since it’s buried a bit:

> A capsule is a Rust struct and associated functions. Capsules interact with each other directly, accessing exposed fields and calling functions in other capsules. Trusted platform configuration code initializes them, giving them access to any other capsules or kernel resources they need. Capsules can protect internal state by not exporting certain functions or fields.

> ...

> Rust’s language protection offers strong safety guarantees. Unless a capsule is able to subvert the Rust type system, it can only access resources explicitly granted to it, and only in ways permitted by the interfaces those resources expose. However, because capsules are cooperatively scheduled in the same single-threaded event loop as the kernel, they must be trusted for system liveness. If a capsule panics, or does not yield back to the event handler, the system can only recover by restarting.

I take it from the present discussion that that might not be as good of an idea as they think.

Worth noting that they also have process isolation on top, but it doesn’t seem to be motivated by any potential insecurity of the type system.

⬐ staticassertion

I don't get how that's ever possible, regardless of soundness issues. Can you not simply use unsafe in a capsule, and violate this constraint? The only way isolates in V8 manage to provide any isolation is because the runtime/ language forbid such things entirely.

I suspect it is not so simple as "Rust's safety ensures malicious rust code can't access data".

⬐ __s

Capsules aren't allowed to use unsafe. The target of tock is not generally going to be out of order, so spectre things shouldn't occur

⬐ staticassertion

Is there a doc about that? Can they also not use external crates? Very curious.

⬐ __s

There's a blog post https://www.tockos.org/blog/2017/crates-are-not-safe

Lots of example code https://github.com/tock/tock/tree/master/capsules

⬐ staticassertion

Thank you.

⬐ Narishma

I believe soundness bug fixes are the only things allowed to break backwards compatibility in Rust.

⬐ steveklabnik

Soundness bugs are the only thing we make an exception in our stability policy for. In general, unsoundness is treated as a serious issue. However, "unsoundness" can mean a few different things; in the "semantics of the language" sense, they're taken very seriously. In the "there's a compiler bug" sense, they're taken seriously, but in accordance with how likely they are to affect end users, and how much work they are to fix. For example, an incorrect type signature in the standard library was fixed one day after release by changing it to the correct one and re-releasing; an issue where casting between floating points and integers causes some problems has still not been fixed, because it partially has to do with LLVM's semantics combined with our semantics, and it's not clear how to do the right thing while not seriously regressing performance. (That being said that particular issue has had a flurry of activity in the past week...)

The GitHub label for these bugs is A-Unsound, which has the description "A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/Soundness".

⬐ mauricioc

Compiler bugs are not what I had in mind, so this answer is very reassuring! The original thread led me to believe this was not an absolute, official policy of the Rust project, but I am happy to hear it is.

⬐ steveklabnik

For more details, here's the written part of this: https://github.com/rust-lang/rfcs/blob/master/text/1122-lang...

Please note that threads on internals are able to be posted to by anyone; things expressed there may not represent the way that the team feels about things.

Something to keep in mind - linear types are on their way[1], with exactly this usecase in mind. Simon Peyton Jones gave an excellent presentation on the topic[2], briefly discussing exceptions, as well as giving a mention to ResourceT and the phantom type solution in the article (described as channel-passing).

[1] https://arxiv.org/abs/1710.09756 [2] https://www.youtube.com/watch?v=t0mhvd3-60Y

⬐ thesz

Please, don't add them to the language. Use the library approach instead, it is much more Haskellish.

⬐ fmap

From a language design perspective it makes a lot of sense to add linear types to the language itself instead of using an encoding. Every encoding that I know of (such as region types encoded as monads, which is what I think the article wants to get at) leads to excessive sequentialization of code. This in turn leads to a lot of boilerplate (or crazy type inference problems) at compile time as well as suboptimal run time performance.

Linear types are the perfect example of a feature that belongs in the core language, or at the very least into a core intermediate language. They are expressive, in that you can encode a lot of high-level design ideas into linear types. You can compile a number of complicated front-end language features into a linearly typed intermediate language. Linear types have clear semantics and can even be used for improved code generation. If we ignore the messy question of how best to expose linear types in a high-level language then this is just an all around win-win situation...

⬐ thesz

Have you took a look at Clean the programming language? It has unique types (used for resource management, but less restrictive than linear types) for decades and guess what? They invented special syntax (the "#-notation") which introduce shadowable names much like regular monad syntax does. And code with this syntax is, basically, sequential code most of the time albeit unique types allow for something like "where" clause. You just easily get lost with these handle, handle1, handle2... names.

I do not oppose inferring linear use at core and/or intermediate representation (GRIN allowed for that and more). I just do not see their utility at the high level, in the language that is visible to the user.

⬐ KirinDave

It's extremely difficult to do this and maintain even the figment of usability.

Unless, of course, you're implying it's very haskellish to implement libraries with huge usability gotchas (of which ResourceT was one until the Ghosts of Departed Proofs paper reminded us we can reuse the machinery of ST), then I totally agree.

⬐ thesz

There was an abstract of PhD thesis devoted to enhancing usability of DSeLs by helping with error messages - they had to be expressed in terms of DSeL, not Haskell-the-language. And linear types as a library (be it ResourceT or something other) is a DSeL.

I think it is a better venue which can help many applications simultaneusly. While linear types won't.

⬐ radarsat1

Is it possible? I mean, to add linear types via a library? I feel like it would have been done already if it were.

⬐ Zalastax

It's possible if you have dependent types and are not afraid to (ab)use the type system. See section 2.4 of my thesis (link in bio) for a taste. You have to squint a bit but a system like that can ensure linearity.

⬐ thesz

Linear types amounts to modification of environment - "use" of linear value removes it from environment, so you can't eat cake and still have it. If you look at the use of unique types in Clean, you will see that their use closely reminds monadic code (e.g. "#" syntax). Otherwise you will need to invent variable names like handle1, handle2, handle3... to refer of "modified" handles generated after each use.

You can easily simulate that using parametrized monad: http://blog.sigfpe.com/2009/02/beyond-monads.html

E.g., hClose will have type like (Has listIn h, listOut ~ Del h listIn) => h -> ParamMonad listIn listOut () and hGetLine will result in type much like this one: (Has list h) => h -> ParamMonad list list String

It is not perfect: you still may have reference to handle after it's use and you may be tempted to introduce it somehow back and get run-time error; you also would struggle juggling two handles for copying files, for example (for this you may have to use ST parametrization trick).

But anyway, you really not need linear types all that often (they are cumbersome - I tried to develop language with linear types, type checking rules and types get unwiledy very soon) and when you do, you can have a library. Just like STM, parsers, web content generation/consumption, etc. Linear types do not warrant language change.

⬐ None

None

⬐ bjoli

I am always impressed by what the ocaml/Haskell people can do compared to my language of choice (scheme).

Iirc Oleg Kiselyov implemented proper delimited continuations in ocaml as a library, without touching the runtime or compiler. Something similar has been done in Haskell.

I doubt fully dependent types can be implemented in Haskell without extra help by ghc. There has been lots of work in the area, and last time I checked you could simulate DT to some degree, but it never was as powerful as the dependant types in idris. Iirc t were some edge cases where the typing became undecidable.

⬐ fasquoika

>Iirc Oleg Kiselyov implemented proper delimited continuations in ocaml as a library, without touching the runtime or compiler.

To clarify this, the library you're talking about implements most of the functionality in C, reusing the runtime's exception mechanism. So it doesn't require any upstream change to compiler or runtime, but it also can't be implemented in pure OCaml.

⬐ bjoli

Hmmm. I remembered incorrectly then. The bytecode version is possible in pure ocaml, but for native it apparently needs C.

For Haskell it is however possible. There is a neat paper by among others Kent Dybvig.

⬐ fjsolwmv

What is "the library approach"? Library approaches have failed.

See http://www.well-typed.com/blog/2016/09/sharing-conduit/

⬐ thesz

Look at distributed-process. It is Erlang-in-Haskell without changing the language.

So library approach thrives.

⬐ whateveracct

Haskell language features are importable :)

⬐ klodolph

Haskell has such an extensive set of language extensions, I would say adding new features to the type system is probably the MOST Haskell-ish way of doing things.

The explicit purpose of Haskell is to be a basis for research into functional language design (edit: among other purposes). By "explicit purpose" I mean exactly that... people got together in 1987 to come up with a language for research. Haskell was never supposed to ossify into some kind of "finished product", it was built exactly so people could experiment with things like linear types. If you want to just write libraries and get stuff done with a more or less fixed language, you probably want to be writing OCaml.

I mean, just look at the list of GHC extensions... there are something like a hundred of them! The list is growing longer every year. https://downloads.haskell.org/~ghc/latest/docs/html/users_gu...

⬐ thesz

They are fixing omissions related to full dependent types, many of them.

Compare language features and Haskell's approach: Erlang and distributed-process, goroutines and channels and Control.Concurrent(.Chan), (D)STM is a library, Control.Applicative and Control.Monad for many things hardly expressible in any other language, etc, etc.

Linear types, I am afraid, would go the way implicit parameters went - their use is cumbersome and they really do not help much with day-to-day programming and when they are needed they can be perfectly implemented with a library.

⬐ dang

> What are you talking about?

Please edit swipes like that out of your comments here. The rest is fine and stands on its own.

⬐ ducklingslicks

What are you talking about? I liked his comment.

⬐ klodolph

I would love to edit that out but the two-hour edit window is so short, sometimes.

⬐ dang

I've reopened it for editing if you still want to do that.

⬐ klodolph

Done, thanks.

⬐ agentultra

I do normal, boring line-of-business programming in Haskell every day.

I think Haskell does have a good model for bringing together practical application of theoretical research.

Parent's comment is spreading the myth that Haskell is an academic language. It's not wrong but it's not Haskell's only stated purpose or utility by far.

⬐ jshevek

For what its worth, when I read the parent comment, I did not at all get the impression that it was "spreading the myth that Haskell is an academic language."

⬐ klodolph

I used to do normal, line-of-business programming and I stand by the comment.

If it sounds like I'm saying that Haskell is not useful for boring, line-of-business programs then I wasn't clear... Haskell is a research language, yes, and not exclusively so. But I'm confused why it's objectionable to spread a "myth" if that myth is, in your words, "not wrong". The stated purpose of Haskell, when it was created, is a matter of historical record.

> It should be suitable for teaching, research, and applications, including building large systems.

This, to me, means that we are not going to freeze the language, and sacrifice research, in order to support business applications. That would go against the goals of the language.

Doing everything as a library seems "un-Haskellish" to me because there's an ongoing and vibrant community that's doing research into things like type theory, which can't be done as libraries, and kicking that group of people off the Haskell platform just to support business applications would be a failure of Haskell as a language.

Haskell can support both groups.

⬐ agentultra

The myth that gets circulated by critics of Haskell is that it is an academic language and has no practical use in industry.

I think your post was unclear and supported that myth. After reading your reply I understand better what you meant!

I agree -- extensions do seem to be working rather well. I hope the new Haskell standard, Haskell2020, will include some of them into the language proper!

I'm looking forward to seeing how linear types work/interact with the rest of the language.

⬐ dllthomas

I'm not convinced the current linear types proposals actually let us solve the problem, in the presence of exceptions. I may very well be missing something, or it may be that exceptions are rare enough that leaking resources until garbage collection only when an exception occurs is fine in practice.

⬐ eridius

FWIW Rust doesn't consider leaking an object to be unsafe. In fact, there's a std::mem::forget() function that can be used to do precisely this. Before Rust 1.0 it was marked `unsafe`, but it was determined that the existence of Rc allowed for creating retain cycles in safe Rust, and "fixing" this was prohibitively complicated, and since it was possible to leak values in safe rust, std::mem::forget() was therefore determined to not be unsafe. This was also when "leaking values isn't a violation of safety" was turned into an actual principle, as opposed to just a hunch that a bunch of people had, and the one API that relied on leaking being unsafe was removed (this was the API for scoped threads, which was marked as unstable right before 1.0 came out, and subsequently an alternative stable safe API for doing scoped threads was hashed out in the crates ecosystem).

My personal opinion but this is purely because I enjoy it the most is functional programming. So much of the positive changes I've seen of late come through functional programming.

For example:

* ReasonML - this is what the founder of React is working on now. The ReasonML claims itself to be JavaScript 2030 (I see it as JavaScript + TypeScript + Immutable.JS + Redux). This contains a lot of the concepts from JavaScript so is a reasonable step to make

* If ReasonML isn't too scary it leads you down a path to OCaml, F# and Elm

* Rust (not strictly a functional programming language, but is ridiculously fast and contains well implemented Linear Types that makes Haskell's Simon Peyton-Jones jealous [0]) - this is one of the most loved programming languages according to the Stack Overflow survey

[0]: https://www.youtube.com/watch?v=t0mhvd3-60Y

Here's a great talk by Simon Peyton Jones on integrating linear types into Haskell: https://www.youtube.com/watch?v=t0mhvd3-60Y