Can someone explain what this means, practically speaking? I know Haskell fairly well, but am not familiar with linear types. These are types that can be used only once, right?
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.
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.)
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.
Any pointers to a comparison between Clean's uniqueness typing and GHC's linear types? And is Rust the motivating factor behind linear types cropping up lately? I see Idris is now getting them as well.
Rust has affine types (can be used no more than once), but not linear types (must be used exactly once). Linear types would be a nice feature for rust, and there's been some discussion about how to add them, but as far as I know there hasn't been any real progress there.
Affine types in Rust are anything with move semantics; for example you can create a method that consumes itself like this:
impl A {
fn use(&mut self) {
// takes a mutable reference to self, so it
// can be used again later
}
fn consume(self) {
// moves self into this function, which means
// it cannot be used again
}
}
I don’t understand how a usage pattern where some variable (representing a semantic object) is said to have an affine type but it can be used more than once. Can you explain how such a type is not just a regular non-substructural type?
Sorry, that wasn't very clear. `&mut self` in the first method ("use") is an example of a non-affine type, `self` in the "consume" method is an affine type which cannot be re-used.
What's the importance of having to use a value? I.e. isn't this the same as discarding it? Or is related to things like resource finalizers — i.e. once you open a file, you have to "consume" it in order for it to be closed?
There are lots of bugs that linear types can prevent. For example, if you have an operation that returns a Result that must be handled, you can use linear types to ensure that it is. You can also use linear types to implement safe memory management (Rust's lifetime system is basically a special case of this), by returning a value from `malloc` which must be used in a call to `free`.
Usually what happens in Rust is that if you don't use an owned allocation, it is automatically freed. However, it is possible to leak memory by making a cycle of heap-allocated structures. Can such cycles be prevented by linear types?
One of the best write-ups on the differences (at a level that is comprehensible to most programmers) is Linearity, Uniqueness, and Haskell by Edsko de Vries.
> is Rust the motivating factor behind linear types cropping up lately?
Philip Wadler wrote "Linear Types Can Change the World!" while he was working on Haskell back in 1990. I vaguely remember there were some mentions of possibly adding it a year or two before Rust was publicly announced, but it seemed like it was going to be far off at the time. I wouldn't be surprised if Rust contributed to a lot of the interest in it - Simon Peyton Jones did specifically say that he had "Rust Envy" for shipping something similar to linear types in one of his talks.
I'm not super well versed on this stuff, but aren't affine types strictly superior? Though I suppose linear types might be better for tracking system resources?
I am fairly well read on substructural type theories, if you could explain what you mean by ‘strictly superior’ then maybe I could formulate some points of interest, but as the question stands, I don’t think there is any justification for claiming that affine types are better than linear types.
As GP alluded to, there’s not really a proper ordering. If you’re talking ease-of-reasoning from a formal methods standpoint, linear types (or ordered types for that matter) are “superior” to affine types. By extension, when compiling to machine code for real-world computing architectures, linear types have advantages. They lend themselves to aggressive compiler optimization, instruction and data cache-friendly access patterns, and automatic parallelization and vectorization opportunities. All of those things boil down to proving equivalence, so the ability to mathematically reason about code has both testing and performance implications.
Affine types are less foreign to most developers. The safe fragment of Rust’s ownership model is an example of an affine type system...and that’s already a bit of a lift for folks new to the borrow checker. Affine types are harder to reason about than linear types, but still much easier to reason about than the Normal [1] (in the proper noun sense) types used in most PLs.
Linear types let you ensure resource cleanup; files flushed/closed, memory freed, radiation-emitter disabled. That's why even in safe Rust code, it's possible to leak memory, and for the program to e.g. shut down without calling the "switch off the radiation emitter" destructor on a medical device.
All of this is performed by destructors/GC cleanup/Drop in most languages.
> That's why even in safe Rust code, it's possible to leak memory
It's possible to leak memory through circular references and lazy evaluation in all languages AFAIK.
> e.g. shut down without calling the "switch off the radiation emitter" destructor on a medical device.
Unsafe unwinding is possible in any language, including one with linear types. If the runtime crashes, there's nothing to guarantee their one-time use.
>All of this is performed by destructors/GC cleanup/Drop in most languages.
Most GC languages don't guarantee that finalisers will run on shutdown, and no languages I'm aware of guarantee that destructors will run. For really safety critical applications it's not enough that it works fine most of the time; it needs to provide an iron-clad guarantee (as e.g. Ada with Spark can provide for many things). When writing a library it's not possible to guarantee the user will use it correctly when the compiler isn't able to enforce this.
>It's possible to leak memory through circular references and lazy evaluation in all languages AFAIK.
In a garbage-collected language, circular references alone aren't enough to cause memory leaks, as if the circle is not referenced transitively from the root object then it will still be collected.
>Unsafe unwinding is possible in any language, including one with linear types. If the runtime crashes, there's nothing to guarantee their one-time use.
That's true and unfortunate. But linear types at least guarantee that with orderly shutdown, every destructor will be called correctly.
There are other ways to release resources in GC languages, and finalisers are not the right way to do it.
In languages like Java, C#, F#, it is quite easy to have a lint check that gives a compiler error when an IAutoCloseable or IDisposable isn't used with a try/using block, just like RAII, with a bit of static analysis help.
Yep, but that doesn't help so much when you're writing a framework or library and want to ensure the user can't mess it up (although current Haskell couldn't help with that either, given there's no way to prohibit the user writing unsafe code).
> Just like in languages like C++ you cannot force stack allocation/global memory segments, which is the only way to make RAII work.
Could you explain a bit more about what you mean here? To me, RAII is about how the constructor is written, and stack allocation/global memory segments are about where the object is created. I don't see any connection between the two.
For example, if I have a class with a custom allocator that allocates from its own arena, I can still do RAII on the members of objects of that class... can't I?
Yeah, but how are you supposed to release the data stored in the area and the owning class, if the destructor doesn't get called?
As an example (ignore possible compile errors),
// in mylib.h
namespace mylib {
template<class allocator = default_arena>
class ArenaString final {
public:
ArenaString();
~ArenaString();
// several String related methods
private:
ArenaAllocator<allocator> stringData;
};
// several utility functions
ArenaString* StringFactory() {
return new ArenaString();
}
}
// now on main.cpp
#include "mylib.h"
void myLeakyFunction()
{
auto strPtr = mylib::StringFactory();
// do something with strPtr
//oops, strPtr is now gone and ArenaString::~ArenaString() won't get called
}
Alternatively, which I think is the main point of your question, one could call something like myArena::clean() somewhere up the call stack to myLeakyFunction.
But then the question about class instances surviving the region as empty shells with a corrupt state in their stringData member data arises.
While this example is made on purpose to illustrate my point, on big code bases (specially with libraries that one doesn't have any kind of control) it can lead to bad code that prevents RAII patterns to work as expected.
Code that most developers on the team won't even realize it is there and probably will spend hours trying to find out what is wrong with the memory management.
OK. So "RAII" means what I meant by RAII (just the constructor technique) plus the rest of the normal memory management approach (destructors). And if it's not stack allocated (or a member of a class that is), you don't get destructors automatically called. I get it.
The only thing I'm left confused about is "global memory segments". How does that fit in? If it's a global it's never destroyed, so you don't have to worry about it? Or did you mean something else?
Well. There goes the library ecosystem until everyone finally realizes this extension doesn't do what they want. sigh
To expand a bit further:
This extension allows annotating function types with linearity information. The problem is that those modified function types control what is allowed to happen inside them. They have no impact on how values are used outside them.
This is the big difference between linear typing and uniqueness typing. Uniqueness typing lets you say "this function is the only thing using this value."
It's possible to use this extension to assemble something sort of like uniqueness, but the ergonomics are pretty awful and no one bothered working through all the ugly details like exception handling in the context of a real application.
I really don't believe this is ever going to be better than existing techniques. But it's absolutely going to make the library ecosystem permanently worse, as lots of packages will get linearity annotations added. Lots of forks will arise without them, for the people who don't want the hassle. Finding the library you actually want is just going to get even more complicated.
I still don't understand how this happened. Every strong objection was just ignored. What's the point of even having a public comment process when it makes no difference to the outcome?
"The centrepiece of our design is to avoid code duplication. Crucially, the same types can be used in linear and non-linear contexts. For example, the linear-base library uses the same types as base. So libraries developed with linear-base will be compatible with libraries developed with base."
The proposal discusses this briefly[1]. The idea seems to be that datatypes themselves remain identical (constructors being linear by default, even with -XNoLinearTypes), but functions are allowed to have more precise signatures.
edit: I'm not knowledgeable enough about this stuff to know if the idea is to just refine the type signature but keep implementations identical, or whether implementations themselves need to change.
Thanks for the pointer! Emphasis mine:
"Because linear functions only strengthen the contract of unrestricted functions, a number of functions of base can get a more precise type. However,
for pedagogical reasons, to prevent linear types from interfering with newcomers' understanding of the Prelude, this proposal does not modify base. Instead, we expect that users will publish new libraries on Hackage including more precisely typed base functions. One such library has already started here."
From the looks of it this isn't done anyway, just a stepping stone to get to the final destination.
Just like value types, modules and concepts in other languages, sometime big bangs require incremental additions to the stable language instead of big bangs.
This is the core argument of the detractors. They say they -XLinearTypes isn't Enough. They want a Big Bang. But it was already very hard work to get this incremental step. A Big Bang is even more work. And the detractors don't have a semblance of an alternative :/ but that hasn't stopped thousands of words of FUD from being spilled online.
* So is it appropriate to say that in linear types a callee says "I will use this exactly once", and in uniqueness types a callee says "I need exclusive access to this"?
* Is there an obvious way to translate from one to the other?
* Rust's type system sounds a lot closer to uniqueness types than linear or affine types. So why do so many people in this thread say that Rust has affine types?
> * Rust's type system sounds a lot closer to uniqueness types than linear or affine types. So why do so many people in this thread say that Rust has affine types?*
Rust enforces exclusive access through ownership, which is orthogonal to linear/affine typing.
Linear types must be used, affine types must be used at most once. Rust's compiler doesn't force code to use types like Futures or Result, at best it emits a warning, so a missing await or match statement can compile without doing what the code is intended to do. In a linear type system, you can mark Futures and Results so that the compiler throws an error when they're created but not consumed by an operation like awaiting or error handling.
It seems inconsistent to claim both
a) this proposal/implementation has bad ergonomics and doesn't solve real problems, and
b) the library ecosystem will become irreparably fragmented as library authors rush to incorporate it or provide linear forks.
Surely if enough people are expending the effort to bring -XLinearTypes to a non-trivial portion of the extant Haskell universe, it is by definition both useful and at least somewhat ergonomic?
It is inconsistent. -XLinearTypes detractors have been making this paradoxical argument for months now. If it's useful, people will use it to build libraries. If it's not, it's all fine.
The FUD from Haskellers depresses me. My consolation is I'll get to build useful shit with -XLinearTypes on GHC mainline now - things detractors told me weren't possible because they were too busy complaining about its imperfection.
It may be inaccurate but it's not inconsistent. Things can sound like a good idea, be embraced enthusiastically by people who haven't had a chance to work with them, and only later reveal serious ergonomic issues once people have a chance to use them in anger.
It seems that you are the one wanting Linear types to be Uniqueness types instead.
> no one bothered working through all the ugly details like exception handling in the context of a real application.
Citation needed?
> it's absolutely going to make the library ecosystem permanently worse, as lots of packages will get linearity annotations added
> Lots of forks will arise without them, for the people who don't want the hassle
How would the situation be different for Uniqueness types?
> I really don't believe this is ever going to be better than existing techniques.
The paper has examples of how it's better than existing method (such at the ST trick). Took me like an hour to read the entire thing months ago.
Strong objections weren't ignored - they just weren't especially compelling. And when pressed for an alternative, nobody could come close to something of the rigor of what was merged.
This entire comment is FUD and the fact that it's at the top of HN is such a PITA. Now I'm gonna have to hear even more people copy-paste argue against the extension instead of making real progress.
This isn't going to make the library ecosystem worse. Please just edit that statement of "fact" out of your comment for all our sakes.
That's all okay though. I'll go make some video games with type-safe manual memory management thanks to this extension :) that's the power of not complaining when things aren't as perfect as you can imagine them.
It's pretty long but it's pretty easy to just random-access read the examples for motivation. Both the Socket and the mutable array examples are great.
FYI, because I know it will be brought up; GHC models linearity differently than Rust, so you can't compare the two against each other, even though you think you would be able to do that.
Rust puts linearity on the types, GHC puts linearity on the arrows.
Want to work on Haskell all day? Co–Star is hiring. Downloaded every 4 seconds, kids compare the app to their therapist, best friend, and a board meeting with the universe. → https://www.costarastrology.com/jobs or email tim (at-squiggle) costarastrology.com
Besides potentially enabling new types of APIs, I simply like that this extension lets you write more precise type signatures. A function with type [a] %1 -> [a] can do less things that a function with type [a] -> [a].
Are there are books/video lectures that explain linear types how they are useful in a programming language?
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. ?
> 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.
>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. ?
I can just speak for myself. Started programming via vocational training (apprenticeship for the title 'computer science expert' in germany) about 4 years ago.
Learned programming with python, which I loved for the productivity it gave me, the whole superpower yadiya. Was assigned some webrelated tasks, so I got in touch with javascript.
My style in these languages was actually 'functional' without me knowing about functional programming - but only to some extent. Mutability, nonstatic typing etc.
So, wanting to become a better programmer, I googled things like "advanced python", which yielded things like decorators, generators and metaclasses. In some video about map, filter and reduce something in me clicked - I didn't want to hide attributes and state in classes and objects anymore. It's not modular, it's not atomic, it's not beautiful.
I came across Rich Hickeys talks [1] and immediately saw that I'm ...home. The paradigms just click with me, I can't imagine falling back to impurity and oop (unless it can't be avoided for whatever reasons). (I still don't write clojure though, for now I'm still enjoying playing around in python and haskell where I can (you may substitute python with js))
And, honestly - if you have the curiosity to learn Haskell, do you really need a phd? I've taught myself bits of maths in the last four years (higher mathematics - number theory (not tech related, just curiosity), graph theory, category theory etc), just driven by curiosity. That being said: If you'd ask me about these topics on the street, I wouldn't claim to be a mathematician, far from it. I just satisfied my curiosity.
I want to understand. Not some math or haskell in specific, but life, logic, control flow, systems theory... Having this urge, diving deeper into mathematical concepts once you need them doesn't feel like a burden. I don't even have my A-levels, so I'm probably as far from a phd as you'll find on HN, but that wouldn't stop me from exploring, from learning, from progress.
Sorry if that was too personal and too much text, I just felt like I'm in the rare position to be able to answer something in depth on HN :-)
> Are there are books/video lectures that explain linear types how they are useful in a programming language?
Just to throw out an example of how they are useful: loads of Ethereum contracts (e.g. every ERC20 variant) track a kind of private assets (tokens). A big class of bugs is double-spend or double-store of these assets, since any instance of that kind of behaviour completely invalidates the contract.
As it turns out, linear types[0] are just the tool to prevent those bugs.
knowledge about haskell tends to be presented in a "first principles" fashion for whatever reason, which is unfortunate. It's not a very pedagogically sound method. I think it has to do with the systematic temperament of most haskell programmers. But motivation and example should really come first.
The important thing is to not be intimidated. You can really get away with just mimicing code:
main = do x <- getLine
putStrLn ("Hello, " ++ x)
for quite a while before you find that you actually need a proper understanding of the underlying concepts of eg. what monads are and how they work. This is enough to get your classic beginner command line programs running. You can do useful stuff with a very basic understanding. And yet you see people trying to start with
(>>=) :: m a -> (a -> m b) -> m b
pure :: a -> m a
as if that's supposed to be in any way meaningful or useful to a newcomer. The trick is to find the good tutorials that give examples for concepts first, and do a good job of demonstrating why abstracting those examples is a useful thing to do.
I don't find FP those concepts any harder to grok than GoF design patterns (in fact, I've never actually gone through the latter in depth; I just see them mentioned occasionally and have learned some via osmosis).
In fact, those particular concepts you list at the end (monad, monoid, functor) are particularly easy: they're just different ways to think about lists (which we can then generalise to other things). I think the main obstacle is terminology, which makes things feel unfamilar.
For example, two lists can be appended together: programmers do this all the time, so it's a very familar operation; hence it might be useful if we could take this intuition and apply it to other situations. One interesting fact about list append, which we often take for granted, is that nesting doesn't matter, e.g. these will always be the same (modulo runtime: the first traverses 'bar' twice, the second traverses 'foo' twice):
We can capture this idea of "combining where nesting doesn't matter" using an interface, e.g. an OOP programmer might write an 'Appendable' interface with an 'append' method. We can implement 'Appendable' for lists, but we can also implement it for other collections like arrays, sets, or even implementation-specific collections like some 'big data' library that distributes values over a cluster of machines.
An interesting thing happens if we try to implement 'Appendable' for key/value mappings: we have to deal with key collisions (the same key appearing in both mappings). One way to handle this is to always keep values from the first mapping; another way is to always keep values from the second mapping. There's also a third possibility: if the value type is also 'Appendable', we can 'append' the conflicting values together! So far, this seems like a neat little API to expose in a package or standard library.
However, there's nothing about this interface which is specific to collections! We can look through our standard programming toolkit for other things which happen to be 'Appendable' too (AKA "combined where nesting doesn't matter"). One obvious example is numbers: addition is a valid way to 'append' numbers, as are multiplication, 'max' and 'min'. This works well with the key/value example above, e.g. we might have a bunch of mappings which count occurrences of something; we can append those mappings together by adding conflicting counters, to get an overall count of all occurrences; if we instead map keys to the largest observed value of something, we can append those mappings by maxing conflicting values, to get the overall largest values; and so on, as a way to divide and conquer our problems.
Note that averaging is not a valid 'append' for numbers since nesting matters, e.g.
The name 'append' doesn't quite capture what's going on here, but it makes sense if we squint a little.
Another form of 'Appendable' value is "optional" or "erroneous" results (e.g. Maybe<T>, Option<T>, Try<T>, Either<Error, T>, ParseResult<T>, etc.). To 'append' two such values together we check the first one to see if it succeeded: if so we return it, otherwise we return the second. (Note that this faces the same ambiguity a...
71 comments
[ 2.9 ms ] story [ 126 ms ] threadI liked this paper:
http://www.cs.utexas.edu/~hunt/research/hash-cons/hash-cons-...
And previous discussion: https://news.ycombinator.com/item?id=20369522
Simon Peyton Jones talk: https://www.youtube.com/watch?v=t0mhvd3-60Y
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.)
Affine types in Rust are anything with move semantics; for example you can create a method that consumes itself like this:
Obviously it's not part of the type system itself, but doesn't the must_use attr get pretty close?
1 - http://edsko.net/2017/01/08/linearity-in-haskell/
Philip Wadler wrote "Linear Types Can Change the World!" while he was working on Haskell back in 1990. I vaguely remember there were some mentions of possibly adding it a year or two before Rust was publicly announced, but it seemed like it was going to be far off at the time. I wouldn't be surprised if Rust contributed to a lot of the interest in it - Simon Peyton Jones did specifically say that he had "Rust Envy" for shipping something similar to linear types in one of his talks.
Linear Types can Change the World!: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.5...
Affine types are less foreign to most developers. The safe fragment of Rust’s ownership model is an example of an affine type system...and that’s already a bit of a lift for folks new to the borrow checker. Affine types are harder to reason about than linear types, but still much easier to reason about than the Normal [1] (in the proper noun sense) types used in most PLs.
[1] https://en.wikipedia.org/wiki/Substructural_type_system
All of this is performed by destructors/GC cleanup/Drop in most languages.
> That's why even in safe Rust code, it's possible to leak memory
It's possible to leak memory through circular references and lazy evaluation in all languages AFAIK.
> e.g. shut down without calling the "switch off the radiation emitter" destructor on a medical device.
Unsafe unwinding is possible in any language, including one with linear types. If the runtime crashes, there's nothing to guarantee their one-time use.
Most GC languages don't guarantee that finalisers will run on shutdown, and no languages I'm aware of guarantee that destructors will run. For really safety critical applications it's not enough that it works fine most of the time; it needs to provide an iron-clad guarantee (as e.g. Ada with Spark can provide for many things). When writing a library it's not possible to guarantee the user will use it correctly when the compiler isn't able to enforce this.
>It's possible to leak memory through circular references and lazy evaluation in all languages AFAIK.
In a garbage-collected language, circular references alone aren't enough to cause memory leaks, as if the circle is not referenced transitively from the root object then it will still be collected.
>Unsafe unwinding is possible in any language, including one with linear types. If the runtime crashes, there's nothing to guarantee their one-time use.
That's true and unfortunate. But linear types at least guarantee that with orderly shutdown, every destructor will be called correctly.
In languages like Java, C#, F#, it is quite easy to have a lint check that gives a compiler error when an IAutoCloseable or IDisposable isn't used with a try/using block, just like RAII, with a bit of static analysis help.
A new without delete, not only causes a memory leak, it also leaks whatever else could be released by the destructor.
Same applies to Rust when heap memory gets forgotten.
Could you explain a bit more about what you mean here? To me, RAII is about how the constructor is written, and stack allocation/global memory segments are about where the object is created. I don't see any connection between the two.
For example, if I have a class with a custom allocator that allocates from its own arena, I can still do RAII on the members of objects of that class... can't I?
As an example (ignore possible compile errors),
Alternatively, which I think is the main point of your question, one could call something like myArena::clean() somewhere up the call stack to myLeakyFunction.But then the question about class instances surviving the region as empty shells with a corrupt state in their stringData member data arises.
While this example is made on purpose to illustrate my point, on big code bases (specially with libraries that one doesn't have any kind of control) it can lead to bad code that prevents RAII patterns to work as expected.
Code that most developers on the team won't even realize it is there and probably will spend hours trying to find out what is wrong with the memory management.
The only thing I'm left confused about is "global memory segments". How does that fit in? If it's a global it's never destroyed, so you don't have to worry about it? Or did you mean something else?
To expand a bit further:
This extension allows annotating function types with linearity information. The problem is that those modified function types control what is allowed to happen inside them. They have no impact on how values are used outside them.
This is the big difference between linear typing and uniqueness typing. Uniqueness typing lets you say "this function is the only thing using this value."
It's possible to use this extension to assemble something sort of like uniqueness, but the ergonomics are pretty awful and no one bothered working through all the ugly details like exception handling in the context of a real application.
I really don't believe this is ever going to be better than existing techniques. But it's absolutely going to make the library ecosystem permanently worse, as lots of packages will get linearity annotations added. Lots of forks will arise without them, for the people who don't want the hassle. Finding the library you actually want is just going to get even more complicated.
I still don't understand how this happened. Every strong objection was just ignored. What's the point of even having a public comment process when it makes no difference to the outcome?
"The centrepiece of our design is to avoid code duplication. Crucially, the same types can be used in linear and non-linear contexts. For example, the linear-base library uses the same types as base. So libraries developed with linear-base will be compatible with libraries developed with base."
edit: I'm not knowledgeable enough about this stuff to know if the idea is to just refine the type signature but keep implementations identical, or whether implementations themselves need to change.
[1] https://github.com/ghc-proposals/ghc-proposals/blob/master/p...
Just like value types, modules and concepts in other languages, sometime big bangs require incremental additions to the stable language instead of big bangs.
Though job. :\",
* Is there an obvious way to translate from one to the other?
* Rust's type system sounds a lot closer to uniqueness types than linear or affine types. So why do so many people in this thread say that Rust has affine types?
Rust enforces exclusive access through ownership, which is orthogonal to linear/affine typing.
Linear types must be used, affine types must be used at most once. Rust's compiler doesn't force code to use types like Futures or Result, at best it emits a warning, so a missing await or match statement can compile without doing what the code is intended to do. In a linear type system, you can mark Futures and Results so that the compiler throws an error when they're created but not consumed by an operation like awaiting or error handling.
Surely if enough people are expending the effort to bring -XLinearTypes to a non-trivial portion of the extant Haskell universe, it is by definition both useful and at least somewhat ergonomic?
The FUD from Haskellers depresses me. My consolation is I'll get to build useful shit with -XLinearTypes on GHC mainline now - things detractors told me weren't possible because they were too busy complaining about its imperfection.
They are clearly a minority though. But very vocal.
It seems that you are the one wanting Linear types to be Uniqueness types instead.
> no one bothered working through all the ugly details like exception handling in the context of a real application.
Citation needed?
> it's absolutely going to make the library ecosystem permanently worse, as lots of packages will get linearity annotations added > Lots of forks will arise without them, for the people who don't want the hassle
How would the situation be different for Uniqueness types?
The paper has examples of how it's better than existing method (such at the ST trick). Took me like an hour to read the entire thing months ago.
Strong objections weren't ignored - they just weren't especially compelling. And when pressed for an alternative, nobody could come close to something of the rigor of what was merged.
This entire comment is FUD and the fact that it's at the top of HN is such a PITA. Now I'm gonna have to hear even more people copy-paste argue against the extension instead of making real progress.
This isn't going to make the library ecosystem worse. Please just edit that statement of "fact" out of your comment for all our sakes.
That's all okay though. I'll go make some video games with type-safe manual memory management thanks to this extension :) that's the power of not complaining when things aren't as perfect as you can imagine them.
https://www.microsoft.com/en-us/research/uploads/prod/2017/1...
It's pretty long but it's pretty easy to just random-access read the examples for motivation. Both the Socket and the mutable array examples are great.
Rust puts linearity on the types, GHC puts linearity on the arrows.
https://imgur.com/s0Mxhcr
https://skillsmatter.com/skillscasts/11067-keynote-linear-ha...
https://www.youtube.com/watch?v=t0mhvd3-60Y
https://www.youtube.com/watch?v=uxv62QQajx8
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. ?
> 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.
I can just speak for myself. Started programming via vocational training (apprenticeship for the title 'computer science expert' in germany) about 4 years ago.
Learned programming with python, which I loved for the productivity it gave me, the whole superpower yadiya. Was assigned some webrelated tasks, so I got in touch with javascript.
My style in these languages was actually 'functional' without me knowing about functional programming - but only to some extent. Mutability, nonstatic typing etc.
So, wanting to become a better programmer, I googled things like "advanced python", which yielded things like decorators, generators and metaclasses. In some video about map, filter and reduce something in me clicked - I didn't want to hide attributes and state in classes and objects anymore. It's not modular, it's not atomic, it's not beautiful.
I came across Rich Hickeys talks [1] and immediately saw that I'm ...home. The paradigms just click with me, I can't imagine falling back to impurity and oop (unless it can't be avoided for whatever reasons). (I still don't write clojure though, for now I'm still enjoying playing around in python and haskell where I can (you may substitute python with js))
And, honestly - if you have the curiosity to learn Haskell, do you really need a phd? I've taught myself bits of maths in the last four years (higher mathematics - number theory (not tech related, just curiosity), graph theory, category theory etc), just driven by curiosity. That being said: If you'd ask me about these topics on the street, I wouldn't claim to be a mathematician, far from it. I just satisfied my curiosity.
I want to understand. Not some math or haskell in specific, but life, logic, control flow, systems theory... Having this urge, diving deeper into mathematical concepts once you need them doesn't feel like a burden. I don't even have my A-levels, so I'm probably as far from a phd as you'll find on HN, but that wouldn't stop me from exploring, from learning, from progress.
Sorry if that was too personal and too much text, I just felt like I'm in the rare position to be able to answer something in depth on HN :-)
[1] https://github.com/tallesl/Rich-Hickey-fanclub#talks
Some more links that I used:
Functor, aplicative, and monad:
https://typeslogicscats.gitlab.io/posts/functor-applicative-...
Category theory for programmers:
https://www.youtube.com/watch?v=I8LbkfSSR58&list=PLbgaMIhjbm...
Just to throw out an example of how they are useful: loads of Ethereum contracts (e.g. every ERC20 variant) track a kind of private assets (tokens). A big class of bugs is double-spend or double-store of these assets, since any instance of that kind of behaviour completely invalidates the contract.
As it turns out, linear types[0] are just the tool to prevent those bugs.
[0]: https://github.com/flintlang/flint/blob/master/proposals/000...
Just get a book like "ML for the Working Programmer", and go through it and its exercises.
https://www.cl.cam.ac.uk/~lp15/MLbook/
Then either follow up with SML books,
http://www.smlnj.org/doc/literature.html#books
Or jump nicely into Haskell with " Learn You a Haskell"
http://learnyouahaskell.com/
The important thing is to not be intimidated. You can really get away with just mimicing code:
for quite a while before you find that you actually need a proper understanding of the underlying concepts of eg. what monads are and how they work. This is enough to get your classic beginner command line programs running. You can do useful stuff with a very basic understanding. And yet you see people trying to start with as if that's supposed to be in any way meaningful or useful to a newcomer. The trick is to find the good tutorials that give examples for concepts first, and do a good job of demonstrating why abstracting those examples is a useful thing to do.In fact, those particular concepts you list at the end (monad, monoid, functor) are particularly easy: they're just different ways to think about lists (which we can then generalise to other things). I think the main obstacle is terminology, which makes things feel unfamilar.
For example, two lists can be appended together: programmers do this all the time, so it's a very familar operation; hence it might be useful if we could take this intuition and apply it to other situations. One interesting fact about list append, which we often take for granted, is that nesting doesn't matter, e.g. these will always be the same (modulo runtime: the first traverses 'bar' twice, the second traverses 'foo' twice):
We can capture this idea of "combining where nesting doesn't matter" using an interface, e.g. an OOP programmer might write an 'Appendable' interface with an 'append' method. We can implement 'Appendable' for lists, but we can also implement it for other collections like arrays, sets, or even implementation-specific collections like some 'big data' library that distributes values over a cluster of machines.An interesting thing happens if we try to implement 'Appendable' for key/value mappings: we have to deal with key collisions (the same key appearing in both mappings). One way to handle this is to always keep values from the first mapping; another way is to always keep values from the second mapping. There's also a third possibility: if the value type is also 'Appendable', we can 'append' the conflicting values together! So far, this seems like a neat little API to expose in a package or standard library.
However, there's nothing about this interface which is specific to collections! We can look through our standard programming toolkit for other things which happen to be 'Appendable' too (AKA "combined where nesting doesn't matter"). One obvious example is numbers: addition is a valid way to 'append' numbers, as are multiplication, 'max' and 'min'. This works well with the key/value example above, e.g. we might have a bunch of mappings which count occurrences of something; we can append those mappings together by adding conflicting counters, to get an overall count of all occurrences; if we instead map keys to the largest observed value of something, we can append those mappings by maxing conflicting values, to get the overall largest values; and so on, as a way to divide and conquer our problems.
Note that averaging is not a valid 'append' for numbers since nesting matters, e.g.
However, if we keep a pair of total/count, they can be 'appended' by adding separately (and not reducing), e.g. The name 'append' doesn't quite capture what's going on here, but it makes sense if we squint a little.Another form of 'Appendable' value is "optional" or "erroneous" results (e.g. Maybe<T>, Option<T>, Try<T>, Either<Error, T>, ParseResult<T>, etc.). To 'append' two such values together we check the first one to see if it succeeded: if so we return it, otherwise we return the second. (Note that this faces the same ambiguity a...