15 ms·

Implement with Types, Not Your Brain

103 points by Tehnix 7y ago

Gormisdomai 7y ago
I would really love to see an IDE that auto suggests / autocompletes code based on typed holes like this. Does such a thing exist?
- Jtsummers 7y ago
  Check out Idris and the book Type Driven Development. It has an emacs mode that does that for you. I’m not sure about other languages. It was a very nice experience though I just went through it for the learning experience and haven’t tried to apply it to any problems since then.
- gcommer 7y ago
  Holes in Agda are a good bit more powerful than in Haskell, and agda's emacs mode has a bunch of very powerful commands for working with them, eg: listing possible values, automatically filling, splitting them by case, etc. For example, for this post's "jonk" example I just had to copy the type into emacs, reformat it a bit into Agda syntax, then press C-c C-a and it automatically figured out the solution that the author worked through manually: λ z z₁ z₂ → z₁ (λ z₃ → z₂ (z z₃)) See the full list of commands at https://agda.readthedocs.io/en/v2.5.2/tools/emacs-mode.html https://agda.readthedocs.io/en/v2.5.2/tools/emacs-mode.html
- derefr 7y ago
  Why even have the code? The type is all the compiler needs to spit out a definition. Your source can just be the type.
- pirocks 7y ago
  Intellij can sorta do this for Java if you fo ctrl+shift+space.
- hardwaresofton 7y ago
  Idris does this with a REPL-like interface: https://www.youtube.com/watch?v=mOtKD7ml0NU https://www.youtube.com/watch?v=mOtKD7ml0NU
kazinator 7y ago
> Which means you can slowly use type holes to chip away at a difficult implementation, without ever really knowing what you're doing. Yeah, look! I started with a function signature and a little _. Lo and behold, fifty seven holes later, I have a graph-coloring optimal register allocator for MIPS for my compiler back end. Don't ask me how it works, but the type system assures it.
- state_less 7y ago
  This type system, is it powered by AI?
  - mrkeen 7y ago
    There's nothing fuzzy going on. If I said f(x) = 2, you could quickly work backwards from that and state: 2 is an Int. x isn't used so it could be any type, let's say a. That means f has type (a -> Int).
- mrkeen 7y ago
  This, but unironically.
dan-robertson 7y ago
I read the argument in the article as something like “strong advanced type systems like Haskell’s are good because instead of manually writing hard functions, one can just write the type (ie the meaning of the function) and do a bunch of menial compiler-directed work to build up one’s function in little steps. This is great because one doesn’t need to “actually” write such horrible functions. I find it slightly silly because one still has to read such functions so it is still hard to know that they do the right thing. For example, consider the function in the article which has type: Sem (State s ': r) a -> S.StateT s (Sem r) a It seems pretty obvious what this morally should do. In some cases it is possible for polymorphism to force a value of a certain type to always behave a certain way. E.g. a value of type [a] must be the empty list because that is the only value with that type. On the other hand there are multiple values of type [[a]] (I.e. an empty list or an infinite list of empty lists or anything in between). A more complicated example is that the only thing a function with the signature of compose ((b -> c) -> (a -> b) -> (a -> c)) can do is compose functions whereas a function of type (Int-> Int) -> (Int-> Int) -> (Int -> Int) can do just about anything. Outside of abstract Haskell libraries, code tends to look more like the second case than the first. In this case it is hard to be sure that the function must behave in the correct way because of its type. I think it hinges on whether it is possible for Put to change the type of the state. If it can then types force you to always take the newly put value and return it with Get, otherwise it would be possible for Put to eg only sometimes work. So if one has to check that the code is correct, one must either read very carefully and check the code, or one must very carefully read the type signature and deduce that the code is correct. In the first case the fact that the compiler made the code easy to write doesn’t really help much. Perl5 taught us that just because a program was easy to write it does not mean it will be easy to read/check. In the second case, why do we have a program at all? If there is only one correct program we could have written then it seems to me that the program is in fact the type and the compiler ought to have been more clever and written it itself. (There are of course plenty of issues with that statement). It seems to me that claiming “Haskell is great because it helps automatically write difficult functions which are impossible to check” or “Haskell is great because it makes me do the manual steps in writing a function that can only ever do one thing and mixes that pointless code in with the thing I care about” is a bit silly. This all being said, I do think holes are a useful feature but I don’t think they are useful for entirely writing a function for you. They are particularly useful in proof assistants like Agda where one must manually exhibit a million trivial propositions and holes help fill in all the boring gaps. Agda doesn’t really suffer from the “multiple things a type could mean” issue.
mpweiher 7y ago
This piqued my interest, because that's the same way TDD works for me. And then it starts with "Let's go through an example together. Consider the random type signature that I just made up:" Hmm...I never have a type signature as a starting point, random or not. I have some sort of requirement, some sort of functionality I want out of the code. Soft fuzzy requirements. And the types rarely if ever tell me what the function does. Heck, a function that's int x int -> int could be just about anything. How about string -> int? Does it convert the string to an integer or count the vowels?
- golergka 7y ago
  > Heck, a function that's int x int -> int could be just about anything. How about string -> int? That's because using types like "int" and "string" is not a real, valid use of a good type system. Instead, you'd typically have a function type of `newton -> sqMeter -> pascal`, or `username -> accessLevel`. All these types would be implemented through basic int and string types, but declaring them explicitly with very limited conversions inbetween would actually use type system to verify correctness of your code.
  - mpweiher 7y ago
    So you're going to not have arithmetic or string manipulation?
    - codebje 7y ago
      You're probably not going to need a separate function for a binary operator.
    - tathougies 7y ago
      Not really. I may have vector length manipulation and address formatting though. But vector lengths are not integers (or natural for that matter) and an address is certainly not a string. Perhaps you could use these primitives to represent these things but we should not confuse representation with equality.
wellpast 7y ago
> Once you really understand the typesystem, most of the time, types really are the best documentation --- they often tell you exactly what the function does, in a way that English comments never will. Snake Oil. Apply this claim to any set of real world functions, however well designed they are. This is classic Haskellism. Obsessed with the lattice of types in the room. Door closed. Real world outside.
- quickthrower2 7y ago
  Not completely. Types are documentation. When going from JS -> TS you suddenly have the ability to create types that allow you to easily discover what is in an object. You can now confidently say foo.bar.replace(...) and know it'll work at runtime. Otherwise you hope that someone has written in a doc somewhere that bar is a string. And judging by npm docs I've seen - that is very unlikely. So you debug at runtime, head over to the github repo, or do an console.log(typeof(... hmm!
  - wellpast 7y ago
    Types alone are severely insufficient documentation. That’s the refutation of the original poster’s claim.
    - perfmode 7y ago
      What are all of the things this function could possibly do to its arguments? (a -> b -> c) -> b -> a -> c
      - deleted 7y ago
        [deleted]
      - wellpast 7y ago
        Infinite.
        quickthrower2 7y ago
quickthrower2 7y ago
> I don't need to use my brain to do programming ... hoistStateIntoStateT :: Sem (State s ': r) a -> S.StateT s (Sem r) a hoistStateIntoStateT (Sem m) = m $ \u -> case decomp u of Left x -> S.StateT $ \s -> liftSem . fmap swap . weave (s, ()) (\(s', m') -> fmap swap $ S.runStateT m' s') (Just . snd) $ hoist hoistStateIntoStateT x Right (Yo Get z _ y _) -> fmap (y . (<$ z)) $ S.get Right (Yo (Put s) z _ y _) -> fmap (y . (<$ z)) $ S.put s ... I definitely need to use my brain to read that code though.
- munchbunny 7y ago
  I have a similar experience with mathematics. "The differential form expressions for Maxwell's equations are incredibly simple!" Yup, they're simple after you've done all of the work to wrap your mind around differential forms in the first place. I did it at some point. It was rewarding, and it was elegant, and it was even fun, but it was anything but easy on my brain. Haskell feels a lot like that. That code snippet gave me the same feeling of having to climb a conceptual mountain to appreciate the metaphorical view at the top. I have no doubt that there is something beautiful there, but of all of the conceptual, programming related mountains I need to climb, the language abstraction one is pretty low priority, because the language I am using really is not my limiting factor. I appreciate that others who care spend a lot of time thinking about this problem, but Haskell's got a long way to go before I'm convinced that it's worth using in everyday contexts.
  - quickthrower2 7y ago
    Absolutely, and I have put a decent amount of time in to learning Haskell. But I've been imperative programming since 8 yo, and as much as I love Haskell I can't be saved from finding it hard to understand. I also find it unmemorable - I could get my head around that code if I tried but 2 weeks later I will forget. I also find that code quite abstract, it looks to be solving some kind of problem that usually the language designer (if say you are in C#) would be solving. Haskell seems to be something that leaks it's mechanics into your code, where as C# keeps it for the most part nicely separated from your code, albeit with the effect of giving the programmer less power. No typeclasses etc.
noncoml 7y ago
I really wanted to get into the promise-land of Haskell, and tried hard to, but my enthusiasm went south when I found out I can hit bugs with lazy-IO that the compiler wouldn't warn me about.
- jose_zap 7y ago
  Lazy Io was an unfortunate historic accident, one which is preached much against in the Haskell community. Alternative standard libraries abound in the ecosystem that remove this accident.
hardwaresofton 7y ago
This post is not for beginners/non-haskellers, I don't understand why it's being posted here. Is this intentional or are people in the haskell community this tone deaf? It's like we're determined to prevent new people from joining. Dear everyone, code like this is not where Haskell starts to get useful, it's useful much earlier. I won't reproduce it here but I just wrote a post with some practical code (and how haskell helped) taken from a project of mine: https://news.ycombinator.com/item?id=20260095 https://news.ycombinator.com/item?id=20260095. If you are using Coyoneda in your code, please do not use it to extol the virtues of Haskell, except if you're sure your audience is expert haskellers/mathematicians/researchers/others who can actually gain something from the post, or if the writing is so sublime that it has reduced the complexity to near zero. Please OP, you're actively hurting the adoption of Haskell by posting stuff like this in the wrong places/context. The author of the article (Sandy Maguire) created a library called polysemy that improved on the efficiency of using a concept called Free Monads in Haskell -- their main benefit is that they let you write functions that deal only in your business domains. A rough corrolary would be a dependency-injected function that could not do anything outside of what the dependency injected pieces do, but also allows for different dependency implementations to be mocked out entirely within the languag (i.e. without the XML/annotation hell that is Spring DI magic).
- stcredzero 7y ago
  Is this intentional or are people in the haskell community this tone deaf? It's like we're determined to prevent new people from joining. It happens with small "misunderstood" groups. People in such groups start doing things to purposely set themselves apart and distinguish themselves from the outside majority. It seems partly subconscious or instinctual, though it's also expressed as conscious actions and can involve quite a bit of thought and rationalization. In particular, it happens with programming communities.
- danharaj 7y ago
  > This post is not for beginners/non-haskellers, I don't understand why it's being posted here. Is this intentional or are people in the haskell community this tone deaf? It's like we're determined to prevent new people from joining. There are plenty of submissions on HN that are aimed at specialists of a field. They get to the front page because people are curious about specialized fields. So, even though I disagree from the pits of my soul with the content of the submission (as a professional Haskell developer, I should add), I think you're being very unfair to say that stuff like this shouldn't be shared with a broader audience.
jrochkind1 7y ago
Are they suggesting writing code that you can't later understand or debug? Does this actually work out for Haskellers? I mean, I guess I'll believe you if you tell me it does, Haskell is different enough from the kind of programming I do that I don't think I know anything at all about it.
- jeremyjh 7y ago
  Some of the type-machinery code (hint, it has words like "hoist" or "lift" that describe type operations, not data operations) is like that, and its really not a problem because it does the only thing it can do given the types, and the things it does have nothing to do with your business domain or I/O so its never going to change unless a library you are using changes. When that happens its annoying but you just play type tetris again until the red squiggly lines go away and then you are fine for another few years. It isn't something I'd really brag about though as its really hard to explain the benefits of this stuff to non-Haskellers and you can end up wasting infinite amounts of time polishing these abstractions instead of getting work done.
  - jrochkind1 7y ago
    > because it does the only thing it can do given the types Okay, this may be (probably is) a stupid question, because I know no Haskell whatsoever, but... if there's really only one thing it can do given the types, why does the code have to be there at all? Why can't you just write "Do the only thing you can do given these types"? If it's code humans aren't meant to read anyway, and it really is the only thing that could be done... why can't the compiler just do it without you having to put the non-human-intelligible code in your source files?
    - syrak 7y ago
      This is an interesting question. Technically there is more than one possible implementation, but you would also have to go out of your way to get it wrong. Automatically determining what constitutes "going out of your way" so that the code can be generated automatically is an active area of research (program synthesis), but as this post already shows, for "simple" cases, we're getting pretty close. As the post mentions, there are certain dead giveaways of an incorrect implementation, such as unused variables. Conversely one may still have some rough idea of the desired code to guide the implementation. The point is not about entirely removing one's mind from the process, but to allow oneself to only think about the choices that matter, which are few. Alternatively, another way to look at the problem is that these types, while already being quite precise, are still not as precise as they could be, because the type system is not sufficiently expressive. And even with the ability to describe the desired properties to uniquely determine the implementation: - it may not be obvious that the implementation is in fact uniquely determined; - a solution, unique or not, may not be easy to find automatically. Program synthesis is essentially the same problem as proof search (c.f. Curry-Howard correspondence); knowing that there is a proof of Fermat's last theorem is not sufficient to construct an actual proof of it from scratch. For these reasons, it may still be desirable to nail down the implementation explicitly even if it is hard to read. It's also worth considering the fact that polysemy (the package that the controversial snippet at the beginning of the post comes from) is very much an implementation of a state-of-the-art effect system using state-of-the-art features of Haskell's type system, so it can be expected that the abstractions to make this code more digestible (for the right audience) are still missing, because no one has ever thought of how to express them yet.
deleted 7y ago
[deleted]
tempsolution 7y ago
Sorry but this is just crazy. I always wonder if people writing blog posts like that have ever worked in a big company. You need to spend at least 2-3 hours a day doing code reviews and most of the rest you are writing code, which subsequently involves reading the code you wrote yourself and others have written. Now we currently use Java here. I worked with other programming languages in companies too, for instance C and C++ which were a nightmare with no equal. Don't get me wrong, when I was in college I just loved creating crazy shit with template metaprogramming and preprocessor metaprogramming. Once you mature out of it, this is just the most craziest thing you could ever do. The reason is simple. Even plain, stupid Java is already incredibly hard to verify during a CodeReview. Spend 2 hours in a row trying to find problems with other's people well written Java code and your brain feels like it explodes. Now with C++ that same task is almost impossible and will likely require 8 hours of your day for the same code volume. With Haskell I would go out on a limb here and say it would require 24 hours of your daily time to handle the same code volume... Not to mention that most programmers even at Google and Amazon would not even be able to either read or write such code and people like me, who could and did in the past would just shake their heads and move on. Nobody wants to deal with such code outside of university...
- mabbo 7y ago
  > most programmers even at Google and Amazon would not even be able to either read or write such code Hello, I am at Amazon. I spend a decent portion of my time working with an in-house Clojure library (not entirely dissimilar to Haskell) which handles some mission critical business logic my team owns. It terrifies me. I hate it. For every hour I spend working with it, I spend another hour trying to convince everyone we need to rewrite it in Java, immediately, or replace it with a different library. None of us have a clue how it works. We can't debug it. The guy who wrote it quit three years ago. I mean, it works. It works very well. But the day it doesn't work, we're not going to have a clue why that is. And then we're in real trouble.
  - rfrey 7y ago
    You could use those hours currently spent lobbying for a rewrite to, you know, learn clojure.
slifin 7y ago
I've never read a code base where I thought the type system was doing a good job of being a DSL for describing business requirements Types are great imo for checking against primitives because the semantics of int string array etc are strong but most languages are encouraging wrapping up primitives in some user defined wrapper then the semantics of the wrapper are implicit, brittle and known only to the author The semantics of your Bob class is more likely to change as it's used over many different contexts than the int type is, if the int type is being swapped out it's usually because the wrong data is being used, which is what we are using types to protect against, it's not usually because there's a problem with what int is
- syrak 7y ago
  > I've never read a code base where I thought the type system was doing a good job of being a DSL for describing business requirements Would refinement types help in that respect? For example, the F* language. https://www.fstar-lang.org/ https://www.fstar-lang.org/ I don't have any experience with "business" code, but my naive understanding is that application-level code is typically very monomorphic which is exactly where refinement types are useful, whereas the OP leverages polymorphism to a large extent (not necessarily), and that works well for general-purpose libraries which don't and must not care about their users' data.
sfink 7y ago
This reminds me of solving physics problems by getting the units right. Blah blah ...15 meters per second... blah blah ...after 10 minutes... blah blah ...how far... blah blah => aha! I probably want to multiply 15 by (10 × 60).
- tome 7y ago
  Yes, very much the same flavour! In each case although it doesn't guarantee the right answer it gets you closer.
  - dllthomas 7y ago
    Obligatory: https://xkcd.com/687 https://xkcd.com/687

103 points by Tehnix 7y ago

I would really love to see an IDE that auto suggests / autocompletes code based on typed holes like this. Does such a thing exist?

Jtsummers 7y ago
Check out Idris and the book Type Driven Development. It has an emacs mode that does that for you. I’m not sure about other languages. It was a very nice experience though I just went through it for the learning experience and haven’t tried to apply it to any problems since then.
gcommer 7y ago
Holes in Agda are a good bit more powerful than in Haskell, and agda's emacs mode has a bunch of very powerful commands for working with them, eg: listing possible values, automatically filling, splitting them by case, etc. For example, for this post's "jonk" example I just had to copy the type into emacs, reformat it a bit into Agda syntax, then press C-c C-a and it automatically figured out the solution that the author worked through manually: λ z z₁ z₂ → z₁ (λ z₃ → z₂ (z z₃)) See the full list of commands at https://agda.readthedocs.io/en/v2.5.2/tools/emacs-mode.html https://agda.readthedocs.io/en/v2.5.2/tools/emacs-mode.html
derefr 7y ago
Why even have the code? The type is all the compiler needs to spit out a definition. Your source can just be the type.
pirocks 7y ago
Intellij can sorta do this for Java if you fo ctrl+shift+space.
hardwaresofton 7y ago
Idris does this with a REPL-like interface: https://www.youtube.com/watch?v=mOtKD7ml0NU https://www.youtube.com/watch?v=mOtKD7ml0NU

kazinator 7y ago

> Which means you can slowly use type holes to chip away at a difficult implementation, without ever really knowing what you're doing. Yeah, look! I started with a function signature and a little _. Lo and behold, fifty seven holes later, I have a graph-coloring optimal register allocator for MIPS for my compiler back end. Don't ask me how it works, but the type system assures it.

state_less 7y ago
This type system, is it powered by AI?
- mrkeen 7y ago
  There's nothing fuzzy going on. If I said f(x) = 2, you could quickly work backwards from that and state: 2 is an Int. x isn't used so it could be any type, let's say a. That means f has type (a -> Int).
mrkeen 7y ago
This, but unironically.

dan-robertson 7y ago

I read the argument in the article as something like “strong advanced type systems like Haskell’s are good because instead of manually writing hard functions, one can just write the type (ie the meaning of the function) and do a bunch of menial compiler-directed work to build up one’s function in little steps. This is great because one doesn’t need to “actually” write such horrible functions. I find it slightly silly because one still has to read such functions so it is still hard to know that they do the right thing. For example, consider the function in the article which has type: Sem (State s ': r) a -> S.StateT s (Sem r) a It seems pretty obvious what this morally should do. In some cases it is possible for polymorphism to force a value of a certain type to always behave a certain way. E.g. a value of type [a] must be the empty list because that is the only value with that type. On the other hand there are multiple values of type [[a]] (I.e. an empty list or an infinite list of empty lists or anything in between). A more complicated example is that the only thing a function with the signature of compose ((b -> c) -> (a -> b) -> (a -> c)) can do is compose functions whereas a function of type (Int-> Int) -> (Int-> Int) -> (Int -> Int) can do just about anything. Outside of abstract Haskell libraries, code tends to look more like the second case than the first. In this case it is hard to be sure that the function must behave in the correct way because of its type. I think it hinges on whether it is possible for Put to change the type of the state. If it can then types force you to always take the newly put value and return it with Get, otherwise it would be possible for Put to eg only sometimes work. So if one has to check that the code is correct, one must either read very carefully and check the code, or one must very carefully read the type signature and deduce that the code is correct. In the first case the fact that the compiler made the code easy to write doesn’t really help much. Perl5 taught us that just because a program was easy to write it does not mean it will be easy to read/check. In the second case, why do we have a program at all? If there is only one correct program we could have written then it seems to me that the program is in fact the type and the compiler ought to have been more clever and written it itself. (There are of course plenty of issues with that statement). It seems to me that claiming “Haskell is great because it helps automatically write difficult functions which are impossible to check” or “Haskell is great because it makes me do the manual steps in writing a function that can only ever do one thing and mixes that pointless code in with the thing I care about” is a bit silly. This all being said, I do think holes are a useful feature but I don’t think they are useful for entirely writing a function for you. They are particularly useful in proof assistants like Agda where one must manually exhibit a million trivial propositions and holes help fill in all the boring gaps. Agda doesn’t really suffer from the “multiple things a type could mean” issue.

mpweiher 7y ago

This piqued my interest, because that's the same way TDD works for me. And then it starts with "Let's go through an example together. Consider the random type signature that I just made up:" Hmm...I never have a type signature as a starting point, random or not. I have some sort of requirement, some sort of functionality I want out of the code. Soft fuzzy requirements. And the types rarely if ever tell me what the function does. Heck, a function that's int x int -> int could be just about anything. How about string -> int? Does it convert the string to an integer or count the vowels?

golergka 7y ago
> Heck, a function that's int x int -> int could be just about anything. How about string -> int? That's because using types like "int" and "string" is not a real, valid use of a good type system. Instead, you'd typically have a function type of `newton -> sqMeter -> pascal`, or `username -> accessLevel`. All these types would be implemented through basic int and string types, but declaring them explicitly with very limited conversions inbetween would actually use type system to verify correctness of your code.
- mpweiher 7y ago
  So you're going to not have arithmetic or string manipulation?
  - codebje 7y ago
    You're probably not going to need a separate function for a binary operator.
  - tathougies 7y ago
    Not really. I may have vector length manipulation and address formatting though. But vector lengths are not integers (or natural for that matter) and an address is certainly not a string. Perhaps you could use these primitives to represent these things but we should not confuse representation with equality.

wellpast 7y ago

> Once you really understand the typesystem, most of the time, types really are the best documentation --- they often tell you exactly what the function does, in a way that English comments never will. Snake Oil. Apply this claim to any set of real world functions, however well designed they are. This is classic Haskellism. Obsessed with the lattice of types in the room. Door closed. Real world outside.

quickthrower2 7y ago
Not completely. Types are documentation. When going from JS -> TS you suddenly have the ability to create types that allow you to easily discover what is in an object. You can now confidently say foo.bar.replace(...) and know it'll work at runtime. Otherwise you hope that someone has written in a doc somewhere that bar is a string. And judging by npm docs I've seen - that is very unlikely. So you debug at runtime, head over to the github repo, or do an console.log(typeof(... hmm!
- wellpast 7y ago
  Types alone are severely insufficient documentation. That’s the refutation of the original poster’s claim.
  - perfmode 7y ago
    What are all of the things this function could possibly do to its arguments? (a -> b -> c) -> b -> a -> c
    - deleted 7y ago
      [deleted]
    - wellpast 7y ago
      Infinite.
      - quickthrower2 7y ago

quickthrower2 7y ago

> I don't need to use my brain to do programming ... hoistStateIntoStateT :: Sem (State s ': r) a -> S.StateT s (Sem r) a hoistStateIntoStateT (Sem m) = m $ \u -> case decomp u of Left x -> S.StateT $ \s -> liftSem . fmap swap . weave (s, ()) (\(s', m') -> fmap swap $ S.runStateT m' s') (Just . snd) $ hoist hoistStateIntoStateT x Right (Yo Get z _ y _) -> fmap (y . (<$ z)) $ S.get Right (Yo (Put s) z _ y _) -> fmap (y . (<$ z)) $ S.put s ... I definitely need to use my brain to read that code though.

munchbunny 7y ago
I have a similar experience with mathematics. "The differential form expressions for Maxwell's equations are incredibly simple!" Yup, they're simple after you've done all of the work to wrap your mind around differential forms in the first place. I did it at some point. It was rewarding, and it was elegant, and it was even fun, but it was anything but easy on my brain. Haskell feels a lot like that. That code snippet gave me the same feeling of having to climb a conceptual mountain to appreciate the metaphorical view at the top. I have no doubt that there is something beautiful there, but of all of the conceptual, programming related mountains I need to climb, the language abstraction one is pretty low priority, because the language I am using really is not my limiting factor. I appreciate that others who care spend a lot of time thinking about this problem, but Haskell's got a long way to go before I'm convinced that it's worth using in everyday contexts.
- quickthrower2 7y ago
  Absolutely, and I have put a decent amount of time in to learning Haskell. But I've been imperative programming since 8 yo, and as much as I love Haskell I can't be saved from finding it hard to understand. I also find it unmemorable - I could get my head around that code if I tried but 2 weeks later I will forget. I also find that code quite abstract, it looks to be solving some kind of problem that usually the language designer (if say you are in C#) would be solving. Haskell seems to be something that leaks it's mechanics into your code, where as C# keeps it for the most part nicely separated from your code, albeit with the effect of giving the programmer less power. No typeclasses etc.

noncoml 7y ago

I really wanted to get into the promise-land of Haskell, and tried hard to, but my enthusiasm went south when I found out I can hit bugs with lazy-IO that the compiler wouldn't warn me about.

jose_zap 7y ago
Lazy Io was an unfortunate historic accident, one which is preached much against in the Haskell community. Alternative standard libraries abound in the ecosystem that remove this accident.

hardwaresofton 7y ago

This post is not for beginners/non-haskellers, I don't understand why it's being posted here. Is this intentional or are people in the haskell community this tone deaf? It's like we're determined to prevent new people from joining. Dear everyone, code like this is not where Haskell starts to get useful, it's useful much earlier. I won't reproduce it here but I just wrote a post with some practical code (and how haskell helped) taken from a project of mine: https://news.ycombinator.com/item?id=20260095 https://news.ycombinator.com/item?id=20260095. If you are using Coyoneda in your code, please do not use it to extol the virtues of Haskell, except if you're sure your audience is expert haskellers/mathematicians/researchers/others who can actually gain something from the post, or if the writing is so sublime that it has reduced the complexity to near zero. Please OP, you're actively hurting the adoption of Haskell by posting stuff like this in the wrong places/context. The author of the article (Sandy Maguire) created a library called polysemy that improved on the efficiency of using a concept called Free Monads in Haskell -- their main benefit is that they let you write functions that deal only in your business domains. A rough corrolary would be a dependency-injected function that could not do anything outside of what the dependency injected pieces do, but also allows for different dependency implementations to be mocked out entirely within the languag (i.e. without the XML/annotation hell that is Spring DI magic).

stcredzero 7y ago
Is this intentional or are people in the haskell community this tone deaf? It's like we're determined to prevent new people from joining. It happens with small "misunderstood" groups. People in such groups start doing things to purposely set themselves apart and distinguish themselves from the outside majority. It seems partly subconscious or instinctual, though it's also expressed as conscious actions and can involve quite a bit of thought and rationalization. In particular, it happens with programming communities.
danharaj 7y ago
> This post is not for beginners/non-haskellers, I don't understand why it's being posted here. Is this intentional or are people in the haskell community this tone deaf? It's like we're determined to prevent new people from joining. There are plenty of submissions on HN that are aimed at specialists of a field. They get to the front page because people are curious about specialized fields. So, even though I disagree from the pits of my soul with the content of the submission (as a professional Haskell developer, I should add), I think you're being very unfair to say that stuff like this shouldn't be shared with a broader audience.

jrochkind1 7y ago

Are they suggesting writing code that you can't later understand or debug? Does this actually work out for Haskellers? I mean, I guess I'll believe you if you tell me it does, Haskell is different enough from the kind of programming I do that I don't think I know anything at all about it.

jeremyjh 7y ago
Some of the type-machinery code (hint, it has words like "hoist" or "lift" that describe type operations, not data operations) is like that, and its really not a problem because it does the only thing it can do given the types, and the things it does have nothing to do with your business domain or I/O so its never going to change unless a library you are using changes. When that happens its annoying but you just play type tetris again until the red squiggly lines go away and then you are fine for another few years. It isn't something I'd really brag about though as its really hard to explain the benefits of this stuff to non-Haskellers and you can end up wasting infinite amounts of time polishing these abstractions instead of getting work done.
- jrochkind1 7y ago
  > because it does the only thing it can do given the types Okay, this may be (probably is) a stupid question, because I know no Haskell whatsoever, but... if there's really only one thing it can do given the types, why does the code have to be there at all? Why can't you just write "Do the only thing you can do given these types"? If it's code humans aren't meant to read anyway, and it really is the only thing that could be done... why can't the compiler just do it without you having to put the non-human-intelligible code in your source files?
  - syrak 7y ago
    This is an interesting question. Technically there is more than one possible implementation, but you would also have to go out of your way to get it wrong. Automatically determining what constitutes "going out of your way" so that the code can be generated automatically is an active area of research (program synthesis), but as this post already shows, for "simple" cases, we're getting pretty close. As the post mentions, there are certain dead giveaways of an incorrect implementation, such as unused variables. Conversely one may still have some rough idea of the desired code to guide the implementation. The point is not about entirely removing one's mind from the process, but to allow oneself to only think about the choices that matter, which are few. Alternatively, another way to look at the problem is that these types, while already being quite precise, are still not as precise as they could be, because the type system is not sufficiently expressive. And even with the ability to describe the desired properties to uniquely determine the implementation: - it may not be obvious that the implementation is in fact uniquely determined; - a solution, unique or not, may not be easy to find automatically. Program synthesis is essentially the same problem as proof search (c.f. Curry-Howard correspondence); knowing that there is a proof of Fermat's last theorem is not sufficient to construct an actual proof of it from scratch. For these reasons, it may still be desirable to nail down the implementation explicitly even if it is hard to read. It's also worth considering the fact that polysemy (the package that the controversial snippet at the beginning of the post comes from) is very much an implementation of a state-of-the-art effect system using state-of-the-art features of Haskell's type system, so it can be expected that the abstractions to make this code more digestible (for the right audience) are still missing, because no one has ever thought of how to express them yet.

deleted 7y ago

[deleted]

tempsolution 7y ago

Sorry but this is just crazy. I always wonder if people writing blog posts like that have ever worked in a big company. You need to spend at least 2-3 hours a day doing code reviews and most of the rest you are writing code, which subsequently involves reading the code you wrote yourself and others have written. Now we currently use Java here. I worked with other programming languages in companies too, for instance C and C++ which were a nightmare with no equal. Don't get me wrong, when I was in college I just loved creating crazy shit with template metaprogramming and preprocessor metaprogramming. Once you mature out of it, this is just the most craziest thing you could ever do. The reason is simple. Even plain, stupid Java is already incredibly hard to verify during a CodeReview. Spend 2 hours in a row trying to find problems with other's people well written Java code and your brain feels like it explodes. Now with C++ that same task is almost impossible and will likely require 8 hours of your day for the same code volume. With Haskell I would go out on a limb here and say it would require 24 hours of your daily time to handle the same code volume... Not to mention that most programmers even at Google and Amazon would not even be able to either read or write such code and people like me, who could and did in the past would just shake their heads and move on. Nobody wants to deal with such code outside of university...

mabbo 7y ago
> most programmers even at Google and Amazon would not even be able to either read or write such code Hello, I am at Amazon. I spend a decent portion of my time working with an in-house Clojure library (not entirely dissimilar to Haskell) which handles some mission critical business logic my team owns. It terrifies me. I hate it. For every hour I spend working with it, I spend another hour trying to convince everyone we need to rewrite it in Java, immediately, or replace it with a different library. None of us have a clue how it works. We can't debug it. The guy who wrote it quit three years ago. I mean, it works. It works very well. But the day it doesn't work, we're not going to have a clue why that is. And then we're in real trouble.
- rfrey 7y ago
  You could use those hours currently spent lobbying for a rewrite to, you know, learn clojure.

slifin 7y ago

I've never read a code base where I thought the type system was doing a good job of being a DSL for describing business requirements Types are great imo for checking against primitives because the semantics of int string array etc are strong but most languages are encouraging wrapping up primitives in some user defined wrapper then the semantics of the wrapper are implicit, brittle and known only to the author The semantics of your Bob class is more likely to change as it's used over many different contexts than the int type is, if the int type is being swapped out it's usually because the wrong data is being used, which is what we are using types to protect against, it's not usually because there's a problem with what int is

syrak 7y ago
> I've never read a code base where I thought the type system was doing a good job of being a DSL for describing business requirements Would refinement types help in that respect? For example, the F* language. https://www.fstar-lang.org/ https://www.fstar-lang.org/ I don't have any experience with "business" code, but my naive understanding is that application-level code is typically very monomorphic which is exactly where refinement types are useful, whereas the OP leverages polymorphism to a large extent (not necessarily), and that works well for general-purpose libraries which don't and must not care about their users' data.

sfink 7y ago

This reminds me of solving physics problems by getting the units right. Blah blah ...15 meters per second... blah blah ...after 10 minutes... blah blah ...how far... blah blah => aha! I probably want to multiply 15 by (10 × 60).

tome 7y ago
Yes, very much the same flavour! In each case although it doesn't guarantee the right answer it gets you closer.
- dllthomas 7y ago
  Obligatory: https://xkcd.com/687 https://xkcd.com/687