> Is manual resource management with linear types a must? Because that's a big bummer. Manual resource management is generally a given in functional languages

> Is manual resource management with linear types a must? Because that's a big bummer. Manual resource management is generally a given in functional languages with linear types. Since your types are linear, you need functions which can destroy your linear types, and generally those functions are called manually. There are certain other approaches you could adopt in a new language -- e.g. you could use C++-like "destructors" where if you don't do anything with a value and it falls out of scope, a function to dispose of the value automatically gets called. I haven't seen that implemented in a functional language with linear types, though. I don't know how well it would play with type inference. Generally, though, linearly typed languages don't worry about this. > Also how is that compare to Rust? Rust doesn't have linear types -- Rust has unique/affine types. An affine value can be used 0 or 1 times (unlike linear values which can only be used exactly 1 time). So in Rust it's possible to "lose" a value by throwing it away or by creating an RC cycle and leaking it. A linear type system wouldn't let you do that. However, Rust does have those automatic destructors which keep you from having to destroy everything manually. > If it's not, is it possible to incorporate it into an existing language with e.g. HM types? HM in and of itself knows nothing about linearity and so you need additional support from the typechecker to implement it. Plenty of languages have extended HM to include linearity, though.