[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 : 58 points
Date : 2025-04-07 17:42 UTC (5 hours 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.
___________________________________________________________________
(page generated 2025-04-07 23:00 UTC)