* "programmers who do not wish the ordering guarantees are entitled not to pay and not to receive", or "We could plough on with proof and, coughing, push this definition through, but tough work ought to make us ponder if we might have thought askew." (https://strathprints.strath.ac.uk/51678/7/McBride_ICFP_2014_...)
Their papers are also generally presented very well - easy to follow, as these things go (by which I mean it's actually feasible to work through with a pencil and paper and understand the contents within a few hours). I really recommend PolyTest which is particularly edifying; before I learned the "avoid the green slime" principle, dependent types were a battle, but when I read it I was enlightened, and it's super interesting to watch the types evolve as the problem is understood.
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 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.
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.
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.
Final line is gold.
> we sometimes blur the distinctions between these distinctions
> venerable program extraction algorithm
> type inference seems a timid virtue
> it is a nuisance that the kind-level ∀ is compulsorily implicit
It sounds fun to do academic research, is that why there's an oversupply of PhD students?
Conor has always had a turn of phrase - every paper has at least one gem.
* "the engineering of coincidence is replaced by the propagation of consequence" (https://www.cs.ox.ac.uk/projects/utgp/school/conor.pdf)
* "programmers who do not wish the ordering guarantees are entitled not to pay and not to receive", or "We could plough on with proof and, coughing, push this definition through, but tough work ought to make us ponder if we might have thought askew." (https://strathprints.strath.ac.uk/51678/7/McBride_ICFP_2014_...)
* "be minimally prescriptive, not maximally descriptive" (https://personal.cis.strath.ac.uk/conor.mcbride/PolyTest.pdf)
Their papers are also generally presented very well - easy to follow, as these things go (by which I mean it's actually feasible to work through with a pencil and paper and understand the contents within a few hours). I really recommend PolyTest which is particularly edifying; before I learned the "avoid the green slime" principle, dependent types were a battle, but when I read it I was enlightened, and it's super interesting to watch the types evolve as the problem is understood.
Yes, it's phd students there's an oversupply of, not mediocre web devs at ad companies
You can use fun language for any discpline. Even stamp collecting.
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.