Live data from Hacker News

Dependent Haskell

serokell.io

41–50 of 92 posts

Re: Dependent Haskell

#41

Earlier quoted context omitted.

> This is an explainabrag My goal here was to show that standard Haskell boils down to a small set of features, therefore it's a simple language. Surely, "simple" does not imply "good" (Brainfuck is also simple), so I then assert that the combination of features that Haskell consists is fertile soil for writing maintainable and performant code. > languages without these features can also have "clean, maintainable cod…

> I have a hard time imagining a clean codebase in a language without some form of polymorphism, first class functions, and algebraic data types You don't have any definition of 'clean', so maybe you mean something precise or maybe you don't, but I have seen clean codebases in all kinds of languages - C, C++, Go, Java. The language doesn't dictate whether your code is clean or not, the programmer does.

Bad programmers will write bad code in any language, but in some languages even the best programmers will struggle to write good code. E.g. I've found even the best C tends to look quite cluttered, because the lack of first-class functions forces the programmer to thread state through "by hand", and the lack of polymorphism means the programmer can't clearly separate the what from the how but has to interleave the two. (Indeed I would say bad C can sometimes look superficially cleaner: things like using global variables for state remove some of the clutter, but ultimately the cure is worse than the disease)

Re: Dependent Haskell

#42

This read like a troll piece. Every line rubbed me in some wrong way until I couldn't take it any more. > Haskell, at its core, is simple: it is just a polymorphic lambda calculus with lazy evaluation plus algebraic data types and type classes. This happens to be just the right combination of features to allow us to write clean, maintainable code that also runs fast. This is an explainabrag which is also wrong: langu…

> This is an explainabrag It's not. Maybe it seems that way because you're not familiar with the terms, so it seems like someone trying to name drop all the stuff they know? But if you are familiar with the terms, it's just informative, and serves to situate you in the space of possible language designs. It's a lambda calculus as opposed to a process calculus, polymorphic as opposed to simply typed, lazy as opposed t…

I'd argue that the informative value is pretty much zero: If a programmer is familiar with lambda calculus, lazy languages, and algebraic types, then there's just no way that person isn't also somewhat familiar with haskell. The explanation is gibberish for those who need it, so its only use is to be self congratulatory for those who don't.

Re: Dependent Haskell

#43

This read like a troll piece. Every line rubbed me in some wrong way until I couldn't take it any more. > Haskell, at its core, is simple: it is just a polymorphic lambda calculus with lazy evaluation plus algebraic data types and type classes. This happens to be just the right combination of features to allow us to write clean, maintainable code that also runs fast. This is an explainabrag which is also wrong: langu…

>This is an explainabrag which is also wrong

It only feels like "explainabrag"ing to some, I would imagine. The terms are all really standard, and listing out features by their names hardly feels braggy. It's a clear, concise way of stating features of a language. Coming from other languages with those features I think the information was conveyed well - but for others it would just look like jargon.

To me, the author was setting up the post - framing the conversation by explaining their view of Haskell as a set of core features. Then they moved on to discuss another feature - dependent types. This makes a lot of sense in the context of dependent types - I think this HN post really nicely conveys why:

https://news.ycombinator.com/item?id=18705128

> What a profoundly dismissive attitude. Why bring up Cyclone and not, say, Swift? Or is Swift meant to be included in "garbage collected languages?"

It's like, pretty mostly true. There are other languages that are memory safe without GC but I don't know of any that are mainstream/ even in use, or that allow free'ing of memory.

Yes Swift is GC'd, just not tracing GC'd.

https://en.wikipedia.org/wiki/Garbage_collection_(computer_s...

> No these are not the same and this is an absurdly wrong conflation. Dart, Objective-C, TypeScript, and others are dynamically typed languages with static type checking. You can't "or rather" this distinction away.

I don't think so.

"Dynamically typed with static type checking" makes no sense. The languages listed are statically typed. They may coincidentally compile to code that checks the type at runtime as well, or code that has or lacks implicit casts, or otherwise carries type information around with the data, or whatever, but the types are statically defined.

Also, dynamic types are often considered to be unityped - every value inhabits one giant union of all possible types.

https://existentialtype.wordpress.com/2011/03/19/dynamic-lan...

Here is a source demonstrating that this view is not unique. You are free to disagree (some do), but it's hardly an "absurdly wrong conflation".

I think your post was pretty unnecessarily critical. You didn't like the post, ok. But maybe you should have challenged that gut reaction - that "rubbed me the wrong way" feeling, because I think your post has considerably more inaccuracies than the article and is unequivocally more hostile. If you'd challenged that feeling maybe you would have learned something?

Re: Dependent Haskell

#44
I fundamentally disagree with the author's thesis. I don't think dependent types are the future of development, but instead I'd bet on refined types (or contracts - see my experiment [0], Liquid Haskell [1] by Ranjit Jhala, and languages Dafny [2] and F* [3] developed by Microsoft on top of Z3 SMT theorem prover [4]), where constraints are explicit yet simple, and proven automatically by an automated theorem prover.

  lookup : (a : array) -> (n : int if 0  whatever
[0] https://github.com/tomprimozic/type-systems/tree/master/refi...

[1] https://ucsd-progsys.github.io/liquidhaskell-blog/

[2] https://rise4fun.com/Dafny/tutorial/guide

[3] https://fstar-lang.org/tutorial - see e.g. section 3 "First proofs about functions on integers"

[4] https://github.com/Z3Prover/z3

Re: Dependent Haskell

#45

Earlier quoted context omitted.

> This is an explainabrag It's not. Maybe it seems that way because you're not familiar with the terms, so it seems like someone trying to name drop all the stuff they know? But if you are familiar with the terms, it's just informative, and serves to situate you in the space of possible language designs. It's a lambda calculus as opposed to a process calculus, polymorphic as opposed to simply typed, lazy as opposed t…

I'd argue that the informative value is pretty much zero: If a programmer is familiar with lambda calculus, lazy languages, and algebraic types, then there's just no way that person isn't also somewhat familiar with haskell. The explanation is gibberish for those who need it, so its only use is to be self congratulatory for those who don't.

Why do you say "self congratulatory" and not "communicative"? You are assuming your conclusion: that it was snobby. But it wasn't. It was just informative, provided, yes, you knew what the words meant.

The author is communicating with other people who know about the space of programming languages, and describing Haskell in a particular way to show its surface area.

Re: Dependent Haskell

#46
post #44

I fundamentally disagree with the author's thesis. I don't think dependent types are the future of development, but instead I'd bet on refined types (or contracts - see my experiment [0], Liquid Haskell [1] by Ranjit Jhala, and languages Dafny [2] and F* [3] developed by Microsoft on top of Z3 SMT theorem prover [4]), where constraints are explicit yet simple, and proven automatically by an automated theorem prover.…

The problem I have is that it's not so obvious to the human reader which things are automatically provable. Constraint solvers are often surprisingly good, and occasionally surprisingly bad, so I'm constantly scared of getting into a "it's working, don't touch it" situation where seemingly simple changes make code stop working.

We're constantly told that traditional typechecking is very limited compared to other forms of formal analysis. But I've always found dependent type systems are enough to express the relevant business constraints, and making the actual typechecking stage trivial seems very worthwhile.

Re: Dependent Haskell

#47

Earlier quoted context omitted.

> This is an explainabrag It's not. Maybe it seems that way because you're not familiar with the terms, so it seems like someone trying to name drop all the stuff they know? But if you are familiar with the terms, it's just informative, and serves to situate you in the space of possible language designs. It's a lambda calculus as opposed to a process calculus, polymorphic as opposed to simply typed, lazy as opposed t…

I'd argue that the informative value is pretty much zero: If a programmer is familiar with lambda calculus, lazy languages, and algebraic types, then there's just no way that person isn't also somewhat familiar with haskell. The explanation is gibberish for those who need it, so its only use is to be self congratulatory for those who don't.

I would assume that some haskell knowledge is assumed, and the author is simply framing the conversation by stating their view of haskell as a set of core features, which they named.

Re: Dependent Haskell

#48

Earlier quoted context omitted.

I was almost 100% certain it was a joke until I read the paragraph that quote is from. I want to reassure you that most Haskell evangelists (myself included) that say stuff like that usually mean it as a joke. Most people who seek to evangelize haskell do not lose sight of the fact that it's pretty daunting at first and has a relatively steep learning curve. That said, Haskell is simple, but it's simple in an unintui…

> Haskell is simple That it might be, but it sure as hell isn't easy. Brainfuck is simple, but nobody would choose to write a real project in it. Most programmers struggle trying to understand what a monad is. That's not easy. The free monad is not easy. Monad transformers are not easy. Understanding foldable/traversable/arrows/applicate is not east. Lens is/are not easy. I have personally worked with dozens of progr…

Comparing Haskell to brainfuck is a little hyperbolic -- you do not have fully understand Monads and their underpinnings to be productive in Haskell. Just like when new programmers write "public static void main" and have no idea what it does, or how JAR files work, or how cout works, newbies can type `do` and get off and running. In Haskell most of your time is spent writing non-monadic code -- writing pure functions that don't care about the outside world.

Another important distinction I want to draw is that while you're that Haskell isn't easy, the difficulty contained within is fundamental to computation itself.

Haskell uses it's type system to buddy-up with category theory which is considered a dual to typed lambda calculus[0]. There are spooky (to me at least, less so to actual mathematicians) natural equivalencies here in that there are certain things you can talk about at the level of Haskell types (category theory) that are universal, and since we're talking about computation, they start becoming universal truths about computations. This is a powerful concept because it changes the way you think about problems. Regardless of whether it's useful in your day job (which might be plumbing two RESTful APIs together) -- I'm not trying to convince anyone to use haskell for everything (you should use the right tool for the job given the constraints), I'm trying to encourage people to try it at least once to see the difference.

Haskell in my mind offers a step stool to understand the deeper theory/mathematics underpinning of computation as a whole, by providing a language that can essentially do both -- express complex concepts and actually do useful things -- it's somewhere on the opposite end of the spectrum from assembly, but not as far as a pen and paper/chalkboard/your mind.

To follow on the point above, all the concepts you're discussing as hard are what we're building in other languages -- the other languages are just giving us versions of the power/expressiveness with corners cut for ergonomics sake, or in the worst cases, drastically reduced power. There is a tradeoff, and it obviously does not always make sense to use Haskell's version of some abstraction, if you do not understand it or it takes you 5x as long to code up. That said, knowing the underlying concepts that underpin these things is the kind of knowledge you can take from project to project -- concepts like traversable show up in file/folder walking, graph traversal, all these problems that you might think were not generically solvable if you only ever dealt with libraries that worked at the lower level (as in one library for walking graphs and the other for walking the filesystem).

You're right that understanding the concepts isn't easy, but this is the best kind of understanding to struggle and overcome -- it's fundamental to the field itself. No one is going to come up with a new Monad/Foldable/Traversable tomorrow, they can generally at best discover new concepts.

> I have personally worked with dozens of programmers that would never be able to write "proper" Haskell.

As long as these programmers learn the paradigms I don't care, use another language that's easier to write. The problem is that you can happily write language x for years and never scratch the surface of these deeper truths/paradigms/approaches, but that doesn't mean it's a good idea for your own personal development as a developer/computer scientist/whatever else. If you don't see value in exploring different, likely fundamental ways of thinking about computing then you do you.

Maybe it's just me, but I see value in languages that expand the way I think -- just like that aha moment when I figured out how to use map/filter/reduce instead of writing for loops. I learned to think in transformations, one step abstracted from the imperative reality.

Haskell may not be for everyone, but the paradigms it exposes are for all computer scientists (as far as I can tell anyway), and thus software developers/engineers who want to work smarter and not harder.

[0]: https://math.stackexchange.com/questions/589311/lambda-calcu...

Re: Dependent Haskell

#49

Earlier quoted context omitted.

I was almost 100% certain it was a joke until I read the paragraph that quote is from. I want to reassure you that most Haskell evangelists (myself included) that say stuff like that usually mean it as a joke. Most people who seek to evangelize haskell do not lose sight of the fact that it's pretty daunting at first and has a relatively steep learning curve. That said, Haskell is simple, but it's simple in an unintui…

> Haskell is simple That it might be, but it sure as hell isn't easy. Brainfuck is simple, but nobody would choose to write a real project in it. Most programmers struggle trying to understand what a monad is. That's not easy. The free monad is not easy. Monad transformers are not easy. Understanding foldable/traversable/arrows/applicate is not east. Lens is/are not easy. I have personally worked with dozens of progr…

> Brainfuck is simple, but nobody would choose to write a real project in it.

Sure. But it's worth knowing whether a language is simple or not (and what tradeoffs have been made to get there).

> Most programmers struggle trying to understand what a monad is. That's not easy.

It's easier than achieving Haskell-like defect rates in languages that have ad-hoc built in solutions to the same problems, IME.

> The free monad is not easy.

Disagree. Certainly it's a lot easier than solving the same problem by hand.

> Monad transformers are not easy.

Agreed, but again, easier than achieving the same defect rates without them.

> Understanding foldable/traversable/arrows/applicate is not east.

Easier than understanding dozens of ad-hoc informally specified implementations of half of them, which is what working in an ecosystem without them boils down to.

> Lens is/are not easy.

Perhaps not, but easier than achieving the same defect rate without them.

Re: Dependent Haskell

#50
post #3

I really do think Haskell is a wonderful tool, but: "Haskell, at its core, is simple: it is just a polymorphic lambda calculus with lazy evaluation plus algebraic data types and type classes." In a different context, I would have interpreted that as a sarcastic parody of Haskell evangelists. Really, I feel like everyone who is going to read that article will either already know that, or will have no idea what that se…

I was almost 100% certain it was a joke until I read the paragraph that quote is from. I want to reassure you that most Haskell evangelists (myself included) that say stuff like that usually mean it as a joke. Most people who seek to evangelize haskell do not lose sight of the fact that it's pretty daunting at first and has a relatively steep learning curve. That said, Haskell is simple, but it's simple in an unintui…

Just realized the list is messed up...

- non-nullable + option types

- function composition (a bunch of languages get stuck in the filter/map phase but never get to the)

- typeclasses + data types over classes + interfaces/abstract classes

- pattern matching

- Monads

- The Free(R) Monad and attempts to make programs more like state machines and encode it at the type level

Post reply on HN