4 ms·
I first became fascinated by linear [1] and uniqueness [2] types with Clean [3], a purely functional language that handles state and IO without monads. This Ha
by chrisaycock 6y ago
I first became fascinated by linear [1] and uniqueness [2] types with Clean [3], a purely functional language that handles state and IO without monads.
This Haskell extension uses linear types for resource safety and scoped effects [4]. For example, linear types can prevent use-after-free errors. Also, linear-typed arrays can perform in-place updates if there are no external pointers to the data.
Similar to linear types is the affine type, where a value is used at-most once. Rust's borrow checker is based on this notion, so that values are "moved" rather than "copied".
[1] https://en.wikipedia.org/wiki/Uniqueness_type https://en.wikipedia.org/wiki/Uniqueness_type
[2] https://en.wikipedia.org/wiki/Substructural_type_system https://en.wikipedia.org/wiki/Substructural_type_system
[3] https://clean.cs.ru.nl/Clean https://clean.cs.ru.nl/Clean
[4] https://arxiv.org/abs/1710.09756 https://arxiv.org/abs/1710.09756
- dmix 6y agoMan, I wish I understood all of this stuff. I have a general enough notion from digging into Haskell and reading into types (including dependent types). I see the value of uniqueness just from using Typescript and having dumb clashes of type variable names, which may be unrelated. But like a lot of Haskell much of this still goes over my head. I'm so conflicted and my intuition is to leave this to the CS university types and focus on IRL productivity in my own field. But I want to invest more time into FP in the future. I'm also technically a "frontend developer" professionally :p
- roflc0ptic 6y agoI have a degree in geography, and learned to do web development largely on the job. It took me about 5 years before I ventured into learning functional programming, and in retrospect, I feel I could’ve been 5 years farther ahead today. It makes you a better programmer, and while it might only make you marginally better at the tasks you currently do, it will open up a wide expanse of other possibilities you didn’t think yourself capable of.
- whateveracct 6y ago> it will open up a wide expanse of other possibilities you didn’t think yourself capable of Haskell has a tendency to make every problem seem exactly the same :)
- solomonb 6y ago"Did you try traverse?" :D
- yodsanklai 6y ago> But like a lot of Haskell much of this still goes over my head. It's not that hard, but it's easier to get one concept at a time. I'm less familiar with Haskell, but languages like Scheme/OCaml are routinely used to teach programming to beginners. Also there's no need to see a dichotomy between "IRL productivity" and "CS/FP". Even if you don't use Haskell directly, ideas from FP make their way to mainstream languages, either as constructs, or libraries, or simply programming style. Overall, the more programming paradigms you know, the easier it gets to learn new languages.
- auslegung 6y agoHave you tried purescript? As a frontend developer you might have more opportunity to use it, and it is heavily influenced by Haskell.
- Kaze404 6y agoThere's also Elm.
- auslegung 6y agoI love Elm but if the poster wants Haskell-ish experience purescript is much more similar. Otoh Elm is simpler and therefore might be a better next step. But since they already seem to have Haskell experience I’d generally recommend purescript if they just want to learn. If they’re choosing a technology for a production product then that’s a completely different consideration
- dmix 6y agoI just want to say I concur with this. I don't consider Elm a full alternative to Purescript, even though I understand the draw. Purescript is more in line with the harder core FP or frontend Haskell I was seeking. On another note, Rust does types and pattern matching quite well where I see that as another draw away from Haskell. But I feel like Haskell is the motherland for this stuff so might as well figure it out eventually.
- dmix 6y agoYes I tried Purescript in the early days and it was buggy as hell with little documentation (even blog post tutorials or githubb repos to learn from). So I decided to wait a couple years before checking it out again, which is coming soon I hope...
- didibus 6y agoIt's not as complicated as the lingo. A type is just metadata about variables and values tracked by the compiler on the static code, as it compiles it. Normally types are used to indicate the set of values a variable is allowed to contain or not. And that info can be used by the compiler to detect mismatch in the code, like if a value is being assigned to a variable that doesn't match its type. But like I said, this is all just metadata about variables and values. So what else could you track and enforce? Well you could also track that some values are never assigned to more than one variable. That would be Uniqueness types. A value of such type is supposed to always have a unique variable pointing to it. So you can't have two variables pointing to it, if you did, the compiler would throw an error. Linear types are similar, with some small differences in the edge case. Specifically, you can cast a value that is non linear to be linear. In effect it means a value that is made linear can not have more references to it after it has been made linear, but it could have many references pointing to it from before it was made linear. Where as a value of a unique type would not allow that. To recap, Uniqueness guarantees that a value has no other references to it, while linearity guarantees that no more references can be made to a value. Finally you have Affine types, which are also just a small difference to the above two. One detail I ommited is Linear and Unique types will also fail if the value is never assigned to any variable. They basically enforce that a value having a linear or unique type must be used at least once. An Affine type is like a linear type that doesn't have to be used at all, thus they say it needs to be used at most once. I'll add one more, Ownership types, like in Rust. Those are like a mix of unique and affine. In that a value with an ownership type can only be refered to by its current owner, but doesn't have to be. It's different to unique types in that the owner is free to refer to it many times, but no other owners can refer to it at the same time. So you see, all of this is just lingo to say, could we come up with some constraints around how many references to the same values we're allowed to have. Then create a type for them so we can tell the compiler to enforce those constraints on values of that type. Now it gets complicated to actually find a way to implement a compiler to track these types and enforce their constraints. That's where the research and challenge is. And it's also tricky to figure out how the programming language can use these and how to make them pleasant to use and not feel like annoying constraint that prevent you from doing things easily.
- timhwang21 6y ago
- japgolly 6y ago> linear-typed arrays can perform in-place updates if there are no external pointers to the data. Holy crap! That's amazing and I hadn't thought of that!