[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: address@hidden*Subject*: Re: The Accessibility of Type Theory Research*From*: Daniel Yokomiso <address@hidden>*Date*: Thu, 20 Nov 2003 08:20:15 -0300 (ART)*In-reply-to*: <r02000200-1028-7C0C085A1B0C11D8BB50003065B28AFA@[168.100.204.225]>*Sender*: 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

**Follow-Ups**:**Re: The Accessibility of Type Theory Research***From:*"Peter J. Wasilko" <futurist@cloud9.net>

**References**:**The Accessibility of Type Theory Research***From:*"Peter J. Wasilko" <futurist@cloud9.net>

- Prev by Date:
**Re: The Accessibility of Type Theory Research** - Next by Date:
**Of Legal Language and CS Notation** - Previous by thread:
**Re: The Accessibility of Type Theory Research** - Next by thread:
**Re: The Accessibility of Type Theory Research** - Index(es):