> 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?
* "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.