Ironically I've come up a bit short on how to use dependent types to do anything more advanced than matching handlers' to route types, which Servant [2] can do fantastically already.
I would love to be able to write types that describe, e.g., assumptions made about external resources, so that I can prove that "assuming my DB has such-and-such a latency, my page will always render in such-and-such a time" or something similar - but it's a bit beyond me at the moment.
As a rule I find that people who take the common, simplistic, tweet-length view of British rule (i.e. that it became rich by stealing from India, that it was the deliberate invoker of India's famines, that it was racist even by its times standards, etc), assume that anyone who disagrees isn't aware of basic history.
I've also noticed that there's always an (annoying) triumphal 'gotcha' when they link to some short-form essay mentioning basic facts, denied by nobody, of the famines and loss of relative share of GDP suffered by India etc.
Again, _everyone knows this_. It comes across as naive and arrogant to assume otherwise.
The effect British rule had in India (and everywhere) was extremely nuanced, and there is a huge amount of interesting history to be debated. After all, we're talking about a subcontinent over a 350 year time period.
The British, for instance, banned the practices of Sati (burning widows alive) and of infanticide, and explicitly allowed Indians to compete on equal terms with the British in examinations to enter the Indian Civil Service.
There's very little consensus amongst historians whether or not they were responsible for the famines India suffered at the time, or if they even made any net money from India whatsoever, given their constant fear of raising taxes.
I'm not necessarily trying to take a position either way, by the way, just begging people who are nodding along to some of these bumper-sticker anti-colonialism comments to read more deeply into what is an unimaginably huge subject.
To add to your point, there’s very little consensus among people on the subcontinent about it. My mom and aunts are borderline monarchists. My dad is a republican, and growing up I heard him complain about the British dividing and conquering by creating tensions between Muslims and Hindus. But even he readily credits the British for developing the region’s laws and institutions.
For canal boating, absolutely. Maybe 20-30k for a cheaper boat. Can moor for free. Coal and fuel maybe £100 a month each, depending on how much you travel/if you have solar etc. You do need to black your hull every few years, but they’re generally sturdy and don’t need much more than that.
I agree with you - but the standards elsewhere seem to be so much lower even than here that I think it's (possibly) worthwhile having political discussions on HN.
Of course, I would love to know of a place that discusses things even more sensibly.
You should look at this like software development. New programming languages come out that try to solve the problems of all the previous languages and unify everyone to code and be productive in the same ecosystem...until another language comes out etc.
It's very hard to get everyone to agree how code plus mathematics should be written. There's a lot of fragmentation and ongoing attempts to unify.
Not true, we certainly have those that start at 8. Consider a ~45m commute and time to get ready, and waking up at 6 something is not unheard of. (I personally had to wake up at 5:45 to catch a bus to a school over an hour away).
What is not true? I'm just going off of what the gpp mentioned.
Now I don't quite understand what you have written here because you just say "we", but assuming you mean work colleagues then I think there is a bit of a difference between someone starting at 8, and making kids catch a bus at 5:45 so that they can start school an hour later at 6:45? That's not waking up at 6, that is out of the house before 6, and while you survived, it really shouldn't be necessary in a 1st world country.
While you did it, there is plenty of evidence that you could have done even better if you weren't subjected to it.
I've loved being able to use Lean's macro system to write JSX-like HTML:
Ironically I've come up a bit short on how to use dependent types to do anything more advanced than matching handlers' to route types, which Servant [2] can do fantastically already.I would love to be able to write types that describe, e.g., assumptions made about external resources, so that I can prove that "assuming my DB has such-and-such a latency, my page will always render in such-and-such a time" or something similar - but it's a bit beyond me at the moment.
[1] https://github.com/alex-wellbelove/LeanServer [2] https://hackage.haskell.org/package/servant