Re: The Accessibility of Type Theory Research

[Daniel Yokomiso <address@hidden>]

 --- "Peter J. Wasilko" <futurist@cloud9.net>
escreveu: >
[snip]
> I think this was intended as a critique of the
> accessibility of the
> notation used to express the Operational Semantics
> of modern type
> theory, which seems to demand a somewhat greater
> level of mathematical
> sophistication than most average language
> aficionados bring to the
> table.

IME in every field of science you need a "... somewhat
greater level of mathematical sophistication than most
average ... aficionados bring to the table.". take
physics, for example. It's true that you can explain
the basic concepts and use analogies to "dumb down"
things like general relativity and quantum mechanics,
but if you want to truly understand the details you
need some mastery in calculus, tensors, etc.. Stephen
Hawking wrote great books "for the masses" but try to
read one of his research papers (I did it when I
studied physics in college, it wasn't pretty ;). 

> Thus to say that it takes more than one pass for
> most people to fully
> grok the chapters of Pierce would be putting it
> mildly.

"Fully grok" something is pretty hard. In "How do we
tell truths that might hurt?" Dijkstra said:
"Programming is one of the most difficult branches of
applied mathematics; the poorer mathematicians had
better remain pure mathematicians" and I agree with
him. CS is a hard to grok, even things that people
think are simple and basic (e.g. OO) are very
difficult to fully grok. Most of OO people don't even
heard about the sigma calculus but think they "grok"
objects.

[snip]

> 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?

IMHO language implementors should read these papers
over and over again until their eyes bleed. Language
design isn't an easy task, unless you want yet another
toy language.

> I think I'm feel myself being drawn into Shriram's
> fourth category.
> 
> --- Peter

There's a series of articles in the Journal of Object
Technology about Type Theory, they're well written,
easy to understand and offer a good introduction to
some aspects. Here's a link to the last one:


The Theory of Classification, Part 9: Inheritance and
Self-Reference
By Anthony J.H. Simons
http://www.jot.fm/issues/issue_2003_11/column2


Best regards,
Daniel Yokomiso.

"The structure of the data guides the computation;
unstructured data is anathema."
 -Brian McNamara

______________________________________________________________________

Yahoo! Mail: 6MB, anti-spam e antivírus gratuito! Crie sua conta agora:
http://mail.yahoo.com.br