Yes, it's exciting problem. I think it's good he's articulated it.
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.
Comments
Yes, it's exciting problem. I think it's good he's articulated it.
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.
> Yet in ways, this paper seems like a confession that he's reached something of a brick wall with the problem.
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'.)