The Accessibility of Type Theory Research

[Shriram Krishnamurthi <address@hidden>]

Peter J. Wasilko wrote:

> But more to the point, if a significant fraction of the language
> designers on this list have a hard time penetrating the language of
> papers that deal with the tradeoffs among alternate typing schemes and
> annotation styles, how can we expect language implementors to make
> effective use of this research or for average programmers to make
> effective use of tools that embody it?

I won't deny that many computer science research papers can be written
much better.  Heck, I have to read these for a living.  I even write
some for a living. (-: (Ambiguity intentional.)

That said:

While there are several home care books, most people ultimately refer
to a trained doctor, right?  (As Twain reputedly said, "Beware of
health books, you might die of a misprint.")

It's even better in language design: there's no certification board
that prevents you from hanging out your shingle.  But surely that
doesn't mean dialog between experts should be reduced to a level that
everyone can understand.

(As a personal aside, do you eschew legal language when speaking about
legal matters to a fellow member of the bar?  If so, I'm rather
curious about how well this works.  Do you think legal language exists
*solely* to create a barrier to comprehension by people not already
members of the club?)

More positively, in my text I have made a small attempt to teach how
to read type judgments:

  http://www.cs.brown.edu/courses/cs173/2003/Textbook/2003-10-27.pdf

(I'll gladly improve the text in response to concrete comments and
criticisms.)

Shriram