Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Dependent Haskell

serokell.io

Post reply on HN
Print view View original

51–60 of 92 posts

Re: Dependent Haskell

#51

Post by jlokier »

lmm wrote: post #39
millstone wrote: post #9

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…

If you want to engage productively, remember that people tend to say things they think are true, so look for a way to read it that makes sense rather than going out of your way to find a way to read it that makes it false. (I guess nitpicking the phrasing for a "middlebrow dismissal" is the best way to get upvotes here nowadays). > nothing about this list implies "runs fast." It doesn't imply it, but it enables it; r…

> > The implication is that memory-safe languages do not have memory leaks, which is completely false.

> There's no such implication, only that memory-unsafety leads to memory leaks, which is true.

If we're going to read in the spirit of "looking for a way to read things that make sense rather than going out of your way to find a way to read it that makes it false"...

Then it depends which sort of implication.

https://en.wikipedia.org/wiki/Implicature

Re: Dependent Haskell

#52

Post by zozbot123 »

int_index wrote: post #26
millstone wrote: post #9

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 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…

> the cost of decrementing/incrementing these counters is very real

Only true if you use pervasive reference counting, with atomic updates. Swift essentially does this, but other languages don't.

One of the reasons why it makes sense to single out tracing GC (as opposed to RC) is that it's essentially a package deal; your whole program needs to be structured to use memory as essentially an in-RAM database, where every single object or reference can be traced after the fact at some arbitrary time in the future. (There are reasons to do this in some cases, even in 'low-level' languages which are not ordinarily garbage collected - see e.g. the use of "entity component systems" in such languages - but it's obviously not a generally-appropriate solution in any real sense!). RC is self-contained, and it need not even be locally inefficient.

> You're talking about gradually typed languages.

Interestingly, gradual typing does seem to end up with a "worst of both worlds"-type situation - the dynamic tag checks and conversions that have to be inserted at every boundary between statically- and dynamically-typed parts of the program introduce pervasive inefficiency, which is only resolved when static typing is used essentially throughout.

Re: Dependent Haskell

#53

Post by empath75 »

pzone wrote: post #20
millstone wrote: post #9

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…

That "explainabrag" pissed me off too. I feel like that kind of thing is super typical among Haskell bloggers.

You’re not the intended audience for this. For people with an academic cs background, it’s perfectly readable.

Re: Dependent Haskell

#54

Post by tomp »

lmm wrote: post #46
tomp wrote: 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 form…

Maybe, but I think that's mostly an implementation issue... Not only will automated theorem provers get better, but the point is, they don't even need to prove anything! A program would be just as valid if you inserted runtime checks for all contracts, or just the ones you can't prove or disprove. Compare that to type systems, different languages have different ways of dealing with issues (e.g. you can disable type errors in Haskell, Python doesn't care either way, Java is unsound, Scala supports the `any` type, TypeScript defaults to `any`, etc). So we can start by putting contracts from if statements directly into types (that still compile to equivalent code with runtime checks), we immediately gain readability, then slowly but surely we'll be able to prove more and more...

Re: Dependent Haskell

#55

Post by empath75 »

torben-friis wrote: post #42
tree_of_item wrote: post #32

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.

This point of view is alien to me. Why, when you see words you don’t understand, don’t you make an effort to learn what they mean? How on earth did you ever become a coder with this kind of attitude?

Re: Dependent Haskell

#56

Post by agentultra »

atilaneves wrote: post #40
hardwaresofton wrote: post #4

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…

Easy for whom?

Finding Haskell difficult is nothing to be ashamed of. However it's going to appear more difficult than it ought to be if you're approaching it as an experienced programmer with strong opinions. It can be humbling to realize that there's a whole branch of programming you're completely new to and know little about. It's going to be difficult to climb that mountain and you will feel like a beginner again and that's okay.

It's worth the effort!

Re: Dependent Haskell

#57

Post by lmm »

tomp wrote: post #54
lmm wrote: post #46

Earlier quoted context omitted.

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 form…

Maybe, but I think that's mostly an implementation issue... Not only will automated theorem provers get better, but the point is, they don't even need to prove anything! A program would be just as valid if you inserted runtime checks for all contracts, or just the ones you can't prove or disprove. Compare that to type systems, different languages have different ways of dealing with issues (e.g. you can disable type e…

> the point is, they don't even need to prove anything! A program would be just as valid if you inserted runtime checks for all contracts, or just the ones you can't prove or disprove.

"Valid" in what sense? I want my code to refuse to compile when it's broken, not compile and then fail at runtime. I certainly don't want similar-looking checks to be usually compile time but occasionally runtime when things get complicated - that way madness lies.

> Compare that to type systems, different languages have different ways of dealing with issues (e.g. you can disable type errors in Haskell, Python doesn't care either way, Java is unsound, Scala supports the `any` type, TypeScript defaults to `any`, etc).

You're talking about minor differences in edge cases/escape hatches. There's much more variation between different contract systems.

> So we can start by putting contracts from if statements directly into types (that still compile to equivalent code with runtime checks), we immediately gain readability, then slowly but surely we'll be able to prove more and more...

Sounds like gradual typing, which I've found a nightmare to work with in practice - all the pain but very little of the gain. Being 95% typechecked (or 95% statically checked) turns out to be a lot like being 0% typechecked.

Re: Dependent Haskell

#58

Post by tomkludy »

Every discussion or article I have read on dependent types assumes that the reader is a mathematician. I usually make it only a few paragraphs in before I am completely lost.

Right now the only thing that seems clear is that dependent typing adds significant mental burden on the programmer to more thoroughly specify types, and to do so absolutely correctly. In exchange for that burden, there must be practical (not theoretical) benefits but they do not come through clearly. All of the examples I've seen are about "index of a list is guaranteed in bounds". That is such a minor and infrequent bug in practice that it does not justify the additional complexity. There must be more, that I'm just not seeing.

Is there a "Dependent types for non-mathematicians" article out there somewhere, where I can learn about patterns and practical applications?

Re: Dependent Haskell

#59

Post by mbrock »

atilaneves wrote: post #40
hardwaresofton wrote: post #4

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…

Wanna name a supposedly easy language and let’s see if we can come up with a list of things about it that are kinda difficult?

Re: Dependent Haskell

#60

Post by tomp »

lmm wrote: post #57
tomp wrote: post #54

Earlier quoted context omitted.

Maybe, but I think that's mostly an implementation issue... Not only will automated theorem provers get better, but the point is, they don't even need to prove anything! A program would be just as valid if you inserted runtime checks for all contracts, or just the ones you can't prove or disprove. Compare that to type systems, different languages have different ways of dealing with issues (e.g. you can disable type e…

> the point is, they don't even need to prove anything! A program would be just as valid if you inserted runtime checks for all contracts, or just the ones you can't prove or disprove. "Valid" in what sense? I want my code to refuse to compile when it's broken, not compile and then fail at runtime. I certainly don't want similar-looking checks to be usually compile time but occasionally runtime when things get compli…

> Being 95% typechecked (or 95% statically checked) turns out to be a lot like being 0% typechecked.

That's just not realistic. All practical languages (even Rust and Haskell) fail for "division by zero", and most (all?) (again even Rust and Haskell) offer escape hatches for their otherwise rather strong static checks. Still (some) people see a lot of value in _more_ static (type/contract) checking.

Post reply on HN