Re: [Haskell] Articles on the value of strong typing
On 3/26/07, Jacob Atzen [EMAIL PROTECTED] wrote: This lead me to the question: Are there any scientific empirical studies of the values of static / stronger type systems as found in Haskell, C# or Java in real world settings? Or any studies comparing weaker type systems in terms of programmer efficiency, defect ratio, etc. It's certainly not scientific, but there is a recent entry on Lambda the Ultimate that contains some empirical evidence: http://lambda-the-ultimate.org/node/2147 -- Martin ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Post-doc position in Martin Odersky's group, EPFL, Switzerland
EPFL Lausanne Programming Methods Group Prof. Martin Odersky We have an open position for a postdoctoral researcher in the Programming Methods Group at EPFL. The research of our group is centered on Scala, a new programming language which fuses functional and object-oriented programming and which interoperates at the same time with Java and .NET. Scala pushes the state of the art in type systems for component abstractions and composition. It also provides many new concepts for web programming. Here are some of our current research directions: - Further developments in the Scala language design - High-level optimizations - Type systems for object-oriented and functional languages - Programming language support for XML - Component technology. - Reliable software, verification, testability. If you work in some of these research areas and are interested in both system building and theory, you will find an active and friendly research environment at Lausanne. The appointment is for one year initially with renewals possible up to three years. The position is open from June, 2005, but later starting dates can also be considered. Compensation is competitive at CHF 80K+ (1 CHF ~~ 0.83 U.S$), depending on age and experience. Informal inquiries about the position may be addressed to [EMAIL PROTECTED] Formal applications should be sent by e-mail to the following address: Mme Yvette Dubuis [EMAIL PROTECTED] Tel. +41 21 693 5202 Fax +41 21 693 6660 To be guaranteed full consideration, applications should be received by May 15th, 2000. Applications should consist of a curriculum vitae, a publication list, and the names of three personal references. Please ask your references to send their letters directly to [EMAIL PROTECTED] EPFL Lausanne is one of two federal universities in Switzerland. It has one of the most nationally diverse research, teaching and learning communities in Europe. Lausanne is situated in very attractive surroundings in the French-speaking part of Switzerland, on the shore of Lake Geneva, in close proximity to the Alps. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[ANN] The Scala programming language
We'd like to announce availability of the first implementation of the Scala programming language. Scala smoothly integrates object-oriented and functional programming. It is designed to express common programming patterns in a concise, elegant, and type-safe way. Scala introduces several innovative language constructs. For instance: - Abstract types and mixin composition unify ideas from object and module systems. - Pattern matching over class hierarchies unifies functional and object-oriented data access. It greatly simplifies the processing of XML trees. - A flexible syntax and type system enables the construction of advanced libraries and new domain specific languages. At the same time, Scala is compatible with Java. Java libraries and frameworks can be used without glue code or additional declarations. The current implementation of Scala runs on Java VM. It requires JDK 1.4 and can run on Windows, MacOS, Linux, Solaris, and most other operating systems. A .net version of Scala is currently under development. For further information and downloads, please visit: scala.epfl.ch == Martin Odersky and the Scala team, Swiss Federal Institute of Technology, Lausanne (EPFL). ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
FOOL 9 Call for Participation
CALL FOR PARTICIPATION The Ninth International Workshop on Foundations of Object-Oriented Languages FOOL 9 Sponsored by ACM SIGPLAN January 19, 2002 Portland, Oregon Following POPL '02 The search for sound principles for object-oriented languages has given rise to much work on the theory of programming languages during the past 15 years, leading to a better understanding of the key concepts of object-oriented languages and to important developments in type theory, semantics, and program verification. The FOOL workshops bring together researchers to share new ideas and results in these areas. The next workshop, FOOL 9, will be held in Portland, Oregon, on Saturday January 19, 2002, the day after POPL'02. To register for the workshop, use the standard registration form, available through: http://www.cse.ogi.edu/PacSoft/conf/popl -- Preliminary schedule Saturday, January 29, 2002 8:40 Start 8:45-9:45 Invited Talk Distributed Objects - The Next 10 Years Andrew Black 9:45-10:15 Break 10:15-12:15 Session 1 Modular Typechecking for Hierarchically Extensible Datatypes and Functions Todd Millstein, Craig Chambers Type-checking multi-methods in ML (A modular approach) Daniel Bonniot First-Class Modules for Haskell Mark Shields, Simon Peyton Jones Extensible Objects Without Labels Christopher Stone 12:15-14:00 Lunch 14:00-15:30 Session 2 Modern Concurrency Abstractions for C# Nick Benton, Luca Cardelli, Cedric Fournet OO languages late-binding signature Antoine Beugnard A Semantics for Advice and Dynamic Joint Points in Aspect-Oriented Programming Mitchell Wand, Gregor Kiczales, Christopher Dutchyn 15:30-16:00 Break 16:00-17:30 Session 3 Automatic Discovery of Read-Only Fields, Jens Palsberg, Tian Zhao, Trevor Jim. Generation of Verification Conditions for Abadi and Leino's Logic of Objects Francis Tang, Martin Hofmann Simple Type Inference for Structural Polymorphism Jacques Garrigue - Steering Committee: Martin Abadi, University of California, Santa Cruz Kim Bruce, Williams College Luca Cardelli, Microsoft Research Kathleen Fisher, ATT Labs Benjamin Pierce, University of Pennsylvania (chair) Didier Remy, INRIA Rocquencourt Program Committee: Viviana Bono, Universita di Torino Craig Chambers, University of Washington Erik Ernst, University of Aalborg Giorgio Ghelli, University of Pisa Atsushi Igarashi, University of Tokyo Shriram Krishnamurthi, Brown University Martin Odersky, EPFL (chair) [EMAIL PROTECTED] Clemens Szyperski, Microsoft Research Jan Vitek, Purdue University ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: rank 2-polymorphism and type checking
PS to my earlier message. I am not at all certain that the Odersky/Laufer thing would in fact solve Janis's problem. You want not only a rank-3 type, but also higher-order unification, since you want to instantiate 't' to \c. forall d . (c-d) - d - d Simon, You are correct to have doubts. Indeed our system would not handle this case, as type variables can only be instantiated to monomorophic types, not to type schemes. The closest you can get to it is to wrap the instance type in a type constructor. I.e. `t' could be instantiated to T (\c. forall d . (c-d) - d - d) where T was declared newtype T = T (\c. forall d . (c-d) - d - d) But I guess that does not solve Janis's problem. Cheers -- Martin ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Final CFP: FOOL 9 -- Foundations of Object-Oriented Languages
FINAL CALL FOR PAPERS The Ninth International Workshop on Foundations of Object-Oriented Languages FOOL 9 Sponsored by ACM SIGPLAN January 19, 2002 Portland, Oregon, USA Following POPL '02 http://www.cs.williams.edu/~kim/FOOL/fool9.html Deadlines Submissions: October 12, 2001 Notifications: November 12, 2001 Final versions: December 10, 2001 The search for sound principles for object-oriented languages has given rise to much work on the theory of programming languages during the past 15 years, leading to a better understanding of the key concepts of object-oriented languages and to important developments in type theory, semantics, and program verification. The FOOL workshops bring together researchers to share new ideas and results in these areas. The next workshop, FOOL 9, will be held in Portland, Oregon, on Saturday January 19, 2002, the day after POPL '02. Submissions for this event are invited in the general area of foundations of object-oriented languages; topics of interest include language semantics, type systems, program analysis and verification, programming calculi, concurrent and distributed languages, and database languages. The main focus in selecting workshop contributions will be the intrinsic interest and timeliness of the work, so authors are encouraged to submit polished descriptions of work in progress as well as papers describing completed projects. A web page will be created and made available as informal electronic conference proceedings. Submission procedure We solicit submissions on original research not previously published or currently submitted for publication elsewhere, in the form of extended abstracts. These extended abstracts should not exceed 5000 words (approximately 10 pages); shorter extended abstracts (e.g., 2000 words) are often sufficient. Submissions should be e-mailed to [EMAIL PROTECTED] by Friday, October 12, 2001, using Postscript or PDF. Each submission may be included inline in a message or as a MIME attachment only. We may not be able to consider late submissions, or submissions that do not have a working and attended return e-mail address. (If electronic submission is impossible, please contact the program chair in September.) Receipt of the submissions will be acknowledged by e-mail. Authors should inquire in case a prompt acknowledgment is not received. Correspondence and questions should be sent to [EMAIL PROTECTED] Steering Committee Martin Abadi, Bell Labs Kim Bruce, Williams College Luca Cardelli, Microsoft Research Kathleen Fisher, ATT Labs Benjamin Pierce, University of Pennsylvania (chair) Didier Remy, INRIA Rocquencourt Program Chair Martin Odersky, Swiss Federal Institute of Technology Lausanne, [EMAIL PROTECTED] Program Committee Viviana Bono, Universita di Torino Craig Chambers, University of Washington Erik Ernst, University of Aalborg Giorgio Ghelli, University of Pisa Atsushi Igarashi, University of Tokyo Shriram Krishnamurthi, Brown University Clemens Szyperski, Microsoft Research Jan Vitek, Purdue University ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
CFP: FOOL 9 -- Foundations of Object-Oriented Languages
Call for Papers The Ninth International Workshop on Foundations of Object-Oriented Languages FOOL 9 Sponsored by ACM SIGPLAN January 19, 2002 Portland, Oregon, USA Following POPL '02 http://www.cs.williams.edu/~kim/FOOL/fool9.html Deadlines Submissions: October 12, 2001 Notifications: November 12, 2001 Final versions: December 10, 2001 The search for sound principles for object-oriented languages has given rise to much work on the theory of programming languages during the past 15 years, leading to a better understanding of the key concepts of object-oriented languages and to important developments in type theory, semantics, and program verification. The FOOL workshops bring together researchers to share new ideas and results in these areas. The next workshop, FOOL 9, will be held in Portland, Oregon, on Saturday January 19, 2002, the day after POPL '02. Submissions for this event are invited in the general area of foundations of object-oriented languages; topics of interest include language semantics, type systems, program analysis and verification, programming calculi, concurrent and distributed languages, and database languages. The main focus in selecting workshop contributions will be the intrinsic interest and timeliness of the work, so authors are encouraged to submit polished descriptions of work in progress as well as papers describing completed projects. A web page will be created and made available as informal electronic conference proceedings. Submission procedure We solicit submissions on original research not previously published or currently submitted for publication elsewhere, in the form of extended abstracts. These extended abstracts should not exceed 5000 words (approximately 10 pages); shorter extended abstracts (e.g., 2000 words) are often sufficient. Submissions should be e-mailed to [EMAIL PROTECTED] by Friday, October 12, 2001, using Postscript or PDF. Each submission may be included inline in a message or as a MIME attachment only. We may not be able to consider late submissions, or submissions that do not have a working and attended return e-mail address. (If electronic submission is impossible, please contact the program chair in September.) Receipt of the submissions will be acknowledged by e-mail. Authors should inquire in case a prompt acknowledgment is not received. Correspondence and questions should be sent to [EMAIL PROTECTED] Steering Committee Martin Abadi, Bell Labs Kim Bruce, Williams College Luca Cardelli, Microsoft Research Kathleen Fisher, ATT Labs Benjamin Pierce, University of Pennsylvania (chair) Didier Remy, INRIA Rocquencourt Program Chair Martin Odersky, Swiss Federal Institute of Technology Lausanne, [EMAIL PROTECTED] Program Committee Viviana Bono, Universita di Torino Craig Chambers, University of Washington Erik Ernst, University of Aalborg Giorgio Ghelli, University of Pisa Atsushi Igarashi, University of Tokyo Shriram Krishnamurthi, Brown University Clemens Szyperski, Microsoft Research Jan Vitek, Purdue University ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Postdoc and PhD Student Position Announcement
EPFL Lausanne Programming Methods Group Prof. Martin Odersky For the Project "Practical Implementations of Functional Nets", funded in part by the Swiss National Science Foundation, we are looking for * Postdoctoral researcher (1 or 2 year term), * PhD student (fully funded). The project explores novel implementation techniques for programming languages which lie in the intersection of the functional, object-oriented, and concurrent language families. The positions offer exciting opportunities for research in a young but rapidly growing group. Postdoctoral applicants should have a strong background in at least two of the following areas: - programming language design and implementation, - functional programming, - object-oriented programming, - concurrent and distributed systems. The ideal candidate will have a lively interest in both system building and theory. She or he will enjoy the opportunity to work collaboratively with other researchers and PhD students at the programming methods group at EPFL. The appointment is for one year with a possible renewal. PhD student applicants should have strong research interests in one or more of the areas given above and should like to work on the boundary betwen theory and practice. They should have obtained a degree equivalent to a Swiss EPFL diploma (usually this is a master's degree, although a B.Sc. with honors might also be considered). The duration of PhD studies at EPFL is typically 4 years. Both positions are open from Fall 2000, with a starting date in Spring or Fall 2001 also being possible. Compensation is competetive: CHF 70K+ for the post-doc position, and CHF 50K+ for the PhD student position (1 CHF ~~ 0.6 U.S$). Informal inquiries about the positions may be addressed to [EMAIL PROTECTED] Formal applications should be sent by e-mail to the following address: Madame Yvette Dubuis [EMAIL PROTECTED] Tel. +41 21 693 5202 Fax +41 21 693 6660 To be guaranteed full consideration, applications should be received by October 15th, 2000. Applications should consist of a curriculum vitae, a publication list, and the names of three personal references (two for PhD students). Please ask your references to send their letters directly to [EMAIL PROTECTED], there is no need for a request from us. EPFL Lausanne is one of two federal universities in Switzerland. It has one of the most nationally diverse research, teaching and learning communities in Europe. Lausanne is situated in very attractive surroundings in the French-speaking part of Switzerland, on the bord of Lake Geneva, in close proximity to the Alps. [apologies if you receive this on multiple lists --MO]
Re: Records and type classes
It seems to be the season for records -- three proposals already and I'm going to add a fourth one! Phil Wadler, Martin Wehr and I have recently completed a paper that describes a radical simplification of type classes. We restrict overloading to functions that have the instance type as first argument. We also do away with class declarations altogether, and keep only a simple form of instance declaration. This is described in the technical report "A second look at overloading", to be found in the papers section of my WWW home page at http://wwwipd.ira.uka.de/~odersky. One nice aspect of our proposal is that it is very much in the spirit of the Hindley/Milner system in that ambiguous types are impossible and we can prove that "well-typed programs cannot go wrong". Another nice aspect is that it gives us polymorphic record typing for free - Ohori's version of it, to be precise. By contrast, current Haskell classes would give us only monomorphic records. Maybe not so nice is that some features of current Haskell cannot be expressed, such as overloaded numbers and functions like "fromInteger". But note that these are precisely the features that seem to cause a lot of problems in current Haskell -- ambiguous types and the monomorphism restriction, to name just two. In general, there are some interesting relationships between record typing and overloading. A good way to look at it is by comparing the role of record field labels with the role of other identifiers. In ML this correspondence made is very clear by writing the selection of field "l" as "#l r", i.e. the label acts like a function identifier. The way I see it, various record type implementations and proposals can be classified as follows. CAML Records : labels behave like non-overloaded identifiers. John Peterson's Proposal Different record types must have different labels. SML Records : labels behave like overloaded identifiers, using ML's overloading concept. Compiler complains if record type is not statically known. Ohori's Records : labels behave like overloaded identifiers, using our overloading type system. Compiler never complains. Mark Jones' records : a special instance of Mark's framework for qualified types. (Mark, I don't have your thesis at hand right now, so please fill in or correct if this is inaccurate). I don't know enough about Giuliano Procida's proposal to be able to classify it. Cheers -- Martin
Re: Multiple parameters to classes
Phil Wadler writes: The GRASP team at Glasgow is putting the finishing touches on a paper that formally describes type classes as implemented in Haskell, which you may find helpful. We will post a pointer to this paper when it's done. I hope Mark Jones and Martin Odersky will also post pointers to their recent work in this area. Kung Chen, Paul Hudak, and I have looked into the problem of extending Haskell's type system such that container type classes become possible. Examples of such classes are "Sequence" (with instance types List and Array, for instance), or "Monad". Last year, there was some discussion on this mailing list as to whether this requires second-order unification. Well, fortunately it doesn't. The results are found in the paper "Parametric Type Classes". It can be picked up by anonymous ftp from nebula.cs.yale.edudirectory: pub/haskell/papers -- Martin
Re: Existential types
Nigel, I am sorry if I have said something wrong in my posting. I agree that the example I gave was insufficient to disprove soundness of Hope+C. On the other hand, no example can *prove* soundness of a type system. So, let me try a bit further. What happens if I extend your example as follows [I can read Hope but writing it is another matter, so forgive me if I stick to Haskell :-)]: let unpack w= let Win x = w in x same (x, y) = unpack x == unpack y in same (index (wl, 1), index (wl, 2)) Does that type? Looking at your typing rules I thought it would, but please correct me if I am wrong. -- Martin
Objects with state, or FP + OOP = Haskell++
Evan Ireland writes:
My formal proposal for existential types in Haskell is "make them the same as
in Hope+C".
This message is to point out some of the difficulties and possible
solutions we have encountered with existential types.
It seems to be rather difficult to establish soundness of type systems
with existential types. The reason is that these systems usually rely
on "Skolemization", a meta-logical construct. In fact, the original
type system of Hope+C seems to be unsound, since Skolem-constants can
escape the body of polymorphic functions and therefore cause different
types to be identified. Here is a (simplified) example:
Suppose we have a heterogeneous list of windows:
ws:: [ex a. Win a = a]
and an indexing function
index:: [ex a. Win a = a] - Int - ex a. Win a.
Then,
index ws 1 :: ex a. Win a = a
index ws 2 :: ex a. Win a = a
but, since the list is heterogeneous, we can not expect that the result
of the two applications of "index" are the same. This is reflected by
the fact that (ex a. Win a = a) is a type scheme, not a type. To get
at the "true" type of a value, the value has to be "opened". In our
example, both index-applications have to be opened separately,
resulting in two different types. Therefore, all is well in type
systems such as Mitchell Plotkin's which have true existential
types.
If we use Skolemization, however, it is easy to run into problems if we
are not careful. The "obvious" Skolemized type for index would be
[Win A = A] - Int - Win A
(Skolem constants written as single capitals here). But then,
index ws 1: A
index ws 2: A
and we conclude that "index" returns the same type every time!
So why not use MitchellPlotkin's system, which does not rely on
Skolemization? Unfortunately, this system does not have the principal
type property, and, therefore, has no type reconstruction.
A system which *has* principal types and comes with a soundness proof
is the topic of Konstantin Laufer's thesis at NYU which is currently
being written up. This system also uses Skolemization, but it
carefully restricts the scopes of Skolem constants. The problem of
designing a type system for existential types that has the principal
type property and at the same time does not rely on Skolemization
is still open, as far as I know.
Martin Odersky
Yale University
References:
@inproceedings{
AUTHOR = "Mitchell, J. and Plotkin, G.",
BOOKTITLE = "Proc. 12th ACM Symp. on Principles of Programming Languages",
PAGES = "37-51",
TITLE = "{Abstract Types have Existential Type}",
YEAR = "1985"}
@inproceedings{
AUTHOR = {K. L\"{a}ufer and M. Odersky},
TITLE = {Type Classes are Signatures of Abstract Types},
BOOKTITLE = {Proc. Phoenix Seminar and Workshop on Declarative
Programming},
MONTH = nov,
YEAR = {1991}
}
@inproceedings{
AUTHOR = {L\"{a}ufer, K. and Odersky, M.},
TITLE = {An Extension of ML with First-Class Abstract Types},
BOOKTITLE = {Proc. ACM SIGPLAN Workshop on ML and its Applications},
YEAR = {1992}
}
