Hacker News Reader

Comment by kreyenborgi | Hacker News Reader

twelve years have passed - is DT less painful today?

David Christiansen did a more recent experience report from 2019 about using Dependently Typed Haskell at Galois.

https://davidchristiansen.dk/pubs/dependent-haskell-experien...

The video is on YouTube somewhere. Having used Haskell and some dependently typed Haskell around the same time, I thought it was a fair assessment of state of play.

I am not sure, but as a Typescripter, I think I'd find refinement types easier - https://github.com/ucsd-progsys/liquidhaskell

I am not sure if they serve the same purpose or how the venn diagrams overlap on this, but in 2000 I loved the idea of the assersion in Ada, and I love even more the idea the type system can prove your number is between 1 and 10 (etc.).

I reckon it occasionally will catch a bug, but more than that is perfect documentation. I don't want delay to be an int, I want it to be a RateLimitBackoffDelaySeconds which is between >0 and <60, for example.

As I understand the nomenclature liquid types are refinement types and they are dependent types, but typically when people say "dependent types" without qualification they mean the much more powerful (and difficult) "full" dependent types where you can do stuff like returning an int or a string depending on some runtime value.

https://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/li...

Yes.

It could be much better but Dependent Haskell has been stymied by pearl clutching in the community about “pragmatism,” and “scaring away new users.” And a few technical hurdles.

I want Dependent Haskell to happen. I think that when you need it, you need it. And when you only have partial support for it you end up with a very confusing set of libraries and conventions to encode dependent types in Haskell that is probably more off-putting than proper language support (singletons, GADTs, type classes and associated type families and.. and.. and..).

That being said, Haskell isn’t exactly funded by a company like Microsoft. It’s a small community and the teams driving these projects are small and staffed with keen volunteers for the most part.

I don’t think DH will happen but I hope it will get through.

Isn't Idris basically Haskell with DT?

At the language level...sort of?

Idris is strict, unlike Haskell. As of Idris 2, it also has a substructural type system which tracks how often terms are used, which is kind of Rust-y and can allow for better runtime performance by ensuring that proofs can be erased (IIUC).

But besides just being a language, Haskell is a whole ecosystem. It's not an amazing ecosystem, but it's good enough for serious work. Idris is not and may never be. A fully-supported Dependent Haskell would be huge for dependent types in practice.

> Idris is strict, unlike Haskell.

"The next Haskell will be strict." — Simon Peyton-Jones

Reply on news.ycombinator.com