Home » forums » LtU Forum

Type Theories

Hi,

I have a question: what're the benefits of investigating type theories when designing new programming construct/model/paradigm? I read through some of the recent interesting papers posts on LtU. Always, the authors dedicate a section to formalize their new programming constructs under various lambda calculi. I'm asking this from the perspective that how does this help us in designing better programming languages? What kind of insights will such process of formalisation give us?

I'm genuinely interested in understanding this. I've been considering of doing a PhD in investigating better programming constructs. I can say I know untyped lambda calculus. Beyond that, I'm not particular strong in "deeper" type theories and other formal systems (e.g. denotational semantics). I'm wondering how a PhD thesis will stand up if it isn't strong in this aspect.

If I want to brush up my skills/knowledge in this area, I suppose the text "Types and Programming Languages"
by Benjamin C. Pierce will be my starting point? Any other suggestions?
--
John

By sciomako at 2007-08-16 07:35 | LtU Forum | previous forum topic | next forum topic | other blogs | 5921 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

TAPL

TAPL is indeed a good place to start. The first chapter (the introduction) talks about the things you asked about.

By Ehud Lamm at Thu, 2007-08-16 08:20 | login or register to post comments

Formalizing

TAPL (and its successor, Advanced Topics in Types and Programming Language) is definitely recommended. To get you started:

  • Formalizing semantics makes it accessible to formal proofs (rather than hand-waving arguments).
  • Formal proofs are important for type systems, as it's all too easy to have inconsistent axioms, incomplete typing, or even undecidable types. Formalizing and proofing properties helps you "debug" your type system. (I didn't read it completely, but this seems to give a good argument: http://www.cs.fiu.edu/~smithg/cop4555/valrestr.html)
  • Type systems give you static guarantees, and guarantees allows you to worry about other parts of your program. (Provided, the type system doesn't constrain the programmer too much, so that she has to constantly fight the type-checker.)
  • Programming languages without formal semantics (or at least quasi-formal semantics) tend to have really ugly border cases. Many PLs do live quite well without those, but it can become really difficult to work with them -- e.g., different implementations might work differently.
  • You cannot prove a program correct, if it is written in a language without a formal semantics. (But you can chose a probabilistic approach, or argue based on experience, or consider the possibility program bugs in your overall design like, e.g., Erlang does.)

There's much, much more to this, but this should give you an idea.

By Thomas Schilling at Thu, 2007-08-16 11:12 | login or register to post comments

A more general suggestion

One trap that a lot of young grad students seem to fall into (I did, once) is getting excited about developing a particular solution, rather than starting by finding an interesting problem. It's easy to say that it would be cool if language X had feature Y, and indeed a lot of excellent work has been done adding Y to X for various X and Y. One thing (but not the only thing) that differentiates good research from cool hacks is that the good research solves a real problem. I'm sure you have ample motivation for investigating some new programming constructs, but be sure to start with the motivation, rather than the novelty or excitement of a particular language extension.

I agree with the TAPL recommendations, though, and I would add that most interesting language properties seem to be more naturally treated by operational or Hoare-style semantics than by denotational semantics. As far as how well a PhD thesis on new programming models or constructs will stand up without formalism -- well, that's up to your committee, but it seems like you probably won't be able to avoid it altogether. :-)

By Will Benton at Thu, 2007-08-16 15:34 | login or register to post comments

I must respectfully disagree in part

Will Benton: I would add that most interesting language properties seem to be more naturally treated by operational or Hoare-style semantics than by denotational semantics.

For a counterpoint to this, please see A Certified Type-Preserving Compiler From Lambda Calculus to Assembly Language. For a very quick, very good visual overview of the main points, I recommend these slides (PDF) from Adam Chlipala's PLDI '07 talk.

By Paul Snively at Thu, 2007-08-16 18:23 | login or register to post comments

Thanks

Paul, thanks for mentioning this reference. I take your point, but I don't think I was totally off-base in my claim for a couple of reasons: (1) most people doing this sort of work are currently using operational or axiomatic semantics (indeed, Chlipala claims that his very use of denotational semantics is novel), and (2) if I understand correctly, there are still several nontrivial limitations of the denotational approach that apply to many interesting language features.

By Will Benton at Thu, 2007-08-16 20:37 | login or register to post comments

Good points

Those are both good points, and I should also mention Xavier Leroy's Coinductive Big-Step Operational Semantics paper. Using big-step operational semantics, as opposed to small-step, is also fairly novel; the paper's abstract provides the requisite motivation. A commonality of Mr. Chlipala's and Dr. Leroy's work, I think, is that both attempt to reduce the cost of applying mechanized metatheory to some of the tedious, error-prone proofs that some of us like to see applied to programming language design.

No doubt there are challenges to the denotational approach to specifying programming language semantics, some of which are addressed by combining the denotational semantics with dependently-typed abstract syntax, some of which will require further investigation and exploration. This investigation seems likely to be worthwhile when you examine the scope of traditional types of proofs that are no longer necessary given the application of technologies from Mr. Chlipala's work—but of course, this observation only holds if you accept the proposition that more mechanized metatheory is desirable rather than the same amount or less.

By Paul Snively at Thu, 2007-08-16 21:08 | login or register to post comments

I understand the main

I understand the main driving force of most researches is to solve real problems. In actual fact, I think it's relatively hard for me to fall into the trap of creating "solution" that looks for problem. Reasoning being I'm not that young. :-) I graduated more than 10 years ago and have been a programmer since then. I have seen problems in real world that I think can be solved with program constructs with more powerful abstraction mechanisms and expressiveness.

By sciomako at Fri, 2007-08-17 06:56 | login or register to post comments

Type theory and FP

After reading the topic and made a search, i found this: http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/
Looks also interesting. Anyone know the book?

By Zsolt Szalai at Fri, 2007-08-17 06:29 | login or register to post comments