September 26th, 2010

beartato phd

(no subject)

At ICFP! Well, the associated workshops that are going on today at least.

Dave MacQueen is doing a talk about how to make good error messages for type errors. The idea seems to be rather straightforward and nice; you annotate identifiers' types with their provenance, propagate this information all the way down to the base types, pass them around during unification, and reveal to the user the provenance of a pair of types when they clash.

It was pointed out that the text-region arguments are only used when the unification fails; I wonder if there's some ultra-lazy way to do it (which doesn't really mean doing two-pass typing...) that only does that computation after it notices unification has failed.

Bob asked a question (or kind of made a comment with rising intonation) about the elephant in the room which is that the problem of type error messages is, as far as the mathematics is concerned, entirely undefined: an unsolvable CSP is just unsolvable, there are no "culprits". And yet (though admittedly I haven't seen a lot of other work in this niche) I rather liked this talk; I want to say that you could reduce the informal-to-formal gap by studying the formal question of which declarations (of top-level typed constants) you might have to minimally vary to make the constraint-solving problem solvable. In other words, figure out a (here's the informal bit:) plausible metric to put on the space of all CSPs, and then at least you're left with a formal problem of finding the nearest solution.
beartato phd

(no subject)

Had a great time already having dinner with people; aij, chrisamaphone, Carl Eastlund, lindseykuper who I got to meet for the first time, Jamie, a dude from Northeastern named Stevie, and maybe that was it? I can't tell if I'm forgetting someone. Ran into Dan Licata on the way back and talked about proof irrelevance some.