- Haskell - Haskell.org

LOPSTR'04 call for papers (extended deadlines!)
by Sandro Etalle 27 Apr '04

27 Apr '04

LOPSTR 2004 Verona, Italy, August 26-28, 2004 http://www.sci.univr.it/~lopstr04 CALL FOR PAPERS ***EXTENDED DEADLINE*** The aim of the LOPSTR series is to stimulate and promote international research and collaboration on logic-based program development, and the workshop is open to contributions in logic-based program development in any language paradigm. Starting this year, LOPSTR will put extra emphasis to the field of verification; in fact LOPSTR will also incorporate the VCL (verification in computational logic) workshop series. LOPSTR'04 will be held at the University of Verona http://www.univr.it co-located with SAS 2004 http://www.sci.univr.it/~sas04, the International Static Analysis Symposium, PEPM 2004 http://www.sci.univr.it/~pepm04 - ACM SIGPLAN 2004 Workshop on Partial Evaluation and Semantics Based Program Manipulation, and PPDP 2004 http://www.sci.univr.it/~ppdp04 - 6th ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming. Past workshops were held in Manchester, UK (1991, 1992, 1998), Louvain-la-Neuve, Belgium (1993), Pisa, Italy (1994), Arnhem, the Netherlands (1995), Stockholm, Sweden (1996), Leuven, Belgium (1997), Venice, Italy (1999), London, UK (2000), Paphos, Cyprus (2001), Madrid, Spain (2002), Uppsala, Sweden (2003). Since 1994 the proceedings have been published in the LNCS series of Springer-Verlag. LOPSTR also aims to be a lively, friendly forum for presenting and discussing work in progress, so it is a real workshop in the sense that it is also intended to provide useful feedback to authors on their preliminary research. Formal proceedings of the workshop are produced only after the workshop, so that authors can incorporate this feedback in the published papers. Scope of the Workshop We solicit extended abstracts and full papers. Topics of interest cover all aspects of logic-based program development, all stages of the software life cycle, and issues of both programming-in-the-small and programming-in-the-large. The following is a non-exhaustive list of topics: * specification * synthesis * verification * transformation * specialisation * analysis * optimisation * composition * reuse * applications and tools * proofs as programs * component-based software development * agent-based software development * software architectures * design patterns and frameworks * program refinement and logics for refinement Submission Guidelines Authors can either submit extended abstracts (short papers) describing work in progress or they can choose to submit full papers. Contributions should be written in English and should be submitted electronically in Postscript or PDF format at http://profs.sci.univr.it/~lopstr04/index.html. Authors are also asked to send the title and abstract of their submission three days before the deadline to lopstr04(a)sci.univr.it. Prospective authors who have difficulties for the electronic submission may contact the chairman at lopstr04(a)sci.univr.it. Extended abstracts should not exceed 6 pages in llncs format and may describe work in progress. Promising abstracts relevant to the scope of LOPSTR will be selected for presentation at the workshop. The submission deadline for extended abstract is May 17, 2004 (extended, strict). Full papers should not exceed 16 pages (including references) in llncs format. These papers will be judged using ordinary conference quality criteria and accepted papers will have to be presented at the workshop and will automatically appear in the pre-proceedings as well as in the final collection of papers, published in the LNCS series. The submission deadline for full papers is May 7, 2004 (extended, strict). Accepted papers and abstracts will be collected in informal pre-proceedings which will be available at the workshop. After the workshop, authors of extended abstract which are judged mature for publication will be invited to submit full papers. These will be reviewed according to the usual refereeing procedures, and accepted papers will be published in the final collection of papers (together with the accepted full papers) which is expected to be published in the Lecture Notes in Computer Science series by Springer-Verlag. All the full papers accepted before the workshop will automatically appear in that book as well; there will be no additional refereeing (although authors will be given a chance to revise their paper, if they so wish, based upon the feedback from the LOPSTR event). Program Committee * Annalisa Bossi (Italy) * Gilles Barthe (France) * Francisco Bueno (Spain) * Maurice Bruynooghe (Belgium) * Giorgio Delzanno (Italy) * Sandro Etalle (The Netherlands) program chair * Tom Ellman (USA) * Patricia M. Hill (UK) * Norbert Fuchs (Switzerland) * Gopal Gupta (USA) * Kung-Kiu Lau (UK) * Fabio Martinelli (Italy) * Alberto Pettorossi (Italy) * Andreas Podelski (Germany) * Abhik Roychoudhury (Singapore) * C.R. Ramakrishnan (USA) * Wim Vanhoof (Belgium) * German Vidal (Spain) Important dates * submission deadline for full papers: May 7, 2004 (extended, strict) * submission deadline for extended abstracts: May 17, 2004 (extended, strict) * Notification: June 6 * Camera-ready: June 16 Sponsor Lopstr 2004 is sponsored by the Association for Logic Programming (ALP) http::/www.cwi.nl/projects/alp

1 0

Re: sizeFM type
by Serge D. Mechveliani 27 Apr '04

27 Apr '04

Alexander is right. Also as Integer has more sense than Int, I would suggest for the future standard Haskell library to have Integer as default. For example: length :: [a] -> Integer smallLength :: [a] -> Int ----------------- Serge Mechveliani mechvel(a)botik.ru On Sun, Apr 25, 2004 at 03:18:20PM -0400, S. Alexander Jacobson wrote: > >[..] > Dell's Poweredge servers address up to 32GB of > memory today! There are already 5.7 billion > people on the planet (>2^31) and 741 million phone > lines. In my mind, there is NO QUESTION that 2^31 > keys is a reasonable size for a FiniteMap or will > be in the very very near future. > > Moreover, it is not clear that the CPU/memory > overhead of returning Integer rather than Int for > sizeFM is sufficiently high to be worth bothering > the programmer about. On Sun, 2004-04-25 Serge D. Mechveliani wrote to glasgow-haskell-users > > > Dear GHC developers, > > > > > > Probably, it is better to provide Integer > > > or Integral a => a > > > instead of Int > > > in the function > > > sizeFM :: FiniteMap k e -> Int

12 18

4 Vacancies at St Andrews
by Kevin Hammond 27 Apr '04

27 Apr '04

A reminder that the deadline for application is tomorrow, 28th April. We have two chairs and two lectureships open to the best candidates. I would welcome some good functional programmers, of course, and am happy to answer any questions! Further details are found at http://www.dcs.st-andrews.ac.uk/news/jobs.php Application forms are available at http://www.st-andrews.ac.uk/hr/recruitment/vacancies Best Wishes, Kevin

1 0

RE: [Haskell] Re: sizeFM type
by Simon Peyton-Jones 27 Apr '04

27 Apr '04

Could we move this debate to Haskell-café? Simon | -----Original Message----- | From: haskell-bounces(a)haskell.org [mailto:haskell-bounces@haskell.org] On Behalf Of Serge D. | Mechveliani | Sent: 27 April 2004 05:49 | To: Ketil Malde | Cc: haskell(a)haskell.org | Subject: Re: [Haskell] Re: sizeFM type | | On Mon, Apr 26, 2004 at 10:09:18PM +0200, Ketil Malde wrote: | > "Serge D. Mechveliani" <mechvel(a)botik.ru> writes: | > | > > Alexander is right. | > > | > > Also as Integer has more sense than Int, | > > I would suggest for the future standard Haskell library to have | > > Integer as default. For example: | > > length :: [a] -> Integer | > > smallLength :: [a] -> Int | > | > Hmm...isn't it possible to use a class here? Perhaps even Num? | > | > class Num a where .... | > : | > length :: [b] -> a | > : | > | | I think, for many functions, like length, it is most natural to | return Integer only. | And it is also natural for many instances (domains) D to provide | maps like toInteger, fromInteger. | Just follow mathematics. | | Example: length xs :: (Rational, Rational) | looks unnatural, | but fromInteger (length xs) :: (Rational, Rational) | looks natural. | | ----------------- | Serge Mechveliani | mechvel(a)botik.ru | | | _______________________________________________ | Haskell mailing list | Haskell(a)haskell.org | http://www.haskell.org/mailman/listinfo/haskell

1 0

ANNOUNCE: GHC version 6.2.1
by Simon Marlow 26 Apr '04

26 Apr '04

============================================================ The (Interactive) Glasgow Haskell Compiler -- version 6.2.1 ============================================================ We are pleased to announce a new patchlevel release of the Glasgow Haskell Compiler (GHC), version 6.2.1. As usual for patchlevel releases, this is mainly a bugfix release and should not break any code that was working with the previous major release (6.2). We did sneak a couple of new features into the compiler: - The "threaded runtime system" is included by default. To link a program with this variant of the RTS, add the -threaded option when linking. The main advantage of the threaded RTS is that it allows calls to foreign functions which block, while allowing other concurrent Haskell threads to continue running. - A debugging variant of the RTS is also included. Use -debug when linking to get it. The debugging RTS includes lots of sanity checking and has some extra options for producing debugging output while your Haskell program is running. How to get it ~~~~~~~~~~~~~ The easy way is to go to the WWW page, which should be self-explanatory: http://www.haskell.org/ghc/ We supply binary builds in the native package format for various flavours of Linux and BSD, and in Windows Installer (MSI) form for Windows folks. Binary builds for other platforms are available as a .tar.gz which can be installed wherever you want. The source distribution is also available from the same place. Packages will appear as they are built - if the package for your system isn't available yet, please try again later. Background ~~~~~~~~~~ Haskell is a standard lazy functional programming language; the current language version is Haskell 98, agreed in December 1998 and revised December 2002. GHC is a state-of-the-art programming suite for Haskell. Included is an optimising compiler generating good code for a variety of platforms, together with an interactive system for convenient, quick development. The distribution includes space and time profiling facilities, a large collection of libraries, and support for various language extensions, including concurrency, exceptions, and foreign language interfaces (C, whatever). GHC is distributed under a BSD-style open source license. A wide variety of Haskell related resources (tutorials, libraries, specifications, documentation, compilers, interpreters, references, contact information, links to research groups) are available from the Haskell home page (see below). On-line GHC-related resources ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Relevant URLs on the World-Wide Web: GHC home page http://www.haskell.org/ghc/ Haskell home page http://www.haskell.org/ comp.lang.functional FAQ http://www.cs.nott.ac.uk/~gmh/faq.html System requirements ~~~~~~~~~~~~~~~~~~~ To compile programs with GHC, you need a machine with 64+MB memory, GCC and perl. This release is known to work on the following platforms: * i386-unknown-{linux,*bsd,mingw32} * sparc-sun-solaris2 * alpha-dec-osf3 * powerpc-apple-darwin (MacOS/X) Ports to the following platforms should be relatively easy (for a wunderhacker), but haven't been tested due to lack of time/hardware: * hppa1.1-hp-hpux{9,10} * i386-unknown-solaris2 * mips-sgi-irix{5,6} * {rs6000,powerpc}-ibm-aix The builder's guide on the web site gives a complete run-down of what ports work; it can be found at http://www.haskell.org/ghc/docs/latest/html/building/building-guide.html Mailing lists ~~~~~~~~~~~~~ We run mailing lists for GHC users and bug reports; to subscribe, use the web interfaces at http://www.haskell.org/mailman/listinfo/glasgow-haskell-users http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs There are several other haskell and ghc-related mailing lists on www.haskell.org; for the full list, see http://www.haskell.org/mailman/listinfo/ Please report bugs using our SourceForge page at http://sourceforge.net/projects/ghc/ or send them to glasgow-haskell-bugs(a)haskell.org. GHC users hang out on glasgow-haskell-users(a)haskell.org. Bleeding edge CVS users party on cvs-ghc(a)haskell.org.

3 2

RE: [Haskell] Why is newChan in the IO Monad?
by Nick Benton 26 Apr '04

26 Apr '04

Channels have identity, so allocating a new one is a side effecting operation. Having it outside the IO monad would require (for example): (newChan, newChan) = (let x = newChan in (x,x)) which is wrong. If you wrap newChan in unsafePerformIO then the compiler will feel free to apply rewrites like the above, which is unlikely to be what you wanted. Nick -----Original Message----- From: haskell-bounces(a)haskell.org [mailto:haskell-bounces@haskell.org] On Behalf Of S. Alexander Jacobson Sent: 23 April 2004 19:22 To: Haskell Mailing List Subject: [Haskell] Why is newChan in the IO Monad? Nothing actually happens when newChan is called except construction of a new datastructure. It would be nice to have non IO monad code be able to create a new Chan that gets passed to IO code that uses it somewhere else. Alternatively, is there a way to create a Chan outside the IO monad? -Alex- _________________________________________________________________ S. Alexander Jacobson mailto:me@alexjacobson.com tel:917-770-6565 http://alexjacobson.com _______________________________________________ Haskell mailing list Haskell(a)haskell.org http://www.haskell.org/mailman/listinfo/haskell

4 3

UNIF'04 workshop @ IJCAR 2004: First Call for Papers
by Michael Kohlhase 26 Apr '04

26 Apr '04

[ Apologies for multiple copies which are unavoidable. -Michael. ] First Call for Papers/Abstracts/System descriptions UNIF 2004 18th International Workshop on Unification July 4-5, 2004, Cork, Ireland Affiliated with IJCAR'04 http://www.faculty.iu-bremen.de/mkohlhase/event/unif04/ UNIF is the main international meeting on unification. Unification is concerned with the problem of identifying given terms, either syntactically or modulo a given logical theory. Syntactic unification is the basic operation of most automated reasoning systems, and unification modulo theories can be used, for instance, to build in special equational theories into theorem provers. The aim of UNIF 2004, as that of the previous meetings, is to to bring together people interested in unification, present recent (even unfinished) work, and discuss new ideas and trends in unification and related fields. In particular, it is intended to offer a good opportunity for young researches and researchers working in related areas to get an overview of the current state of the art in unification theory and get in contact with the experts in the field. ---------------------------------------------------------------------- TOPICS OF INTEREST ---------------------------------------------------------------------- A non-exclusive list of topics of interest is: * Unification * E-unification * Unification Algorithms * Higher-Order Unification * String Unification * Context Unification * Combination problems * Disunification * Typed Unification * Related Topics * Constraint Solving * Tree Descriptions * Matching * Narrowing * Applications * Type Checking and Type Inference * Automated Deduction * Rewriting * Functional and Logic Programming * Grammars * Computational Linguistics * Implementations ---------------------------------------------------------------------- INVITED SPEAKERS ---------------------------------------------------------------------- There will be two invited speakers. ---------------------------------------------------------------------- IMPORTANT DATES ---------------------------------------------------------------------- Deadline for electronic submission: Friday, May 14, 2004 Email: unif04(a)iu-bremen.de Notification of acceptance: Monday, May 24, 2004 Deadline for camera-ready papers: Monday, June 7, 2004 Workshop: July 4 - 5, 2004 ---------------------------------------------------------------------- SUBMISSION DETAILS ---------------------------------------------------------------------- Authors are invited to submit via email an abstract (1-5 pages), a paper (no longer than 15 pages), or a system description (no more than 5 pages) in Postscript or PDF format to: unif04(a)iu-bremen.de before May 14, 2004. Authors are encouraged to use LaTeX2e and the Springer llncs class. ---------------------------------------------------------------------- PUBLICATION ---------------------------------------------------------------------- Accepted papers, abstracts and system descriptions will be included in the proceedings which will be available at the workshop. ---------------------------------------------------------------------- ORGANIZING COMMITTEE ---------------------------------------------------------------------- Michael Kohlhase (International University Bremen, Germany) Hitoschi Ohsaki (National Institute of Advanced Industrial Science and Technology, Amagasaki, Japan) Steve Prestwich (Universtity College, Cork, Ireland) Ralf Treinen (Ecole Normale Superieure, Cachan, France) Manfred Schmidt-Schauss (Johann Wolfgang Goethe-Universit"at Frankfurt am Main, Germany) -- ------------------------------------------------------------------------- Prof. Dr. Michael Kohlhase, Office: Research 1, Room 62 Professor for Computer Science Campus Ring 12, School of Engineering & Science D-28758 Bremen, Germany International University Bremen tel/fax: +49 421 200 3140/3103 http://www.cs.cmu.edu/~kohlhase e-mail: <m.kohlhase(a)iu-bremen.de> --------------------------------------------------------------------------

1 0

a newbie question
by Ben_Yu＠asc.aon.com 26 Apr '04

26 Apr '04

Hi there. I got this question while I'm messing around with my toy monad. I was thinking about creating a generic monad that can persist state change even when fail is called. The StateT monad will discard the state change so it makes it hard to add tracing to the program. (at least to me. If there's any nice way of doing this, please kindly instruct me.) Then I come to this problem. I can summarize it by removing all irrelavant stuff like this: to_write :: ((x->a)->r) -> (x->(a,s)) -> (r,s) to_write f1 f2 = ... how do I implement it? I can't get a data of type x, so the only way is to pass f2 into f1. In order to pass f2 to f1, I have to discard the s returned by f2. Thus, I lose the s forever. Hope I'm getter myself clear. Any comment is welcome. Ben.

3 2

WSC9 - Call for Papers
by Ajith Abraham 25 Apr '04

25 Apr '04

** WSC9 - Call for Papers *** ### FREE ONLINE CONFERENCE ### WSC9: 9th Online World Conference on Soft Computing in Industrial Applications September 20th - October 08th, 2004 ** On the World Wide Web ** Conference URL: http://www.cs.nmt.edu/~wsc9/ Mirror: http://wsc9.softcomputing.net/ General Information about WSC9: Original papers and tutorials are invited for the 9th Online World Conference on Soft Computing in Industrial Applications (WSC9) to be held on the Internet. WSC9 aims at bringing together outstanding research and developments in the field of soft computing (evolutionary computation, fuzzy logic, neural networks, and their fusion) and its applications across the world with the goal to publish high-quality research quickly and with less cost. Accepted papers of WSC9 will be published as an edited volume by Springer Verlag, Germany after the conference. Moreover, extended versions of selected papers of the conference will also be invited for a "fast track" submission for the Elsevier Science Applied Soft Computing Journal. We aim to have inspiring discussions between the authors and participants, and make them visible to everyone on the Internet. There will be a number of mirror sites around the world to make easier the access to this major event. Please note that the registration is open to everyone and it is completely free of charge. June 04th, 2004 Deadline for submissions of regular papers, online survey paper proposals and online tutorial proposals. Papers are submitted in electronic form as PDF-files through the conference web site. Authors are also encouraged to submit multi-media demonstrations (including software etc.) July 30th, 2004 Acceptance/rejection notification August 27th, 2004 Submission of full papers and online presentations September 20th - October 08th, 2004 Online conference November 12th, 2004 Submission of camera-ready papers for final review Topics of Interest: Submissions are invited in, but not limited to, any of the following areas: Soft Computing for Modeling, Control, and Optimization Fuzzy Control Neuro-Fuzzy Systems Genetic Fuzzy Systems Neuro-Fuzzy-Genetic Systems Software Agent Systems and Architectures Multi-Agent Architectures and Collaborative Learning Ant Colony Optimization Fuzzy Information Fusion Rough Sets Bayesian Networks Fuzzy Image Processing Bio-inspired Systems Artificial Neural Networks Support Vector Machines Evolutionary Algorithms, Simulated Annealing, Tabu Search Evolutionary Multiobjective Optimization Hybrid Optimization Techniques (integration of global search and local search techniques) Simulation Environments Data Mining Industrial Applications of Soft Computing Intelligent Information Retrieval Language Processing Robotics Autonomous Reasoning Fault Diagnosis Bioinformatics Web Intelligence Speech Processing Business Information Systems Knowledge Management Paper Submission Authors should fill up the online form and upload a full paper (max. 10 pages) in PDF format by June 04, 2004. Authors who are interested to submit a paper should send an expression of interest to: <wsc9(a)softcomputing.net> including title of paper and author details. Organized session proposals and tutorials are welcome. Please notify the Special Events Chair, Katrin Franke (katrin.franke(a)ipk.fhg.de) about your intention to organize a session/tutorial as soon as possible. For special sessions, please send session title, organizer’s name and e-mail address, a short synopsis of session objective (max. 100 words), organizer's expertise in the field, and a tentative list of papers in the proposed technical session. At least three session papers have to be submitted by June 04, 2004. For online proposals and survey papers, please send the abstract and biography of the presenter before June 04, 2004 and if approved send the final presentation paper by August 27th, 2004. Paper Acceptance: All accepted papers would be presented during the online conference. Participants are also encouraged to present multimedia presentations like online demonstrations, software, video clips etc.) to make the online discussions more interesting. Authors of accepted papers have to register and visit the conference website on a regular basis in order to respond to questions and comments on their paper without delay. By November 26th, 2004, camera-ready copies of extended papers have to be submitted for final inclusion in the conference proceedings. Significantly revised and enhanced versions of selected papers of the conference will also be invited for a "fast track" submission for the Applied Soft Computing Journal. WSC 9 Organization Honorary Chair Ronald Yager, Iona College, USA General Chair Ajith Abraham, Oklahoma State University, USA Program Chair Mario Köppen, Fraunhofer IPK Berlin, Germany International Co-chairs Frank Hoffmann, University of Dortmund, Germany Avineri Erel, Ben-Gurion University of the Negev, Israel Sponsorship Chair Rajkumar Roy, University of Cranfield, UK Publication Chair Bernard de Baets, Ghent University, Belgium Virtual Exhibition Chair Fabio Zambetta, University of Bari, Italy Special Events Chair Katrin Franke, Fraunhofer IPK Berlin, Germany Industrial Liason Chairs Antony Satyadas, IBM, USA Suthikshn Kumar, Larsen & Toubro Infotech, India Best Paper Award Chair Janos Abonyi, University of Veszprém, Hungary International Technical Program Committee Walter D. Potter, University of Georgia, USA Mark Embrechts, Rensselaer Polytechnic Institute, USA Hisao Ishibuchi, Osaka Prefecture University, Japan Thomas Sudcamp, Wright State University, USA Christian Wöhler, Daimler Chrysler AG, Germany Vasile Palade, Oxford University, UK Marley Vellasco, University College London, UK Yaochu Jin, Honda Research Institute Europe, Germany Yukinori Suzuki, Muroran Institute of Techology, Japan John Debanham, University of Technology Sydney, Australia Yanqing Zhang, Georgia State University, USA Srinivasan S.H., Satyam Computers, India Okyay Kaynak , Bogazici University, Turkey Hung T. Nguyen, New Mexico State University, USA Aureli Soria Frisch, FhG IPK Berlin, Germany Jae C. Oh, Syracuse University, USA Andrea Bonarini, Politecnico di Milano, Italy Andreas Koenig, University of Kaiserslautern, Germany Bart Baesens, Katholieke Universiteit Leuven, Belgium Brian Carse, University of the West of England, UK Christophe Marsala, University Pierre et Marie Curie Paris, France Detlef D. Nauck, BTexact Technologies Ipswich, UK Francisco Herrera, E.T.S. Ingeneria Informatica Granada, Spain Frank Klawonn, University of Applied Sciences Braunschweig/Wolfen, Germany Guy de TrÈ, Ghent University, Belgium Hani Abdel Kader Hagras, University of Essex, UK Javier Ruiz-del-Solar, Universidad de Chile, Chile Leandro dos Santos Coelho, Pontificia Universidade Catolica do Paran Curitib, Brazil Luis Magdalena, Ciudad Universitaria Madrid, Spain Mauro Dell'Orco, Polytechnic of Bari, Italy Sankar Kumar Pal, Indian Statistical Institute Kolkata, India SenÈn Barro Ameneiro, SEVIMAV Santiago de Compostela, Spain Vicent Torra, Universitat AutÚnoma de Barcelona, Spain Takeshi Furuhashi, Mie University, Japan Oscar Cordon, University of Granada, Spain Vitorino Ramos, CRVM IST, Portugal P. Saratchandran, Nanyang Technological University, Singapore Sonja Petrovic-Lazarevic, Monash University, Australia Andew Sung, New Mexico Institute of Mining and Technology, USA Zaheeruddin, Jamia Milia Islamia New Dehli, India Xiao-Zhi Gao, Helsinki University of Technology, Finland Edward Tunstel, NASA, USA Berend Jan van der Zwaag, University of Twente, The Netherlands Muhammad Sarfraz, King Fahd University of Petroleum and Minerals, Saudi Arabia ------------------------------------------------ Please address all general enquiries to <wsc9(a)softcomputing.net>

1 0

Re: [Haskell] Correct interpretation of the curry-howard isomorphism
by Bruno Oliveira 24 Apr '04

24 Apr '04

Hi! Thanks Connor, I enjoyed your answer, it was very illustrative. >> but then, it would be too easy to write this in haskell: >> >> coerce :: a -> b >> coerce x = undefined >> >> As an obvious consequence, Haskell type system would be unsound. >> >> So, I assumed that this would be a wrong interpretation. >This is the part of your email which frightens me the most. Of >course Haskell's type system is unsound! What factors lead you to >this kind of assumption? Clearly a misconception of mine. Is it a good excuse that people told me that (or I misunderstood them) :) ? >The type system does not become a logic until you populate some of >the types (hopefully only those corresponding to true propositions) >with the terms which describe the construction of proofs. You can't >pretend that Haskell is sound just by hoping that Curry and Howard >(when properly interpreted) won't be able to see the broken bits. >It's nonetheless an interesting question which bits you need to >throw away to get a sound language. You'll have to get rid of > y :: (p -> p) -> p > unJust :: Maybe wmd -> wmd >and hence the programming language features which enable them to >be constructed, in particular, pattern matching with incomplete >coverings, and general recursion. Yes, I thought about those implications, that's why I also thought (incorrectly) that it would be too limiting and therefore probably wrongly interpreted. It is also, not too hard to see, as you said, that general recursion would validate that interpretation (even without using any other primitives or functions): coerce :: a -> b coerce = coerce or even coerce :: a -> b coerce x = let y = y in y Then, even if we ignored the primitives, Haskell would still be unsound! Moreover, we could then say that most of the functional languages (which have a similar type system) are unsound. Right ? Is it "Charity" an exception on this? >There's an interesting paper `Elementary Strong Functional >Programming' by David Turner, in which he proposes such a language. >He suggests that, at least for paedagogical purposes, a functional >language which gave up completeness for consistency might be no >bad thing. I'm inclined to agree with him. I will take a look on it. >So I won't make any foolish and portentous pronouncements about >dependent types being the only way to save us from damnation. I'll >merely observe that we often use the unsound parts of programming >languages as the best approximations available to the programs >we really mean: we don't intend recursion to loop infinitely, >we just have no means to explain in the program why it doesn't; >we don't intend to apply unJust to Nothing, we just have no means >to explain in the program why this can't happen. Dependent types >support a higher level of articulacy about what is really going on, >reducing, but not removing entirely the need to work outside the >consistent fragment of the language. They do not save us from Satan >but from Wittgenstein. Whereon you know something, thereon speak! Dependent types definitely seem an advance to me. I saw recently a presentation of a very impressive tool (epigram - I wonder if you have heard about it :P). I'll be definitely take a better look on it as soon as I finish some work with more priority. Best Regards, Bruno

6 6