Mon, 26 September 2011
New Idea: Fill in all of Daniel's esoteric type theory references!!! Send references and links to scala-types@googlegroups.com Comments[2]
|
- Just listened to this episode while walking on a warm summer's night here in Melbourne. Enjoyed it. Covered alot of rare stuff I'm into or spend time pondering, like what is {dependent types | object-orientation | objects-as-modules} good for?
I know its hard to balance spontaneity and sparkle against having a logical flow and being comprehensible. This episode felt weighted to the former (Markus Voelter at SERadio is a great example of doing the latter well).
By the end, Daniel had offered a decent (IMO) definition/explanation of objects as Record of Functions + Open-recursion, then Runar asked "what's that actually useful for?". That's kind of the $1M question. And then, you guys apparently decamped to the bar, the podcast ended, and the question went unanswered, to the listener's ears at least... - Some clarification on the "Phil Wadler" story - it wasn't typestate, it was dependent types (in the context of Agda). Phil was attending a course run by Conor McBride (Strathclyde Uni) on Agda. Phil was looking to provide a proof that a selection sort produced a sorted sequence, something that was far beyond what Conor was prepared to teach in this course, which was mostly intended to be an introduction to using dependent types through Agda for graduate students. Phil eventually managed to produce the proof within Agda but the time it took and the length of the definition (relative to what it was actually doing) demonstrated that the effort is not always justified.
However you could argue that with something as foundational as sorting, something that is likely to be reused, the effort may be justified as the benefit is shared by a lot of people.
Post your comment:
Follow us on twitter!