Types Considered Harmful
lambda-the-ultimate.org
lambda-the-ultimate.org
In particular something like this will (I think) be a perfect substrate for refactoring parsers, semantic diff tools, and other neat stuff...
Yet in ways, this paper seems like a confession that he's reached something of a brick wall with the problem.
If you look at the bidirectional link, http://lambda-the-ultimate.org/node/1526, he goes over a series of partial solutions before discussing his (very general) approach. I suspect that a workable system might be better through putting together all the classes of partial-but-well-behaved solutions rather than attempting a fully general solution.
Another thing that interests me is bidirectional code that operates on itself.
If "the problem" is that of providing accurate, fully static types for this type of transform, then of course yes. ;)
I think the end result is improved (easier to learn and more flexible) for consciously relaxing that goal, however.
(Edit to muse: I think 'relaxing' is a far more intelligent & interesting approach to overly-ambitious goals, as opposed to 'abandoning'.)
His website: http://www.cis.upenn.edu/~bcpierce/
two PhDs for Haskell
This presentation is so lighthearted... I realy like it.
A lot of academic research doesn't acknowledge that the reason a working programmer wants a tool that is really simple is because I am constantly working with the threat of my project becoming overwhelmingly complex. A really simple, clear tool lets me keep a little more distance from that final, looming complexity.
Sometimes I pretty much know what assembly I want and it's much easier to make a C compiler produce it than to get GHC to produce it.
One example is multiplication in the complex roman numeral system vs. (our) simple arabic numeral system.
Another example is PHP (tool) for webapps (task). Worked for YouTube and CDBaby. -- Honestly, I think the concept of embedding commands in HTML is brilliantly simple, because the program is largely isomorphic to the result, making it intuitive to reason about. [disclaimer not a webapp developer]
Simple until you have to come in and maintain it. There are many levels of simple. What is often simple for the original writer is horrible for the person who picks it up later on and has to extend and maintain it.
1. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.11....
I also found this one quite interesting: http://www.cs.brown.edu/~arjun/public/poly-contracts.pdf
http://www.eiffel.com/developers/design_by_contract.html
I actually have trouble with mathematics, because it is so flexible. For example, equality of sets A and B is typically shown by saying that every element of A is in B, and every element in B is in A. Why on earth do they do that? Why not just say they're the same??!
One advantage is it gives you the flexibility to demonstrate the first limb using one technique, and the second limb with a completely unrelated approach. I saw one example of showing equivalence of language defined by a class of grammars, and a language defined by constraints over sequences. You could even use a constructive and a non-constructive proof for each half.
It's a way of subdividing that is decoupled.
"Considered Harmful" Essays Considered Harmful http://meyerweb.com/eric/comment/chech.html