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

61–70 of 92 posts

Re: Dependent Haskell

#61

Post by anon_d »

tomkludy wrote: post #58

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

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

It's basically the opposite of this.

If a language has dependent types, you can continue to use it in the same way as a language with does not have dependent types.

BUT, there's a lot of programming patterns that previously couldn't be implemented in a type-safe way, that now can be. This also gives a ton of opportunities for libraries to implement abstractions that weren't expressible before.

Dependent types are not that complicated, actually, and they don't add any burden to programs that don't use them.

Re: Dependent Haskell

#62

Post by lmm »

tomkludy wrote: post #58

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

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

I'd say that's backwards: rather a dependently typed language relaxes a huge restriction that most programming languages have, that only certain things can be used as types. Any program that's valid in language X is also valid in a dependently typed version of language X (e.g. most Haskell functions translate directly into Idris as long as they don't rely on laziness).

Dependent types make it easier to encode properties that you care about into the type system, i.e. rather than the programmer having to get them right, the compiler can check them for you. Far from burdening the programmer, it lightens your mental load.

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

Most code is in terms of domain-specific things, and so the types you use are also domain-specific. In my experience every code bug (as distinct from "behaving as specified but not as intended" bugs) boils down to "we thought x, but actually y" and can be avoided by making more precise use of a type system. If you have bugs that hit production, you can probably avoid them with better types. If you avoid production bugs by using tests, you can probably replace most of those tests with types and they'll become more concise and easier to maintain. But of course the specifics of what types to use will be specific to your domain; examples like list indices are common because they're one of those rare types that virtually everyone uses.

Re: Dependent Haskell

#63

Post by ncmncm »

hinata wrote: post #22
chc4 wrote: post #19

Earlier quoted context omitted.

It does reference counting, but it's not mark-and-sweep stop the world reference counting. It's as garbage collected as shared_ptr and doesn't try to collect cycles. Feels a bit weird to put that under the same bucket as Java.

Academically, both reference counting (C++, Swift, some patterns in Rust) and tracing garbage collection (Java, C#) fall under the umbrella of garbage collection.

The important distinction, then, is obligate garbage collection. Can I write a substantial program that does, and needs, no garbage collection of any kind? In C++ and Rust, yes, trivially, every day.

The distinction matters because without obligate GC, you get the benefit of destructors (or in Rust, the Drop trait), and have the tool for resource management of every kind, usually written "}". Reference counting GC is rarely used in well-designed C++ and Rust programs, simply because there is rarely any need for it. Reliance on shared_ptr or ARC is recognized as a disease of forced Java converts.

Re: Dependent Haskell

#64

Post by lmm »

tomp wrote: post #60
lmm wrote: post #57

Earlier quoted context omitted.

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

> All practical languages (even Rust and Haskell) fail for "division by zero"

Well, they don't have dependent types. In something like Idris you can do safe natural division.

> most (all?) (again even Rust and Haskell) offer escape hatches for their otherwise rather strong static checks.

The difference is that those escape hatches are explicit, and used rarely enough that you can give them special attention in testing/code review - in those languages it's not 95% typechecked but more like 99.9%. (Indeed in Haskell you can use a flag to disallow bypassing the typesystem entirely, and people do).

Re: Dependent Haskell

#65

Post by wtetzner »

peteretep wrote: post #38
pzone wrote: post #20

Earlier quoted context omitted.

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

At first I thought it was a joke along the lines of "A monad is just a monoid in the category of endofunctors, what's the problem?", but no, it seems to be being said non-ironically.

How is this the same thing?

- polymorphic lambda calculus: Lambda calculus with generics

- lazy evaluation: Well, lazy evaluation. Not sure how else to describe this

- algebraic data types: Again, how else to describe this? Put in a full description of what algebraic data types are?

- type classes: Haskell has type classes.

I really don't see what the problem is. If you're coming in to an article about dependent types, and you don't know what these things are, I think don't think the reasonable response is for the author to explain all of it to the reader. This isn't a beginner's introduction to Haskell.

Re: Dependent Haskell

#66

Post by ncmncm »

zozbot123 wrote: post #52
int_index wrote: post #26

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…

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

The term for languages like Swift, Java, and Haskell is "obligate GC". The cost of obligate GC is only superficially just the poor memory locality, interruptions, and bad citizenship -- worse is that the power of destructors is denied you, and with it the power to automate managing every other kind of resource.

Re: Dependent Haskell

#67

Post by [deleted] »

joe_the_user wrote: post #16
huntie wrote: post #7

Earlier quoted context omitted.

Dependent types are types which depend on values. As an example, think of the cons procedure: (List A, A) -> List A. It takes a List of A's and an A and returns a List of A's. With dependent types you can write this as (List n A, A) -> List n+1 A. This tells us that cons takes a List of A's with length n and an A returns a List of A's with length n+1. Edwin Brady shows off some examples in Idris here[1]. I thought th…

When I see this definition, I scratch my head and wonder why this isn't a different way to introduce object orientation, generics, c++ parameterized templates and such.

[deleted]

Re: Dependent Haskell

#68

Post by chrisdone »

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

Adding examples, with dependent types we can write the type-safe printf in Idris:

https://github.com/chrisdone/sandbox/blob/master/dependently...

Meanwhile with Liquid Haskell (refinement types), it was really easy for me to define a date data type that can only construct valid year-month-day combinations:

https://github.com/chrisdone/sandbox/blob/master/liquid-hask...

The `if ..` tests are all required, otherwise Liquid Haskell rejects the program.

So I see value in both directions, if you extrapolate from these examples to harder problems.

Re: Dependent Haskell

#69

Post by xelxebar »

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.

I dunno. It can just be that the intended audience is expected to know these terms already. It'd be weird to call any Nature paper an explainbrag simply because it uses field-specific terminology.

Personally, when little things like that piss me off, I find it more helpful to introspect "why do I have such a strong emational reaction to this little thing?" than to go about laying moral judgement. I find this approach is especially good at promoting effective communication in places where it's easy to misinterpret intenions, like text.

Re: Dependent Haskell

#70

Post by lmm »

ncmncm wrote: post #66
zozbot123 wrote: post #52

Earlier quoted context omitted.

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

The term for languages like Swift, Java, and Haskell is "obligate GC". The cost of obligate GC is only superficially just the poor memory locality, interruptions, and bad citizenship -- worse is that the power of destructors is denied you, and with it the power to automate managing every other kind of resource.

> worse is that the power of destructors is denied you, and with it the power to automate managing every other kind of resource.

These are orthogonal concerns. Plenty of languages without GC do not have good support for ARM (e.g. C), and a GCed language can still have good support for ARM (e.g. monadic regions in Haskell). C++ is really the only language that conflates the two, and IME its RAII style is overrated in practice (there are a lot of rules you have to follow to avoid leaking, and for many of them you get very little warning if you break it).

Post reply on HN