[HN Gopher] Hasochism: The pleasure and pain of dependently type...
___________________________________________________________________
Hasochism: The pleasure and pain of dependently typed Haskell
programming [pdf] (2013)
Author : fanf2
Score : 93 points
Date : 2025-04-07 17:42 UTC (1 days ago)
(HTM) web link (personal.cis.strath.ac.uk)
(TXT) w3m dump (personal.cis.strath.ac.uk)
| moomin wrote:
| Final line is gold.
| kubb wrote:
| > 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?
| smus wrote:
| Yes, it's phd students there's an oversupply of, not mediocre
| web devs at ad companies
| clusterfook wrote:
| You can use fun language for any discpline. Even stamp
| collecting.
| Smaug123 wrote:
| 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.
| kreyenborgi wrote:
| twelve years have passed - is DT less painful today?
| clusterfook wrote:
| 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.
| IshKebab wrote:
| 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...
| lambda_foo wrote:
| 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.
| agentultra wrote:
| 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.
| HKH2 wrote:
| Isn't Idris basically Haskell with DT?
| wk_end wrote:
| 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.
| jech wrote:
| > Idris is strict, unlike Haskell.
|
| "The next Haskell will be strict." -- Simon Peyton-Jones
___________________________________________________________________
(page generated 2025-04-08 23:02 UTC)